Tweaked code by removing an obsolete case, and added discussion of linear to :doc force. Added a way to set gag-mode to nil for regressions.

Quoting a comment added to (defxdoc note-8-4 ...):

; Cleaned up source function tilde-@-assumnotes-phrase-lst-gag-mode by removing
; an obsolete case having to do with forcing guards.  We noticed this case as
; we added to :doc force to explain forcing by linearization (thanks to Mihir
; Mehta for a query leading to that :doc improvement).

Since the code change is relevant to output, this time I ran an
"everything" regression with both

INHIBIT='(set-inhibit-output-lst (list (quote proof-tree)))'

and, to set gag-mode to nil,

ACL2_CUSTOMIZATION=`pwd`/acl2-customization-files/set-gag-mode-nil.lisp

-- and to support that, I added
acl2-customization-files/set-gag-mode-nil.lisp to the git repository.

I also ran :mini-proveall as a quick check that I didn't break normal
output (hard to imagine, with my tiny change).

Author: MattKaufmann

acl2-customization-files/set-gag-mode-nil.lisp

@@ -0,0 +1 @@
+#!acl2(set-gag-mode nil)

books/centaur/esim/tutorial/cert.acl2

@@ -37,3 +37,11 @@
 (include-book "centaur/esim/portcullis" :dir :system)
 (include-book "centaur/aig/portcullis" :dir :system)
 ; cert-flags: ? t :ttags :all
+
+; Matt K. mod: If proof output is enabled and gag-mode is off, then turn on
+; gag-mode (might as well use the default of :goals) to avoid printing huge
+; object.  This happened 5/11/2020 when attempting to certify boothmul.lisp.
+(if (and (not (member-eq 'prove (f-get-global 'inhibit-output-lst state)))
+         (null (gag-mode)))
+    (set-gag-mode :goals)
+  state)

books/demos/mini-proveall-input.lsp

