Major Section: OTHER
Stack overflows may occur, perhaps caused by looping rewrite rules. In some Lisps, especially GCL, stack overflows often manifest themselves as segmentation faults, causing the entire ACL2 image to crash. Finding looping rewrite rules can be tricky, especially if you are using books supplied by other people. (However, see set-rewrite-stack-limit for a way to avoid stack overflows caused by rewriter loops.)
A wonderful trick is the following. When there is a stack overflow
during a proof, abort and then try it again after turning on rewrite
stack monitoring with :brr t. When the stack
overflows again, exit to raw Lisp. How you exit to raw Lisp depends
on which Lisp you are using. In Allegro Common Lisp, for example,
the stack overflow will leave you in an interactive break. It is
often a good idea to exit the break immediately (e.g., using
:pop if you use Allegro Common Lisp, or :q using GCL), which
will leave you in the top-level ACL2 command loop, after which it is
recommended to leave that loop using :q. That will leave
you in raw Lisp. Then, execute
(cw-gstack)If the loop is in the rewriter, it will probably be evident! You can re-enter the ACL2 loop now with
(lp).
Note: By default, cw-gstack ``eviscerates'' terms, printing
abbreviated representations of large terms. The user can control
this behavior by using (cw-gstack :evisc-tuple x), where x
is nil or an evisceration tuple; see ld-evisc-tuple. For
example, (cw-gstack :evisc-tuple nil) will avoid all
evisceration, while the default behavior can be obtained by using
(cw-gstack :evisc-tuple '(nil 3 4 (hide))), meaning that
substructures deeper than 3 are replaced by ``#'' and those
longer than 4 are replaced by ``...'', and terms of the form
(hide ...) are printed as <hidden>.
If you are in GCL the stack overflow may cause a segmentation fault
and abort the Lisp job. This makes it harder to debug but here is
what you do. First, re-create the situation just prior to
submitting the form that will cause the stack overflow. You can do
this without suffering through all the proofs by using the
:ld-skip-proofsp option of ld to reload your
scripts. Before you submit the form that causes the stack overflow,
exit the ACL2 command loop with :q. In raw GCL type:
(si::use-fast-links nil)This will slow GCL down but make it detect and signal stack overflows rather than overwrite the system memory. Now reenter the ACL2 command loop with
(lp).
Now carry on as described above, turning on rewrite stack monitoring
with :brr t and provoking the stack overflow. When
it occurs, you will be in an interactive break. Exit to raw Lisp
with two successive :q's, one to get out of the error break
and the next to get out of the top-level ACL2 command loop. Then
in raw GCL execute (cw-gstack).
Suggestion: Once you have found the loop and fixed it, you should
execute the ACL2 command :brr nil, so that you don't slow
down subsequent proof attempts. If you are in GCL, you should also
get into raw Lisp and execute (si::use-fast-links t).