		Search-engine friendly clone of the ACL2 documentation.

Cw-gstack

Debug a rewriting loop or stack overflow

After break-rewrite is enabled (with :brr t or in the scope of with-brr-data), cw-gstack can be invoked to show a stack backtrace when a proof is interrupted (because of control-c or because of a loop).

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 by default, 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>; this behavior can be changed by setting the :TERM evisc-tuple (see set-evisc-tuple). Also see set-iprint for an alternative to printing ``#'' and ``...''.

Stack overflows may occur, perhaps caused by looping rewrite rules. In some Lisps, stack overflows may 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.)

Normally, a stack overflow will cause the printing of an error message that suggests how to proceed. Just follow those instructions, and you will generally be able to see what is causing the loop.

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.