1

ACL2 退出代码 137 是什么意思?输出如下所示:

Form:  ( INCLUDE-BOOK "centaur/ubdds/param" ...)
Rules: NIL
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
:REDUNDANT
Note: not introducing any A4VEC field bindings for A, since none of
its fields appear to be used.
Note: not introducing any MODSCOPE field bindings for SCOPE, since
none of its fields appear to be used.


;;; Starting full GC,  10,736,500,736 bytes allocated.
Exit code from ACL2 is 137
top.cert seems to be missing
4

2 回答 2

1

看起来像“Linux OOM 杀手”杀死了你的程序。

退出状态 137 表示程序以信号 9 (SIGKILL) 终止(参见此处):

当命令在编号为 N 的致命信号上终止时,Bash 使用值 128+N 作为退出状态。

128+9=137

日志中的这条消息告诉我们,您的 ACL2 证明消耗了 10Gb 的内存:

;;; 开始完整的 GC,分配了 10,736,500,736 个字节。

Linux 有一个功能,当系统内存非常低时,它会杀死有问题的进程。它被称为OOM Killer:https ://www.kernel.org/doc/gorman/html/understand/understand016.html

此类事件由内核记录。您可以立即看到它们,以确保:

$ dmesg |grep -i "killed process"
Mar  7 02:43:11 myhost kernel: Killed process 3841 (acl2) total-vm:128024kB, anon-rss:0kB, file-rss:0kB

有两个ACL2调用 :可以用来控制内存消耗set-max-memmaybe-wash-memory

(include-book "centaur/misc/memory-mgmt" :dir :system) ;; adds ttag
(value-triple (set-max-mem (* 4 (expt 2 30))))           ;; 4 GB

不幸的是,这两个调用并不能保证内存会被释放。考虑使用功能更强大的计算机进行证明。

于 2017-09-03T02:29:50.210 回答
0

退出代码 137 表明它已被带有 -9 的 bash 杀死

参考:http ://www.tldp.org/LDP/abs/html/exitcodes.html

于 2015-06-04T20:52:46.897 回答