Prove$
A way to call the prover from a program
For examples, see community book
books/tools/prove-dollar-tests.lisp.
General Form:
(prove$ term ; any term (translated or not)
&key
catch-hard-error ; default t
hints ; default nil
ignore-ok ; default t
instructions ; default nil
otf-flg ; default nil
prover-error-output-off ; default t
skip-proofs ; default :same
step-limit ; default nil
time-limit ; default nil
with-output) ; default (:off :all :on error :gag-mode nil)
where all arguments except with-output are evaluated. The value of
keyword :with-output, if supplied, should be a list containing arguments
one would give to the macro, with-output, hence a list that satisfies
keyword-value-listp. The hints, instructions, otf-flg, time-limit, and step-limit arguments are as one
would expect for calls of the prover; see defthm. It is illegal to
supply non-nil values for both hints and instructions. The
ignore-ok option has the same effect as if set-ignore-ok were
called with that same value, immediately preceding the call of prove$
— but of course warning and error messages may be suppressed, depending
on with-output. The skip-proofs option defaults to :same,
which causes prove$ to avoid proofs during include-book and, more
generally, any time that (ld-skip-proofsp state) is not nil. When
skip-proofs is not :same then proofs take place if and only if the
value of skip-proofs is not nil, as though (set-ld-skip-proofsp
state) were evaluated immediately preceding evaluation of the prove$
call. The value of prover-error-output-off must be either t, which
represents the list ("Failure" "Step-limit"), or a list of strings;
error messages arising during the proof whose type is one of these strings is
to be suppressed, as though set-inhibit-er had been executed on these
strings. Finally, the value of catch-hard-error is t by default,
which causes hard errors from the prover — in particular, when there is
a stack overflow in the rewriter — to be treated as ordinary proof
failures; also, it suppresses the general error message from a hard error and
it suppresses the error message from rewriter stack overflows.
Prove$ returns an error-triple, (mv erp val state). If
there is a syntax error (so-called ``translation error'') in the given term,
hints, or instructions, then erp is non-nil. Otherwise, erp is
nil and val is t when term is successfully proved, else
nil.
Note that after evaluation of a prove$ call, you can evaluate the form
(last-prover-steps state) to get the number of prover steps that were
taken — except, a negative number indicates a step-limit violation. See
last-prover-steps.
