		Search-engine friendly clone of the ACL2 documentation.

Last-prover-steps

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 summary printed for an event typically includes a line showing the prover steps counted, for example as follows.

Prover steps counted:  7240

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 more generally, for all forms that are set up to print a summary, such as calls of thm or certify-book — regardless of whether or not summary 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, e.g., with (thm (equal x x)); 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.

Note that the ``most recently completed event'' in this sense includes compound events. Consider the following example.

(progn (thm (equal (append (append x y) z) (append x y z)))
       (thm (equal (car (cons x y)) x)))

The summaries show (in some ACL2 versions, at least) 435 steps for the first call of thm and 7 steps for the second call of thm, with 442 steps thus shown in the summary for the entire progn call. Subsequent evaluation of (last-prover-steps state) returns 442. On the other hand, suppose that (set-prover-step-limit 440) is evaluated immediately before evaluating the progn call above. Then the summaries show the following for the two thm calls and the progn call, in order as follows.

Prover steps counted:  435
Prover steps counted:  More than 5
Prover steps counted:  More than 440

Since the most recently completed event is the progn call, then (last-prover-steps state) returns -440.

We conclude with two remarks for advanced users who wish to invoke last-prover-steps in the development of utilities that track prover steps.

Remark 1. Suppose that you want to write a utility that takes some action based on the number of prover steps performed by the first event that is generated within a sequence of events, 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 ...))

Remark 2. It is possible to write utilities that are treated as events for purposes of the discussion above; that is, their calls can be followed by evaluating (last-prover-steps state) as described above. For an example of how to do this using the ACL2 system macro with-ctx-summarized, see the implementation of prove$ in community-book books/tools/prove-dollar.lisp.