Ld-skip-proofsp
How carefully ACL2 processes your commands
Examples:
ACL2 !>(set-ld-skip-proofsp t state)
T
ACL2 !s>(set-ld-skip-proofsp nil state)
NIL
ACL2 !>(set-ld-skip-proofsp 'include-book state)
INCLUDE-BOOK
ACL2 !s>
A global variable in the ACL2 state, called 'ld-skip-proofsp,
determines the thoroughness with which ACL2 processes your commands.
This variable may take on one of three values: t, nil or
'include-book. When ld-skip-proofsp is non-nil, the
system skips all proofs, which of course can render the system unsound. The
form (set-ld-skip-proofsp flg state) is the general-purpose way of
setting ld-skip-proofsp. This global variable is an ``ld
special,'' which is to say, you may call ld in such a way as to
``bind'' this variable for the dynamic extent of the ld.
When ld-skip-proofsp is non-nil, the default prompt
displays the character s. Thus, the prompt
ACL2 !s>
means that the default defun-mode is :logic (otherwise
the character p, for :program, would also be printed; see
default-print-prompt) but ``proofs are being skipped.''
Observe that there are two legal non-nil values, t and
'include-book. When ld-skip-proofsp is t, ACL2 skips
all proof obligations but otherwise performs all other required analysis of
input events. When ld-skip-proofsp is 'include-book,
ACL2 skips not only proof obligations but all analysis except that required to
compute the effect of successfully executed events. To explain the
distinction, let us consider one particular event, say a defun. Very
roughly speaking, a defun event normally involves a check of the
syntactic well-formedness of the submitted definition, the generation and
proof of the termination conditions, and the computation and storage of
various rules such as a :definition rule and some :type-prescription rules. By ``normally'' above we mean when
ld-skip-proofsp is nil. How does a defun behave when
ld-skip-proofsp is non-nil?
If ld-skip-proofsp is t, then defun performs the
syntactic well-formedness checks and computes and stores the various rules,
but it does not actually carry out the termination proofs. If
ld-skip-proofsp is 'include-book, defun does not do
the syntactic well-formedness check nor does it carry out the termination
proof. Instead, it merely computes and stores the rules under the assumption
that the checks and proofs would all succeed. Observe that a setting of
'include-book is ``stronger'' than a setting of t in the
sense that 'include-book causes defun to assume even more
about the admissibility of the event than t does.
As one might infer from the choice of name, the include-book event
sets ld-skip-proofsp to 'include-book when processing the
events in a book being loaded. Thus, include-book does the
minimal work necessary to carry out the effects of every event in the book.
The syntactic checks and proof obligations were, presumably, successfully
carried out when the book was certified.
A non-nil value for ld-skip-proofsp also affects the system's
output messages. Event summaries (the paragraphs that begin ``Summary'' and display the event forms, rules used, etc.) are not printed when
ld-skip-proofsp is non-nil. Warnings and observations are printed
when ld-skip-proofsp is t but are not printed when it is
'include-book.
Intuitively, ld-skip-proofsp t means skip just the proofs and
otherwise do all the work normally required for an event; while
ld-skip-proofsp 'include-book is ``stronger'' and means do
as little as possible to process events. In accordance with this
intuition, local events are processed when ld-skip-proofsp
is t but are skipped when ld-skip-proofsp is 'include-book.
The ACL2 system itself uses only two settings, nil and 'include-book, the latter being used only when executing the events
inside of a book being included. The ld-skip-proofsp setting of t
is provided as a convenience to the user. For example, suppose one has a file
of events. By loading it with ld with ld-skip-proofsp set
to t, the events can all be checked for syntactic correctness and
assumed without proof. This is a convenient way to recover a state lost by a
system crash or to experiment with a modification of an events
file.
The foregoing discussion is actually based on a lie. ld-skip-proofsp
is allowed two other values, 'initialize-acl2 and
'include-book-with-locals. The first causes behavior similar to t
but skips local events and avoids some error checks that would
otherwise prevent ACL2 from properly booting. The second is identical to
'include-book but also executes local events.
These additional values are not intended for use by the user, but no barriers
to their use have been erected.
User-defined tools may temporarily modify the global setting of
ld-skip-proofsp; for example, see remove-hyps.
We close by reminding the user that ACL2 is potentially unsound if
ld-skip-proofsp is set by the user. Indeed, direct setting of
ld-skip-proofsp is illegal within a book (except during make-event expansion). We provide access to it simply to allow
experimentation and rapid reconstruction of lost or modified logical worlds.
