Major Section: MISCELLANEOUS
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 assumes
that which ought to be proved and is thus 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
miminal 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.
We close by reminding the user that ACL2 is potentially unsound if
ld-skip-proofsp is ever set by the user. We provide access to it
simply to allow experimentation and rapid reconstruction of lost or
modified logical worlds.
