Pstack
Seeing what the prover is up to
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+: evaluating a function on explicit arguments while assuming
that warrant hypotheses are true
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
Subtopics
- Verbose-pstack
- Seeing what the prover is up to (for system hackers)
