LD-SKIP-PROOFSP

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>

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.