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

.

### VERBOSE-PSTACK -- seeing what is the prover up to

`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

`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