3

SBCL で ACL2 をコンパイルするときに、低レベル デバッガーへのクラッシュを回避するにはどうすればよいですか? Linux で SBCL 1.2.3 を使用してコンパイルすると、次のエラー メッセージが表示されます。

<snip>
ACL2 loading '((COMP-FN :EXEC NIL "1" STATE)).
 NIL

Finished loading '((COMP-FN :EXEC NIL "1" STATE)).

******************************************************************************
          Initialization complete, beginning the check and save.
******************************************************************************
Heap exhausted during garbage collection: 7776 bytes available, 15360 requested.
 Gen StaPg UbSta LaSta LUbSt Boxed Unboxed LB   LUB  !move  Alloc
Waste   Trig    WP  GCs Mem-age
   0:     0     0     0     0     0     0     0     0     0        0
  0 10737418    0   0  0.0000
   1:     0     0     0     0     0     0     0     0     0        0
  0 10737418    0   0  0.0000
   2:     0     0     0     0     0     0     0     0     0        0
  0 10737418    0   0  0.0000
   3: 30389 30230     0     0 12248  2558    25    25     0 448761472
38039936 408790346    0   1  0.8870
   4: 32241 32765 32025 32577  1417  1177   182    42     0 91900528
439696  2000000    0   0  0.0000
   5:     0     0     0     0  1248   157     0     0     0 46039040
  0  2000000 1197   0  0.0000
   6:     0     0     0     0     0     0     0     0     0        0
  0  2000000    0   0  0.0000
   Total bytes allocated    = 586701040
   Dynamic-space-size bytes = 1073741824
GC control variables:
   *GC-INHIBIT* = false
   *GC-PENDING* = false
   *STOP-FOR-GC-PENDING* = false
fatal error encountered in SBCL pid 26451(tid 46912509763072):
Heap exhausted, game over.

Welcome to LDB, a low-level debugger for the Lisp runtime environment.
ldb>
4

1 に答える 1

2

マット・カウフマンは次のように書いています。

SBCL で ACL2 を構築するには、デフォルトの 536870912 バイトを超えてメモリ サイズを増やす必要があります。通常、オプション「--dynamic-space-size 2000」を使用します。たとえば、~/bin/sbcl では次のようになります。

<some-path>/sbcl-1.2.2-x86-64-linux/src/runtime/sbcl --core <some-path>/sbcl-1.2.2-x86-64-linux/output/sbcl.core --dynamic-space-size 2000 "$@"

于 2014-09-03T12:47:47.390 に答える