Major Section: OTHER
Example Forms:
(cw-gstack)
(cw-gstack :frames 10) ; show only the top 10 frames
(cw-gstack :frames '(1 10)) ; same as above: show only frames 1 through 10
(cw-gstack :frames '(10 20)) ; show only frames 10 through 20
(cw-gstack :evisc-tuple (evisc-tuple 3 4 nil nil))
; print with print-level 3 and print-length 4
(cw-gstack :evisc-tuple nil) ; print using default ``evisceration'',
; essentially the same as just above
(cw-gstack :evisc-tuple '(nil 3 4 (hide)))
; same as just above
General Form:
(cw-gstack :frames frames :evisc-tuple evisc-tuple)
where :frames and :evisc-tuple are optional, but if they are
supplied, their values are evaluated. The value of frames should be
either a natural number or a list of two natural numbers, the first less than
the second; and the value of evisc-tuple should be an
evisc-tuple (see evisc-tuple). If :evisc-tuple is omitted, then
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>. Also see set-iprint for an alternative to printing
``#'' and ``...''.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).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).
