Major Section: OTHER
General Forms: (pstack) ; inspect break (pstack t) ; inspect break, printing all calls in abbreviated form (pstack :all) ; as above, but only abbreviating the ACL2 world
When the form (pstack) is executed during a break from a proof, or at the
end of a proof that the user has aborted, a ``process stack'' (or ``prover
stack'') will be printed that gives some idea of what the theorem prover has
been doing. Moreover, by evaluating (verbose-pstack t) before
starting a proof (see verbose-pstack) one can get trace-like information
about prover functions, including time summaries, printed to the screen
during a proof. This feature is currently quite raw and may be refined
considerably as time goes on, based on user suggestions. For example, the
usual control of printing given by set-inhibit-output-lst is irrelevant
for printing the pstack.
The use of (pstack t) or (pstack :all) should only be used
by those who are comfortable looking at functions in the ACL2 source code.
Otherwise, simply use (pstack).
Entries in the pstack include the following (listed here alphabetically, except for the first).
preprocess-clause, simplify-clause, etc. (in general,xxx-clause):
top-level processes in the prover ``waterfall''
clausify: splitting a goal into subgoals
ev-fncall: evaluating a function on explicit arguments
ev-fncall-meta: evaluating a metafunction
forward-chain: building a context for the current goal using
forward-chaining rules
induct: finding an induction scheme
pop-clause: getting the next goal to prove by induction
process-assumptions: creating forcing rounds
remove-built-in-clauses: removing built-in clauses (see built-in-clause)
process-equational-polys: deducing interesting equations
remove-trivial-equivalences: removing trivial equalities (and
equivalences) from the current goal
rewrite-atm: rewriting a top-level term in the current goal
setup-simplify-clause-pot-lst: building the linear arithmetic database
for the current goal
strip-branches, subsumption-replacement-loop: subroutines of
clausify
waterfall: top-level proof control
