Как избежать сбоя низкоуровневого отладчика при компиляции ACL2 на SBCL?

Как избежать сбоя низкоуровневого отладчика при компиляции ACL2 на SBCL? Вот сообщение об ошибке, которое я получаю при компиляции с использованием SBCL 1.2.3 в Linux:

<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>

sbcl acl2
person interestedparty333    schedule 03.09.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Мэтт Кауфманн пишет:

Чтобы построить ACL2 на SBCL, необходимо увеличить размер памяти сверх значения по умолчанию 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 "$@"

person interestedparty333    schedule 03.09.2014