Limit the number of steps for proofs

Logically, `set-prover-step-limit`, there is at
best a loose connection between the counting of steps and `with-prover-time-limit`.

The arguments of

Depending on the machine you are using, you may have less than a half-hour
of time before the number of prover steps exceeds the maximum limit on prover
steps that may be imposed, which is one less than the value of
`set-prover-step-limit`.

For examples of how step-limits work besides those presented below, see the
community book

For a utility that returns an indicator of the number of prover steps most recently taken, see last-prover-steps.

Note that

Examples: ; Limit (mini-proveall) to 100,000 prover steps (which happens to suffice) (with-prover-step-limit 100000 (mini-proveall)) ; Same as above for the inner call of with-prover-step-limit; so the ; mini-proveall call completes, but then we get an error because the second ; argument of the outer with-prover-step-limit call took more than 200 ; steps. (with-prover-step-limit 200 (with-prover-step-limit 100000 (mini-proveall))) ; Same as preceding form just above, except that this time there is no error, ; because the inner call of with-prover-step-limit has an extra argument ; of t inserted into the second argument position, which specifies that this ; entire inner call is treated as though it uses no prover steps. (with-prover-step-limit 200 (with-prover-step-limit 100000 t (mini-proveall))) ; The inner call limits (mini-proveall) to 200 prover steps, which fails ; almost immediately. (with-prover-step-limit 100000 (with-prover-step-limit 200 (mini-proveall))) ; Do not limit the number of prover steps, regardless of such a limit imposed ; globally or by the surrounding context. (with-prover-step-limit nil (mini-proveall)) ; Same as just above (indeed, nil above is converted to ; *default-step-limit*): (with-prover-step-limit *default-step-limit* (mini-proveall)) ; Advanced example: Limit the indicated theorem to 100 steps, and when the ; proof does not complete, then put down a label instead. (mv-let (erp val state) (with-prover-step-limit 100 (thm (equal (append (append x x) x) (append x x x)))) (if erp (deflabel foo :doc "Attempt failed.") (value (list :succeeded-with val)))) ; Use extra argument of t to avoid ``charging'' steps for the indicated ; form. (with-prover-step-limit 500 (encapsulate () (with-prover-step-limit 500 t ; Don't charge prover steps for this first defthm. (defthm test1 (equal (append x (append y z)) (append (append x y) z)) :rule-classes nil)) (defthm test2 (equal (append x (append y z)) (append (append x y) z)) :rule-classes nil))) General Forms: (with-prover-step-limit expr form) (with-prover-step-limit expr flg form)

where

If the value of

Finally we describe the optional extra Boolean argument, `progn` form is entered, and if `(with-prover-step-limit k form1')`. However, if `(with-prover-step-limit k t form1')`, then because of the
extra argument of

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