modify the nature of proof output
Major Section:  OTHER


:set-gag-mode t ; enable gag-mode (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

where val is one of t, nil, or :goals.

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. Future releases of ACL2 may install this setting as the default. Please contact the ACL2 implementors if you have suggestions for improving output in gag-mode.

The basic idea of gag-mode is to focus attention on so-called ``key checkpoints''. A key checkpoint is a goal that cannot be simplified, but is not descended from another such goal. (Technical point: ``Descended'' signifies the same proof by induction and forcing round). 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. In gag-mode, a key checkpoint is only displayed when ACL2 decides to push that goal, or a descendent of it, for an attempted proof by induction.

Normally you will probably want to use a value of t for set-gag-mode. However, you may find 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. The value :goals will cause the name of a goal to be printed as soon as it is generated (by invoking see set-print-clause-ids), in addition to the printing of key checkpoints -- the latter occurring, as described above, only when it or a subgoal is pushed for a proof by induction. 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) ; generally 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 (or the parent induction, if any) should be analyzed. In general, the ``higher level'' the checkpoint, the more worthy it is of attention. Thus, we suggest that before you look at the top-level checkpoints before looking at those labeled ``Key checkpoints under a top-level induction''.