# 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)