Tools for debugging FGL failures
In this topic we list some techniques for debugging FGL failures.
FGL keeps almost all of the state of its interpreter inside its interpreter
The stack is contained in a nested stobj inside the interpreter state, but
it can be dumped into a regular ACL2 object using the function
;; From within the ACL2 loop, save the stack into a constant (using std/util/defconsts.lisp): (defconsts *my-stack* (fgl::interp-st-extract-stack fgl::interp-st)) ;; Or put it in a state global, accessed as (@ :my-stack): (f-put-global ':my-stack (fgl::interp-st-extract-stack fgl::interp-st) state) ;; The following macro does the same as the call above: (fgl::save-fgl-stack :to :my-stack) ;; From within a raw Lisp break, save the stack as a defparameter: (defparameter *my-stack* (fgl::interp-st-extract-stack (cdr (assoc 'fgl::interp-st *user-stobj-alist*)))
Note: be sure NOT to do the latter when in a raw Lisp break resulting from a stack overflow! It may cause your Lisp to crash completely.
The stack object's type is major-stack, which is documented under fgl-stack. Essentially it is a nonempty list of major-frame objects representing scopes such as function calls and rewrite rules. Each frame contains some variable bindings and debug info identifying what rule application that frame represents, as well as a minor stack representing a nesting of lambdas.
A useful tool for examining a stack object is
It may be useful to set a lower recursion limit for the FGL interpreter.
The default is 10000, but it may help to catch runaway rule applications to
limit it to 1000 or less. This can be adjusted by setting the state global
Most of the work of FGL is done by rewrite rules -- even the expansion of function definitions is just treated as an application of a rewrite rule. Tracing rewrites can help debug problems due to rule applications unexpectedly failing or recurring out of control, etc. See fgl-rewrite-tracing.