Sets the step-limit used by the ACL2 prover

This event provides a way to limit the number of so-called ``prover
steps'' permitted for an event. See with-prover-step-limit for a way
to specify the limit on prover steps for a single event, rather than globally.
For a related utility based on time instead of prover steps, see with-prover-time-limit. For examples of how step limits work, see the
community book

Note: This is an event! It does not print the usual event summary
but nevertheless changes the ACL2 logical world and is so recorded.
Moreover, its effect is to set the `ACL2-defaults-table`, and hence its
effect is `local` to the book or `encapsulate` form containing it;
see ACL2-defaults-table.

Example Forms: (set-prover-step-limit *default-step-limit*) ; no limit on prover steps (set-prover-step-limit nil) ; abbreviation for the form just above (set-prover-step-limit 10000) ; allow at most 10,000 prover steps per event General Form: (set-prover-step-limit expr)

where

This event specifies the limit on the number of ``steps'' counted by the
ACL2 prover during processing of an event. Currently, a step is counted for
each call of the system functions

Depending on the computer you are using, you may have less than a half-hour
of time before the number of prover steps exceeds the maximum step-limit,
which is one less than the value of

There is at best a loose connection between the counting of steps and
`with-prover-time-limit`. In particular, for a call of

The limit is relevant for every event, as well as for calls of `thm`
and `certify-book` — and more generally, to any form that creates
a ``summary context'' to print the usual event summary. The limit is
also put in force when entering the interactive proof-builder. A call
of

The limit applies to each event, not just ``atomic'' events. Consider the following example.

(set-prover-step-limit 500) (encapsulate () (defthm lemma-1 ; takes 380 steps (equal (append (append x y) z) (append x y z)) :rule-classes nil) (defthm lemma-2 ; would take 319 steps (equal (len (append x y)) (+ (len x) (len y))) :rule-classes nil))

The first `defthm` event,

Prover steps counted: 380 LEMMA-1

The second `defthm` event, `encapsulate` event.
Thus, when the number of steps would exceed 120, the proof of

ACL2 Error in STEP-LIMIT: The prover step-limit, which is 120 in the current context, has been exceeded. See :DOC set-prover-step-limit.

The summary for

Prover steps counted: More than 120

The summary for the `encapsulate` event then indicates that the
available steps for that event have also been exceeded:

Prover steps counted: More than 500

The discussion above applies to any event that contains other events, hence
applies similarly to `progn` events.

For those who use `make-event`, we note that prover steps in the
expansion phase similarly contribute to the total number of steps counted.
For example, suppose that the limit is 500 prover steps as above, and you
submit `events` (see embedded-event-form), such as calls of
`thm`. For example, a small built-in ACL2 test suite that includes
`thm` forms can be run by evaluating the form

ACL2 !>(make-event (er-progn (mini-proveall) (value '(value-triple nil)))) [[... output omitted here ...]] Summary Form: ( MAKE-EVENT (ER-PROGN ...)) Rules: NIL Warnings: Double-rewrite, Equiv, Subsume and Non-rec Time: 0.38 seconds (prove: 0.04, print: 0.29, other: 0.05) Prover steps counted: 41090 NIL ACL2 !>

- Last-prover-steps
- The number of prover steps most recently taken