Major Section: MISCELLANEOUS
For discussions of prover step limits, See set-prover-step-limit and
see with-prover-step-limit. The value of the form
(last-prover-steps state) indicates the number of prover steps taken, in
the sense described below, for the most recent context in which an event
summary would normally be printed. Note that the value of
(last-prover-steps state) is updated for all events, and for all
other forms such as calls of thm or certify-book, that would
print a summary -- regardless of whether or not such output is inhibited
(see set-inhibit-output-lst and see set-inhibited-summary-types). In
particular, the value is updated (typically to nil) for table
events, even when no summary is printed; for example, the value is
updated to nil for table events such as (logic),
(program), and even calls of set-prover-step-limit.
The value of (last-prover-steps state) is determined as follows, based on
the most recent summary context (as described above):
nil, if no prover steps were taken; else,the (positive) number of steps taken, if the number of steps did not exceed the starting limit; else,
the negative of the starting limit.
We conclude with a remark for advanced users who wish to invoke
last-prover-steps in the development of utilities that track prover
steps. Suppose that you want to write a utility that takes some action based
on the number of prover steps performed by the first defun event that is
generated, among others, for example the number of prover steps taken to
admit f1 in the following example.
(progn (defun f1 ...)
(defun f2 ...))
A solution is to record the steps taken by the first defun before
executing subsequent events, as follows (see make-event).
(progn (defun f1 ...)
(make-event (pprogn (f-put-global 'my-step-count
(last-prover-steps state)
state)
(value '(value-triple nil))))
(defun f2 ...))
