SET-GAG-MODE

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 val

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)

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.

Evaluation of 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 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

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 set-saved-output is disabled when gag-mode is active. Also note that calling set-gag-mode 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''.

We conclude with remarks 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 (@ checkpoint-processors); see @. Any or all of the symbols eliminate-destructors-clause, fertilize-clause, generalize-clause, or 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)))

See set-evisc-tuple, in particular the discussion there of :GAG-MODE, for how to influence slightly just what is printed in gag-mode.