ACL2退出代码137是什么意思？

Question

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

Answer 1

看来"Linux OOM杀手“杀了你的程序。

退出状态137意味着使用信号9 (SIGKILL)终止程序(请参见这里)：

当命令终止于号码为N的致命信号时，Bash使用值128+N作为退出状态。

128+9=137

日志中的这条消息告诉我们，您的ACL2证明消耗了10 of内存：

；；启动完整GC，分配10,736,500,736字节。

Linux有一个特性，当系统内存非常少时，它会杀死一个令人不快的进程。它被称为OOM杀手：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-mem和maybe-wash-memory，您可以使用它们来控制内存消耗。

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

不幸的是，这两个调用并不保证内存将被释放。考虑使用更强大的计算机作为你的证据。

Answer 2

一个137的退出代码表明它已经被bash和-9杀死了。

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