Improved theory-invariant messages. Fixed :pe for define to show guar…

…ds and more. Added 3 symbols to *acl2-exports*. Cleaned up rtl :doc. Improved acl2-doc browser, dealing better with `:' and [n], and enhancing "i" command to count the matches.

Quoting :doc note-7-3 (the latter part of the change above (showing a
book) was J's idea):

  Warning and error messages produced upon [theory-invariant]
  violations now include additional explanation. Thanks to David
  Hardin and Grant Passmore for helpful remarks leading us to make
  this change. Those messages also now show where the theory
  invariant was defined: a book pathname, or ``top-level'' if
  directly in the loop.

The use of :pe on a form introduced by DEFINE now shows the guards
and, more generally, is more faithful to the actual form.  Thanks to
Eric Smith for pointing out that the guard was missing.

Added the following symbols to *acl2-exports*: ER-LET*,
SET-BAD-LISP-CONSP-MEMOIZE, and WITH-GUARD-CHECKING-EVENT.

Cleaned up rtl :doc warnings and tweaked links from the rtl pages to
David Russinoff's rtl manual.

Fixed acl2-doc to deal better with names containing the `:' character.
For example, clicking on child links Rtl::MASC:_The_Formal_Language
(from RTL::MODELING_ALGORITHMS_IN_SYSTEMC_AND_ACL2) and
Gl::6._Writing_:g-bindings_forms (GL::BASIC-TUTORIAL) had failed.
That change has been mentioned by expanding an existing release note
(sub-)item, but here are two new (sub-) items (quoting :doc note-7-3):

    * Text in square brackets, for example [1], is no longer recognized as
      a link (though Emacs still highlights it). Thanks to Mihir
      Mehta for pointing out this issue.

    * In the [ACL2-doc] browser, when the ``i'' (acl2-doc-index) command is
      invoked without a prefix argument, the mode line shows the
      number of matches. (The remaining matches continue to be
      accessible using the ``,'' (acl2-doc-index-next) command.)

books/misc/check-acl2-exports.lisp

@@ -89,7 +89,6 @@
     COUNT ; defined in books/coi/bags/basic.lisp
     DEFUN-MODE
     DIVE-INTO-MACROS-TABLE
-    ER-LET* ; should add to *acl2-exports*
     ERROR1
     FIND-RULES-OF-RUNE
     LOOP-STOPPER
@@ -106,10 +105,8 @@
     REMOVE-DIVE-INTO-MACRO
     REWRITE
     SAFE-MODE
-    SET-BAD-LISP-CONSP-MEMOIZE ; should add to *acl2-exports*
     TYPE-SET
     WATERFALL
-    WITH-GUARD-CHECKING-EVENT ; should add to *acl2-exports*
 
 ; Some of the following might be added to *acl2-exports*, but perhaps not; they
 ; come from defpointers to system-utilities.

books/rtl/rel11/lib/doc.lisp

@@ -52,18 +52,26 @@
       |Odd Rounding|
       |IEEE Rounding|
       |Denormal Rounding|))
