|
|
|---|
|
|
|
|---|
Modify the nature of proof output
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
where
By default, gag-mode is enabled, set to
(gag-mode) ; evaluates to 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. The first two forms below set gag-mode on, while the other turns it off; these may be placed in your ACL2 customization file; see ACL2-customization.
(set-gag-mode :goals) ; (default) avoid most prover output; show goal names (set-gag-mode t) ; avoid most prover output; also, hide goal names (set-gag-mode nil) ; allow prover output
Gag-mode focuses 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, or less often, induction schemes. (To suppress or abbreviate
induction schemes in gag-mode, see set-evisc-tuple, specifically, the
discussion of
Evaluation of
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. This can be done provided proof output is not inhibited (see set-inhibit-output-lst) during the proof attempt; see pso and see pso!.
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. That feature emphasizes that unsuccessful sub-inductions 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, it might be helpful to 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
(assign checkpoint-processors (remove 'eliminate-destructors-clause (@ checkpoint-processors)))
Note that the value of
See set-evisc-tuple, in particular the discussion there of