How can I avoid crashing in the low-level debugger when compiling ACL2 to SBCL?

How can I avoid crashing in the low-level debugger when compiling ACL2 to SBCL? Here is the error message I get when compiling using SBCL 1.2.3 on 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> 

      

+3


source to share


1 answer


Matt Kaufman writes:

To create ACL2 on SBCL, you need to increase the memory size beyond the default of 536870912 bytes. I usually use the "--dynamic-space-size 2000" option, for example this in my ~ / 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 "$@"

+2


source







All Articles