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
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. 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
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,
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
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 (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''.