@@ -5,4 +5,6 @@
 ; Here is a quick test that we sometimes run.  To see what it generates,
 ; evaluate (trans1 '(mini-proveall)).
 
+(set-gag-mode :goals)
+
 (mini-proveall)

books/demos/mini-proveall-log.txt

@@ -7,6 +7,8 @@ ACL2 !>>(SET-INHIBITED-SUMMARY-TYPES '(TIME STEPS))
  (TIME STEPS)
 ACL2 !>>(SET-INHIBIT-OUTPUT-LST '(PROOF-TREE))
  (PROOF-TREE)
+ACL2 !>>(SET-GAG-MODE :GOALS)
+<state>
 ACL2 !>>(MINI-PROVEALL)
 ACL2 !>>>:LOGIC
 

books/projects/paco/books/proveall-input.lsp

@@ -3,6 +3,8 @@
 (include-book "../paco")
 (in-package "PACO")
 
+(acl2::set-gag-mode :goals)
+
 (acl2::table acl2::theory-invariant-table nil nil :clear)
 
 (ACL2::SET-MATCH-FREE-ERROR NIL)

books/projects/paco/books/proveall-log.txt

@@ -15,6 +15,8 @@ Rules: NIL
  "../paco.lisp"
 ACL2 !>>(IN-PACKAGE "PACO")
  "PACO"
+PACO !>>(ACL2::SET-GAG-MODE :GOALS)
+<state>
 PACO !>>(ACL2::TABLE ACL2::THEORY-INVARIANT-TABLE
                      NIL NIL :CLEAR)
 

books/system/doc/acl2-doc.lisp

@@ -32116,6 +32116,40 @@ current fast alists."
  this happen?  The type system ``punted'' the forced hypothesis to the
  rewriter, which established it.</p>
 
+ <p>The discussion above may give the impression that a forcing round only
+ takes place because of a failure to relieve a forced hypothesis.  A notable
+ exception, however, is due to @(see linear-arithmetic).  Consider the
+ following example:</p>
+
+ @({
+ (implies (not (equal 0 x))
+          (or (< 0 x) (< x 0)))
+ })
+
+ <p>This is not a theorem; in particular, it fails when @('x') is @('nil').
+ What is missing is the hypothesis, @('(acl2-numberp x)').  If you try to prove
+ the displayed formula above and you look at the proof using @(':')@(tsee pso),
+ you'll see the following.</p>
+
+ @({
+ But forced simplification reduces this to T, using the :executable-
+ counterpart of FORCE and linear arithmetic.
+ })
+
+ <p>Thus, no specific rule created this forcing round (see also @(see
+ forcing-round)).  Rather, ACL2 was able to prove the goal using linear
+ arithmetic, but it needed to force the assumption that @('x') is a number.
+ This is clear when we look at output for the forcing round:</p>
+
+ @({
+ [1]Goal, below, will focus on
+ (ACL2-NUMBERP X),
+ which was forced in
+  Goal'
+   by the linearization of
+   (EQUAL 0 X).
+ })
+
  <p>Finally, we should mention that the rewriter is never willing to force when
  there is an @(tsee if) term present in the goal being simplified.  Since
  @(tsee and) terms and @(tsee or) terms are merely abbreviations for @(tsee if)
@@ -86156,6 +86190,11 @@ it."
 ; led to this improvement.  Also avoided a raw Lisp error for EQUIV when the
 ; alleged equivalence relation is supplied as an atom that is not a symbol.
 
+; Cleaned up source function tilde-@-assumnotes-phrase-lst-gag-mode by removing
+; an obsolete case having to do with forcing guards.  We noticed this case as
+; we added to :doc force to explain forcing by linearization (thanks to Mihir
+; Mehta for a query leading to that :doc improvement).
+
   :parents (release-notes)
   :short "ACL2 Version  8.4 (xxx, 20xx) Notes"
   :long "<p>NOTE!  New users can ignore these release notes, because the @(see

doc.lisp

@@ -35606,6 +35606,35 @@ Subtopics
   ``punted'' the forced hypothesis to the rewriter, which established
   it.
 
+  The discussion above may give the impression that a forcing round
+  only takes place because of a failure to relieve a forced
+  hypothesis.  A notable exception, however, is due to
+  [linear-arithmetic].  Consider the following example:
+
+    (implies (not (equal 0 x))
+             (or (< 0 x) (< x 0)))
+
+  This is not a theorem; in particular, it fails when x is nil.  What
+  is missing is the hypothesis, (acl2-numberp x).  If you try to
+  prove the displayed formula above and you look at the proof using
+  :[pso], you'll see the following.
+
+    But forced simplification reduces this to T, using the :executable-
+    counterpart of FORCE and linear arithmetic.
+
+  Thus, no specific rule created this forcing round (see also
+  [forcing-round]).  Rather, ACL2 was able to prove the goal using
+  linear arithmetic, but it needed to force the assumption that x is
+  a number.  This is clear when we look at output for the forcing
+  round:
+
+    [1]Goal, below, will focus on
+    (ACL2-NUMBERP X),
+    which was forced in
+     Goal'
+      by the linearization of
+      (EQUAL 0 X).
+
   Finally, we should mention that the rewriter is never willing to
   force when there is an [if] term present in the goal being
   simplified.  Since [and] terms and [or] terms are merely

doc/acl2-code-size.txt

@@ -1,14 +1,14 @@
 Source files (not including doc.lisp):
 ------------------------------------
   CODE LINES:
-  143024 lines,   6366699 characters
+  143021 lines,   6366396 characters
   COMMENT LINES:
    80139 lines,   4827139 characters
   BLANK LINES:
    33611 lines,     33611 characters
   TOTAL:
-  256774 lines,  11227449 characters
+  256771 lines,  11227146 characters
 ------------------------------------
 Documentation (file books/system/doc/acl2-doc.lisp):
-  130174 lines,   5750050 characters
+  130213 lines,   5751468 characters
 ------------------------------------

doc/home-page.html

@@ -152,7 +152,7 @@
 <center>
 <b><a href="mailto:[email protected]">Matt Kaufmann</a> and <a href="mailto:[email protected]">J Strother Moore</a></b><br>
 <a href="http://www.utexas.edu">University of Texas at Austin</a><br>
-May 8, 2020
+May 11, 2020
 </center>
 
 <p>

prove.lisp

@@ -8951,24 +8951,21 @@
        (let* ((cl-id-phrase
                (tilde-@-clause-id-phrase
                 (access assumnote (car lst) :cl-id)))
+              (rune (access assumnote (car lst) :rune))
               (x
-               (cond ((and (consp (access assumnote (car lst) :rune))
-                           (null (base-symbol (access assumnote (car lst)
-                                                      :rune))))
+               (cond ((and (consp rune)
+                           (null (base-symbol rune)))
                       (list " ~@0 by primitive type reasoning"
                             (cons #\0 cl-id-phrase)))
-                     ((eq (access assumnote (car lst) :rune) 'equal)
+                     ((eq rune 'equal)
                       (list " ~@0 by linearization"
                             (cons #\0 cl-id-phrase)))
-                     ((symbolp (access assumnote (car lst) :rune))
-                      (list " ~@0 by assuming the guard for ~x1"
-                            (cons #\0 cl-id-phrase)
-                            (cons #\1 (access assumnote (car lst) :rune))))
                      (t
-                      (list " ~@0 by applying ~x1"
-                            (cons #\0 cl-id-phrase)
-                            (cons #\1 (access assumnote (car lst)
-                                              :rune)))))))
+                      (assert$ ; Check that we no longer assume a guard.
+                       (not (symbolp rune))
+                       (list " ~@0 by applying ~x1"
+                             (cons #\0 cl-id-phrase)
+                             (cons #\1 rune)))))))
          (add-to-set-equal x acc))))))
 
 (defun tilde-*-assumnotes-column-phrase-gag-mode (assumnotes)