-     (|Floating-Point Exceptions and Specification of x86 Elementary Arithmetic Instructions| ; exps.lisp
+     (|Floating-Point Exceptions and Specification of x86 Elementary Arithmetic Instructions| ; excps.lisp
+      (|IEEE-Compliant Square Root| ; sqrt.lisp
+       |Truncation {Square Root}|
+       |Odd Rounding {Square Root}|
+       |IEEE Rounding {Square Root}|)
       (|SSE Floating-Point Instructions|
-       |The SSE Control and Status Register|
-       |Overview of SSE Floating-Point Exceptions|
-       |SSE Pre-Computation Exceptions|
-       |SSE Post-Computation Exceptions|)
+; None of the following seems to be present in this directory.
+       ;; |The SSE Control and Status Register|
+       ;; |Overview of SSE Floating-Point Exceptions|
+       ;; |SSE Pre-Computation Exceptions|
+       ;; |SSE Post-Computation Exceptions|
+       )
       (|x87 Instructions|
-       |x87 Control Word|
-       |x87 Status Word|
-       |Overview of x87 Exceptions|
-       |x87 Pre-Computation Exceptions|
-       |x87 Post-Computation Exceptions|))
+; None of the following seems to be present in this directory.
+       ;; |x87 Control Word|
+       ;; |x87 Status Word|
+       ;; |Overview of x87 Exceptions|
+       ;; |x87 Pre-Computation Exceptions|
+       ;; |x87 Post-Computation Exceptions|
+       ))
     (|Implementation of Elementary Operations|
      (|Addition| ; add.lisp
       |Bit Vector Addition|
@@ -81,22 +89,22 @@
      (|SRT Division and Square Root| ; srt.lisp
       |SRT Division and Quotient Digit Selection|
       |SRT Square Root Extraction|
-      |Square Root Seed Tables|)
-     (|IEEE-Compliant Square Root| ; sqrt.lisp
-      |Truncation {Square Root}|
-      |Odd Rounding {Square Root}|
-      |IEEE Rounding {Square Root}|))
+      |Square Root Seed Tables|))
     (|Modeling Algorithms in SystemC and ACL2| ; masc.lisp
      (|MASC: The Formal Language|
       |Language Overview|
       |Arithmetic|
-      |Control Restrictions|
-      |Mapping SystemC to MASC|
-      |Mapping MASC to ACL2|)
+; None of the following seems to be present in this directory.
+      ;; |Control Restrictions|
+      ;; |Mapping SystemC to MASC|
+      ;; |Mapping MASC to ACL2|
+      )
      (|Applications|
-      |Integer Multiplication|
-      |Vector Compression|
-      |Fused Multiply-Accumulate|))
+; None of the following seems to be present in this directory.
+      ;; |Integer Multiplication|
+      ;; |Vector Compression|
+      ;; |Fused Multiply-Accumulate|
+      ))
     |Bibliography|))
 
 (defun rtl-node-name-basic (sym)
@@ -182,16 +190,27 @@
           name)))
 
 (defmacro defsection-rtl (name parent &rest events)
+
+; Formerly we linked each specific section in the ACL2 manual to the
+; corresponding section in Russinoff's manual.  However, these have not stayed
+; in perfect sync, so we no longer try to maintain that correspondence.
+; Fortunately, it's not really necessary, since Russinoff's top page has a
+; complete Table of Contents.
+
   (let* ((entry (rtl-node-entry name))
          (section-name (cadr entry))
-         (url (caddr entry)))
+         ;;(url (caddr entry))
+         (url "http://russinoff.com/libman/top.html")
+         )
     `(defsection ,section-name
        :parents (,(if (eq parent 'rtl) 'rtl (cadr (rtl-node-entry parent))))
        :short ,(symbol-name name)
        :long ,(concatenate 'string
-                           "<p>See also <a href='" url "'>"
+                           "<p>See also "
                            "the corresponding section in David Russinoff's "
-                           "online rtl manual</a>.</p>"
+                           "<a href='"
+                           url
+                           "'>online rtl manual</a>.</p>"
                            (defsection-rtl-defs events))
        (deflabel ,(intern-in-package-of-symbol
                    (concatenate 'string (symbol-name name) "$SECTION")

books/std/util/define.lisp

@@ -1072,6 +1072,28 @@ examples.</p>")
            (cdar kwd-alist)
            (convert-kwd-alist-back-into-plist (cdr kwd-alist)))))
 
+(defun pe-entry-args (args returnspecs)
+  (declare (xargs :guard (true-listp args)))
+  (cond ((endp args) nil)
+        ((and (eq (car args) :long)
+              (cdr args))
+         (list* :long "Documentation is available via :doc."
+                (pe-entry-args (cddr args) returnspecs)))
+        ((and (eq (car args) :prepwork)
+              (cdr args))
+         (list* :prepwork "<event list elided>"
+                (pe-entry-args (cddr args) returnspecs)))
+        ((and (eq (car args) :returns)
+              (cdr args)
+              (consp returnspecs))
+         (list* :returns
+                (prettify-returnspecs-for-pe returnspecs)
+                (pe-entry-args (cddr args) returnspecs)))
+        ((eq (car args) '///)
+         (list '/// "<events elided>"))
+        (t (cons (car args)
+                 (pe-entry-args (cdr args) returnspecs)))))
+
 (defun parse-define
   (name            ; User-level name, e.g., FOO
    args            ; Everything that comes after the name
@@ -1163,29 +1185,7 @@ examples.</p>")
 
        (returnspecs   (parse-returnspecs name returns world))
 
-       (pe-entry
-        `(define ,name ,raw-formals
-           ;; Documentation string, if simple enough...
-           ,@(b* ((short (cdr (assoc :short kwd-alist)))
-                  ((when (stringp short))
-                   `(:short ,short))
-                  ((when (or short (cdr (assoc :long kwd-alist))))
-                   ;; There's documentation but it's too complex to print nicely
-                   ;; right now, let's just tell the user there's docs available.
-                   `("Documentation is available via :doc.")))
-               ;; No documentation, skip this part.
-               nil)
-           ;; Returnspecs, cleaned up to remove hint stuff
-           ,@(and (consp returnspecs)
-                  (list :returns (prettify-returnspecs-for-pe returnspecs)))
-           ;; We also don't want to see other ugly proof-related things like
-           ;; :hints and :guard-debug and stuff like that, so keep only the
-           ;; things that seem most valuable/short.
-           ,@(convert-kwd-alist-back-into-plist
-              (keep-assocs '(:inline :non-executable :well-founded-relation :measure)
-                           kwd-alist))
-           ,@traditional-decls/docs
-           ,body))
+       (pe-entry (list* 'define name (pe-entry-args args returnspecs)))
 
        (guard-verification-will-happen-anyway-p
         ;; Design decision: define will ignore set-verify-guards-eagerness 1

books/system/doc/acl2-doc.lisp

@@ -74444,6 +74444,12 @@ it."
  acl2-pc::s).  Thanks to Eric Smith for requests that led us to make this
  change.</p>
 
+ <p>Warning and error messages produced upon @(tsee theory-invariant)
+ violations now include additional explanation.  Thanks to David Hardin and
+ Grant Passmore for helpful remarks leading us to make this change.  Those
+ messages also now show where the theory invariant was defined: a book
+ pathname, or ``top-level'' if directly in the loop.</p>
+
  <h3>New Features</h3>
 
  <p>New optional arguments allow the @(tsee pso) utility to restrict output to
@@ -74951,7 +74957,13 @@ it."
 
  <li>Links are inserted much more reliably.  That is, the surrounding of text
  by square brackets for text-based display now virtually always creates links
- that can be followed to topics in the @(see acl2-doc) browser.</li>
+ that can be followed to topics in the @(see acl2-doc) browser.  In particular,
+ that browser now handles names properly that contain the @(':')
+ character.</li>
+
+ <li>Text in square brackets, for example [1], is no longer recognized as a
+ link (though Emacs still highlights it).  Thanks to Mihir Mehta for pointing
+ out this issue.</li>
 
  <li>Automatic insertion of links for expressions <tt>@@('(name ...)')</tt>, as
  <tt>@@('([name] ...)')</tt>, should not happen for text-based display.  This
@@ -74969,6 +74981,11 @@ it."
  behavior to other tags (see @('xdoc-tag-elide-alist') in @(see
  community-books) file 'books/xdoc/display.lisp').</li>
 
+ <li>In the @(see acl2-doc) browser, when the ``i'' (@('acl2-doc-index'))
+ command is invoked without a prefix argument, the mode line shows the number
+ of matches.  (The remaining matches continue to be accessible using the ``,''
+ @('(acl2-doc-index-next)') command.)</li>
+
  </ul>
 
  <p>Incorporated changes to @('emacs/emacs-acl2.el') put forward by Keshav

defpkgs.lisp

@@ -244,7 +244,7 @@
         EQLABLE-LISTP
         EQLABLE-LISTP-FORWARD-TO-ATOM-LISTP
         EQLABLEP EQLABLEP-RECOG EQUAL
-        EQUAL-CHAR-CODE ER ER-PROGN ER-PROGN-FN
+        EQUAL-CHAR-CODE ER ER-LET* ER-PROGN ER-PROGN-FN
         ER-PROGN-FN@PAR ER-PROGN@PAR
         EVENP EVENS EVENT EVISC-TUPLE
         EXECUTABLE-COUNTERPART-THEORY
@@ -466,7 +466,7 @@
         SEARCH SECOND
         SERIALIZE-READ SERIALIZE-WRITE SET-ABSSTOBJ-DEBUG
         SET-ACCUMULATED-PERSISTENCE
-        SET-BACKCHAIN-LIMIT
+        SET-BACKCHAIN-LIMIT SET-BAD-LISP-CONSP-MEMOIZE
         SET-BODY SET-BOGUS-DEFUN-HINTS-OK SET-BOGUS-MEASURE-OK
         SET-BOGUS-MUTUAL-RECURSION-OK
         SET-CASE-SPLIT-LIMITATIONS
@@ -631,6 +631,7 @@
         WARNING! WATERFALL-PARALLELISM WATERFALL-PRINTING
         WET WITH-FAST-ALIST
         WITH-GUARD-CHECKING WITH-GUARD-CHECKING-ERROR-TRIPLE
+        WITH-GUARD-CHECKING-EVENT
         WITH-LIVE-STATE WITH-LOCAL-STATE WITH-LOCAL-STOBJ WITH-OUTPUT
         WITH-OUTPUT-LOCK
         WITH-PROVER-STEP-LIMIT WITH-PROVER-STEP-LIMIT!

doc.lisp

@@ -77,7 +77,7 @@ Subtopics
   [defthm], [in-theory], [xargs], [state], etc., without an acl2::
   prefix.
 
-  The constant *acl2-exports* lists 1402 symbols, including most
+  The constant *acl2-exports* lists 1405 symbols, including most
   documented ACL2 system constants, functions, and macros. You will
   typically also want to import many symbols from Common Lisp; see
   [*common-lisp-symbols-from-main-lisp-package*].
@@ -270,8 +270,8 @@ Subtopics
        eqlable-alistp-forward-to-alistp
        eqlable-listp
        eqlable-listp-forward-to-atom-listp
-       eqlablep eqlablep-recog
-       equal equal-char-code er er-progn
+       eqlablep eqlablep-recog equal
+       equal-char-code er er-let* er-progn
        er-progn-fn er-progn-fn@par er-progn@par
        evenp evens event evisc-tuple
        executable-counterpart-theory
@@ -517,6 +517,7 @@ Subtopics
        serialize-write set-absstobj-debug
        set-accumulated-persistence
        set-backchain-limit
+       set-bad-lisp-consp-memoize
        set-body set-bogus-defun-hints-ok
        set-bogus-measure-ok
        set-bogus-mutual-recursion-ok
@@ -697,6 +698,7 @@ Subtopics
        waterfall-parallelism waterfall-printing
        wet with-fast-alist with-guard-checking
        with-guard-checking-error-triple
+       with-guard-checking-event
        with-live-state with-local-state
        with-local-stobj with-output
        with-output-lock with-prover-step-limit
@@ -73099,6 +73101,13 @@ Changes to Existing Features
   [ACL2-pc::s]. Thanks to Eric Smith for requests that led us to make
   this change.
 
+  Warning and error messages produced upon [theory-invariant]
+  violations now include additional explanation. Thanks to David
+  Hardin and Grant Passmore for helpful remarks leading us to make
+  this change. Those messages also now show where the theory
+  invariant was defined: a book pathname, or ``top-level'' if
+  directly in the loop.
+
 
 New Features
 
@@ -73604,7 +73613,11 @@ EMACS Support
     * Links are inserted much more reliably. That is, the surrounding of
       text by square brackets for text-based display now virtually
       always creates links that can be followed to topics in the
-      [ACL2-doc] browser.
+      [ACL2-doc] browser. In particular, that browser now handles
+      names properly that contain the : character.
+    * Text in square brackets, for example [1], is no longer recognized as
+      a link (though Emacs still highlights it). Thanks to Mihir
+      Mehta for pointing out this issue.
     * Automatic insertion of links for expressions @('(name ...)'), as
       @('([name] ...)'), should not happen for text-based display.
       This was however done when generating short strings for
@@ -73617,6 +73630,10 @@ EMACS Support
       display}''. A general mechanism is in place for extending this
       behavior to other tags (see xdoc-tag-elide-alist in
       [community-books] file 'books/xdoc/display.lisp').
+    * In the [ACL2-doc] browser, when the ``i'' (acl2-doc-index) command is
+      invoked without a prefix argument, the mode line shows the
+      number of matches. (The remaining matches continue to be
+      accessible using the ``,'' (acl2-doc-index-next) command.)
 
   Incorporated changes to emacs/emacs-acl2.el put forward by Keshav
   Kini (thanks!), as follows.