the number of prover steps most recently taken

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)
                           (value '(value-triple nil))))
       (defun f2 ...))