		Search-engine friendly clone of the ACL2 documentation.

Fgl-debugging

Save-fgl-stack

Save the FGL stack to a state global for easy inspection.

Saves the stack from the fgl-interpreter-state into an ACL2 state global, :stack by default and otherwise controlled by the :to keyword argument. Examples of usage:

(fgl::save-fgl-stack)               ;; accessed via (@ :stack)
(fgl::save-fgl-stack :to :my-stack) ;; accessed via (@ :my-stack)
(fgl::save-fgl-stack :to a-stack)   ;; accessed via (@ a-stack)

;; if somehow you need to access the stack in an
;; interpreter state other than @('fgl::interp-st'):
(fgl::save-fgl-stack :to :my-stack :interp-st my-interp-st)

;; inspect the bottom 20 frames of the stack:
(nthcdr (- (len (@ :stack)) 20) (@ :stack))