Major Section: SWITCHES-PARAMETERS-AND-MODES
Examples: :set-gag-mode t ; enable gag-mode, suppressing most proof commentary (set-gag-mode t) ; same as above :set-gag-mode :goals ; same as above, but print names of goals when produced :set-gag-mode nil ; disable gag-mode General Forms: (set-gag-mode val) :set-gag-mode valwhere
valis one of
The basic idea of gag-mode is to avoid much of the verbose output from the theorem prover, leaving only output that is expected to be helpful. You are strongly encouraged to put the form
(set-gag-mode t) ; or, (set-gag-mode :goals)in your ACL2 customization file; see acl2-customization. The default value is
The basic idea of gag-mode is to focus attention on so-called ``key checkpoints''. By default, a checkpoint is a goal that cannot be simplified. (Below we discuss how to change this default.) A key checkpoint is a checkpoint that is not descended from another checkpoint. (Technical point: ``Descended'' signifies that both goals are at the top level in the same forcing round, or are in the same proof by induction.) Successful ACL2 users generally focus their attention on key checkpoints; for a discussion of how to use ACL2 prover output in an effective manner, see the-method, and see introduction-to-the-theorem-prover for a more detailed tutorial. In gag-mode, a key checkpoint is only displayed when ACL2 is unable to make any further progress on that goal or some descendent of it, other than with a proof by induction.
set-gag-mode t enters gag-mode, so that only key
checkpoints are printed. Evaluation of
set-gag-mode :goals also enters
gag-mode, but will additionally cause the name of a goal to be printed as
soon as it is generated (by invoking see set-print-clause-ids). The
:goals setting is useful for cases in which the prover spends very little
of its time generating goals to be proved by induction, yet you want to see
that it is making progress. For finer-grained feedback about the
simplifier's activity, see dmr.
The current value of gag-mode is returned by a macro of the same name:
(gag-mode) ; evaluates to t, nil, or :goals
(Remark for advanced users. The notion of ``checkpoint'' can be modified by
the user. The default, as discussed above, is for a checkpoint to be a goal
that cannot be simplified. Put differently, a checkpoint is acted on by one
of the processes in the value of the form
see @. Any or all of the symbols
eliminate-irrelevance-clause can be removed from this value in order that
invocation of the corresponding proof process does not cause its input goal
to be labeled a checkpoint. For example, if you do not want destructor
elimination to be treated differently from simplification for purposes of
labeling checkpoints, you can evaluate the following form (see assign):
(assign checkpoint-processors (remove 'eliminate-destructors-clause (@ checkpoint-processors)))Note that the value of
(@ checkpoint-processors)also affects the proof tree display; see proof-tree-details. End of Remark.)
An alternative to gag-mode is to use proof-trees; see proof-tree. With proof-trees it is not so important to avoid excessive prover output, since the proof-tree display provides structure that makes it easy to monitor proof attempts and navigate output for a proof that has failed or seems to be failing. Still, output can take time to print, so you may get better performance with gag-mode.
The intention of gag-mode is to show you only the parts of a proof attempt
that are relevant for debugging a failure; additional output is generally
more likely to be distracting than truly helpful. But on occasion you may
want to see the full proof output after an attempt made with gag-mode. If
so, then see pso and see pso!. Since
set-gag-mode takes responsibility
for the saving of output, related utility
disabled when gag-mode is active. Also note that calling
erases the currently saved output, if any.
You may notice that gag-mode tends to print relatively little information about goals pushed for proof by sub-induction -- i.e., a proof of *i.j, *i.j.k, etc. The principle here is that sub-inductions that do not succeed should generally be avoided, not analyzed for ways to make them succeed. Instead, the key checkpoint that generated the goal pushed for this induction is more appropriate to analyze. In general, the ``higher level'' the checkpoint, the more worthy it is of attention. Thus, we suggest that look at the top-level checkpoints before looking at those labeled ``Key checkpoints under a top-level induction''.