Added NUMBER as a type-spec. On proof failure, suggest including appl…

…y$ book when appropriate. Introduce len$ macro and use it in definition of pseudo-termp. Fix wormhole bug. Changed names: er-soft-off-p and er-soft-off-p1 to er-off-p and er-off-p1, resp. Use *base-10-chars* in warning$-cw1. Eliminated a call of warning$-cw in books/xdoc/display.lisp.

Quoting :DOC note-8-6:

  The symbol, number, is now a legal [type-spec].

  When an event fails, then if it involves definition [rune]s for
  [loop$] [scion]s, the failure message may suggest including the
  book projects/apply/top if it hasn't already been included.  That
  book provides quite a few lemmas about [loop$] scions.

  Replaced [length] calls in the defun of [pseudo-termp] with calls of
  a new macro, len$, which is a call of [mbe] that invokes [length]
  in the :exec code and [len] in the :logic code.  Thanks to Eric
  Smith for requesting such an enhancement, and for discussing
  specifics of it, so as to avoid the need for at least one
  unfortunate rule that if (pseudo-termp term) then (not (stringp
  (cdr term))), apparently needed because length behaves specially on
  strings.

  Fixed a bug that was causing calls of [wormhole] to signal an error.

Quoting comments in (defxdoc note-8-6 ...):

; Changed er-soft-off-p[1] to er-off-p[1]: just a name change, since this is
; about hard errors too, not just soft errors.

Other changes:

- Use *base-10-chars* in warning$-cw1.

- Eliminated call of warning$-cw (deprecated) in the definition of
  warn-on-missing-topic-names in books/xdoc/display.lisp.

Successfully ran "make devel-check" and "make proofs" in addition to
the usual regression-everything.

acl2-fns.lisp

@@ -1745,6 +1745,10 @@ notation causes an error and (b) the use of ,. is not permitted."
   #-cltl2 x)
 
 (defmacro safe-open (filename &rest args &key direction &allow-other-keys)
+
+; Note that this macro has the same default :element-type (i.e., character) as
+; open.
+
   (assert (member direction ; might later support :io and :probe
                   '(:input :output)
                   :test #'eq))

axioms.lisp

@@ -8162,6 +8162,30 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
 
 ; Now we define the weak notion of term that guards metafunctions.
 
+(defmacro len$ (x)
+
+; This variant of len is logically just len, but it executes as length in
+; guard-verified and program-mode code.  In such code it should thus be called
+; only when x is a true list, but it may be slightly faster than len because
+; the Lisp implementation may optimize the definition of length.  The following
+; experiment (performed on an Intel-based Mac) showed length to be faster than
+; len in CCL and perhaps about the same in SBCL.
+
+; :q ; go into raw Lisp
+; (defconstant *c* (loop for i from 1 to 1000 by 10
+;                        collect (make-list (* 1000 i))))
+; (defun f () (loop for x in *c* when (= (len x) 3) collect x))
+; (defun g () (loop for x in *c* when (= (length x) 3) collect x))
+; (time (f))
+; (time (g))
+
+; At first glance it may appear that x is being evaluated twice below from a
+; call of len$.  But in fact, only the :logic or the :exec code will be
+; evaluated from a call of len$.
+
+  `(mbe :logic (len ,x)
+        :exec (length ,x)))
+
 (mutual-recursion
 
 (defun pseudo-termp (x)
@@ -8181,12 +8205,12 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
 ; the checks below.
 
                (and (true-listp (car x))
-                    (equal (length (car x)) 3)
+                    (equal (len$ (car x)) 3)
                     (eq (car (car x)) 'lambda)
                     (symbol-listp (cadr (car x)))
                     (pseudo-termp (caddr (car x)))
-                    (equal (length (cadr (car x)))
-                           (length (cdr x))))))))
+                    (equal (len$ (cadr (car x)))
+                           (len$ (cdr x))))))))
 
 (defun pseudo-term-listp (lst)
   (declare (xargs :guard t))
@@ -11570,6 +11594,7 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
         ((eq x 'rational) (list 'rationalp var))
         ((eq x 'real) (list 'real/rationalp var))
         ((eq x 'complex) (list 'complex/complex-rationalp var))
+        ((eq x 'number) (list 'acl2-numberp var))
         ((and (consp x)
               (eq (car x) 'rational)
               (true-listp x)
@@ -18271,6 +18296,13 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
                    (case
                      typ
                      ((:character :object)
+
+; We allow the :element-type to default to character in the following call of
+; safe-open.  That may seem surprising when typ is :object.  But read-object
+; calls read, and the CL HyperSpec doesn't impose any requirements on the
+; stream when calling read.  So we prefer to leave :element-type as the
+; default.
+
                       (safe-open os-file-name :direction :input
                                  :if-does-not-exist nil))
                      (:byte (safe-open os-file-name :direction :input
@@ -18464,16 +18496,24 @@ evaluated.  See :DOC certify-book, in particular, the discussion about ``Step
                       ((:character :object)
                        (cond ((eq file-name :string)
                               (make-string-output-stream))
-                             (t (safe-open os-file-name :direction :output
-                                           :if-exists :supersede
+                             (t
+
+; We allow the :element-type to default to character in the following call of
+; safe-open.  That may seem surprising when typ is :object.  But read-object
+; calls read, and the CL HyperSpec doesn't impose any requirements on the
+; stream when calling read.  So we prefer to leave :element-type as the
+; default.
+
+                              (safe-open os-file-name :direction :output
+                                         :if-exists :supersede
 
 ; In ACL2(p) using CCL, we have seen an error caused when standard-co was
 ; connected to a file.  Specifically, waterfall-print-clause-id@par was
 ; printing to standard-co -- i.e., to that file -- and CCL complained because
 ; the default is for a file stream to be private to the thread that created it.
 
-                                           #+(and acl2-par ccl) :sharing
-                                           #+(and acl2-par ccl) :lock))))
+                                         #+(and acl2-par ccl) :sharing
+                                         #+(and acl2-par ccl) :lock))))
                       (:byte
                        (cond ((eq file-name :string)
                               (make-string-output-stream

basis-a.lisp

@@ -5079,10 +5079,10 @@
                             (fmt-ctx ctx col channel state)
                             (fmt1 ":  " nil col channel state nil)))))))
 
-(defun er-soft-off-p1 (summary wrld)
+(defun er-off-p1 (summary wrld)
 
-; This function is used by er-soft to determine whether a given error should be
-; printed.
+; This function is used by er-soft, er-hard?, and er-hard to determine whether
+; a given error should be printed.
 
   (declare (xargs :guard (and (or (null summary)
                                   (and (stringp summary)
@@ -5095,15 +5095,15 @@
         summary
         (table-alist 'inhibit-er-table wrld))))
 
-(defun er-soft-off-p (summary state)
+(defun er-off-p (summary state)
   (declare (xargs :stobjs state
                   :guard (and (or (null summary)
                                   (and (stringp summary)
                                        (standard-string-p summary)))
                               (state-p state)
                               (standard-string-alistp
                                (table-alist 'inhibit-er-table (w state))))))
-  (er-soft-off-p1 summary (w state)))
+  (er-off-p1 summary (w state)))
 
 (defun error-fms-channel (hardp ctx summary str alist channel state newlines)
 
@@ -5119,7 +5119,7 @@
 ; by our er macro.  We rewrote the function this way simply so we
 ; would not have to remember that some variables are special.
 
-  (cond ((er-soft-off-p summary state)
+  (cond ((er-off-p summary state)
          state)
         (t
          (flet ((newlines (n channel state)

basis-b.lisp

@@ -3475,6 +3475,7 @@
                          (equal (stobjs-in val wrld) '(nil state))
                          (equal (stobjs-out val wrld) '(nil state)))
                     (cond ((or (eq val 'brr-prompt)
+                               (eq val 'wormhole-prompt)
                                (ttag wrld))
                            (value nil))
                           (t (er soft ctx

books/centaur/gl/gl-generic-interp.lisp

@@ -80,10 +80,9 @@
 (progn ;; sublis-into-term-pseudo-termp
   (defthm len-sublis-into-list
     (implies (pseudo-term-listp x)
-             (equal (length (sublis-into-list x subst))
-                    (length x)))
-    :hints (("goal" :induct (len x)
-             :in-theory (enable length))))
+             (equal (len (sublis-into-list x subst))
+                    (len x)))
+    :hints (("goal" :induct (len x))))
 
   (defthm-sublis-into-term-flg
     sublis-into-term-pseudo-term-lemma

books/kestrel/apt/rename-params-tests.lisp

@@ -380,12 +380,16 @@
                              ((SYMBOLP (CAR TERM))
                               (SYMBOLP (CAR TERM)))
                              ((TRUE-LISTP (CAR TERM))
-                              (AND (EQUAL (LENGTH (CAR TERM)) 3)
+                              (AND (EQUAL (mbe :logic (len (CAR TERM))
+                                               :exec (length (car term)))
+                                          3)
                                    (EQ (CAR (CAR TERM)) 'LAMBDA)
                                    (SYMBOL-LISTP (CADR (CAR TERM)))
                                    (NEW-PSEUDO-TERMP (CADDR (CAR TERM)))
-                                   (EQUAL (LENGTH (CADR (CAR TERM)))
-                                          (LENGTH (CDR TERM)))))
+                                   (EQUAL (mbe :logic (len (CADR (CAR TERM)))
+                                               :exec (length (CADR (CAR TERM))))
+                                          (mbe :logic (len (CDR TERM))
+                                               :exec (length (CDR TERM))))))
                              (T NIL)))
                      (DEFUN NEW-PSEUDO-TERM-LISTP (TERMS)
                        (DECLARE (IGNORABLE TERMS))

books/kestrel/utilities/my-get-event-tests.lisp

@@ -59,12 +59,12 @@
                             ((NOT (PSEUDO-TERM-LISTP (CDR X))) NIL)
                             (T (OR (SYMBOLP (CAR X))
                                    (AND (TRUE-LISTP (CAR X))
-                                        (EQUAL (LENGTH (CAR X)) 3)
+                                        (EQUAL (LEN$ (CAR X)) 3)
                                         (EQ (CAR (CAR X)) 'LAMBDA)
                                         (SYMBOL-LISTP (CADR (CAR X)))
                                         (PSEUDO-TERMP (CADDR (CAR X)))
-                                        (EQUAL (LENGTH (CADR (CAR X)))
-                                               (LENGTH (CDR X))))))))
+                                        (EQUAL (LEN$ (CADR (CAR X)))
+                                               (LEN$ (CDR X))))))))
                     (DEFUN PSEUDO-TERM-LISTP (LST)
                       (DECLARE (XARGS :GUARD T))
                       (COND ((ATOM LST) (EQUAL LST NIL))

books/system/doc/acl2-doc.lisp

@@ -56615,8 +56615,9 @@ tables in the current Hons Space."
  last line output).  You may define your own @(see prompt) printing function,
  @('fn'), and install it with @('(set-ld-prompt 'fn state)').  However, a trust
  tag must be active (see @(see defttag)) when you set @('ld-prompt') to other
- than @('t') or @('nil') (with one exception: the function @('brr-prompt'),
- which prints the prompt in the @(see break-rewrite) loop).</p>
+ than @('t') or @('nil') (with two exceptions: the functions @('brr-prompt')
+ and @('wormhole-prompt'), which print the prompt in the @(see break-rewrite)
+ loop and the general @(see wormhole) loop, respectively).</p>
 
  <p>If you supply an inappropriate @(see prompt) function, i.e., one that
  causes an error or does not return the correct number and type of results, the
@@ -101528,6 +101529,9 @@ it."
 
 ; Fixed guard for warning1-cw (warning$, ...?) to allow summary of ("foo").
 
+; Changed er-soft-off-p[1] to er-off-p[1]: just a name change, since this is
+; about hard errors too, not just soft errors.
+
   :parents (release-notes)
   :short "ACL2 Version  8.6 (xxx, 20xx) Notes"
   :long "<p>NOTE!  New users can ignore these release notes, because the @(see
@@ -101739,6 +101743,19 @@ it."
  ACL2 Error [Failure] in ( THM ...):  See :DOC failure.
  })
 
+ <p>When an event fails, then if it involves definition @(see rune)s for @(tsee
+ loop$) @(see scion)s, the failure message may suggest including the book
+ @('projects/apply/top') if it hasn't already been included.  That book
+ provides quite a few lemmas about @(tsee loop$) scions.</p>
+
+ <p>Replaced @(tsee length) calls in the defun of @(tsee pseudo-termp) with
+ calls of a new macro, @('len$'), which is a call of @(tsee mbe) that invokes
+ @(tsee length) in the @(':exec') code and @(tsee len) in the @(':logic') code.
+ Thanks to Eric Smith for requesting such an enhancement, and for discussing
+ specifics of it, so as to avoid the need for at least one unfortunate rule
+ that if @('(pseudo-termp term)') then @('(not (stringp (cdr term)))'),
+ apparently needed because @('length') behaves specially on strings.</p>
+
  <h3>New Features</h3>
 
  <p>The new zero-ary attachable system function, @(tsee heavy-linear-p), allows
@@ -101837,6 +101854,8 @@ it."
  requesting such a capability, to support faster loading of @('.port') files by
  the build system (see @(tsee build::cert.pl)).</p>
 
+ <p>The symbol, @('number'), is now a legal @(see type-spec).</p>
+
  <h3>Heuristic and Efficiency Improvements</h3>
 
  <p>Added a &ldquo;desperation heuristic&rdquo; to compute a stronger context,
@@ -101990,9 +102009,12 @@ it."
  @(tsee LD) special @(tsee ld-skip-proofsp) is non-@('nil') at that time.
  Thus, that situation no longer disqualifies such a world from supplying the
  @(see portcullis) commands to a book to be certified without keyword argument
- @(':skip-proofs-okp t) of @(tsee certify-book).  Thanks to Sol Swords for
+ @(':skip-proofs-okp t') of @(tsee certify-book).  Thanks to Sol Swords for
  pointing out this bug.</p>
 
+ <p>Fixed a bug that was causing calls of @(tsee wormhole) to signal an
+ error.</p>
+
  <h3>Changes at the System Level</h3>
 
  <p>The `@('make')' target, @('save-exec'), now builds @('custom-saved_acl2')
@@ -143708,6 +143730,7 @@ introduction-to-the-tau-system) for more information about Tau.</dd>
   (NOT type)             (NOT (p X))
                          where (p x) is the meaning for type-spec type
   NULL                   (EQ X NIL)
+  NUMBER                 (ACL2-NUMBERP x)
   (OR type1 ... typek)   (OR (p1 X) ... (pk X))
                          where (pj x) is the meaning for type-spec typej
   RATIO                  (AND (RATIONALP X) (NOT (INTEGERP X)))

books/xdoc/display.lisp

@@ -762,8 +762,10 @@
             '(lambda (acl2::whs)
                (let ((data (wormhole-data acl2::whs)))
                  (and data
-                      (acl2::warning$-cw
+                      (acl2::warning$-cw0
                        'xdoc
+                       nil
+                       (default-state-vars t)
                        "Please note the following broken topic link ~
                         name~#0~[~/s~]: ~&0.  To suppress such warnings: ~x1."
                        (reverse (remove-duplicates-equal data))

doc.lisp

@@ -60295,8 +60295,9 @@ Subtopics
   define your own [prompt] printing function, fn, and install it with
   (set-ld-prompt 'fn state).  However, a trust tag must be active
   (see [defttag]) when you set ld-prompt to other than t or nil (with
-  one exception: the function brr-prompt, which prints the prompt in
-  the [break-rewrite] loop).
+  two exceptions: the functions brr-prompt and wormhole-prompt, which
+  print the prompt in the [break-rewrite] loop and the general
+  [wormhole] loop, respectively).
 
   If you supply an inappropriate [prompt] function, i.e., one that
   causes an error or does not return the correct number and type of
@@ -98718,6 +98719,20 @@ Changes to Existing Features
 
     ACL2 Error [Failure] in ( THM ...):  See :DOC failure.
 
+  When an event fails, then if it involves definition [rune]s for
+  [loop$] [scion]s, the failure message may suggest including the
+  book projects/apply/top if it hasn't already been included.  That
+  book provides quite a few lemmas about [loop$] scions.
+
+  Replaced [length] calls in the defun of [pseudo-termp] with calls of
+  a new macro, len$, which is a call of [mbe] that invokes [length]
+  in the :exec code and [len] in the :logic code.  Thanks to Eric
+  Smith for requesting such an enhancement, and for discussing
+  specifics of it, so as to avoid the need for at least one
+  unfortunate rule that if (pseudo-termp term) then (not (stringp
+  (cdr term))), apparently needed because length behaves specially on
+  strings.
+
 
 New Features
 
@@ -98825,6 +98840,8 @@ New Features
   requesting such a capability, to support faster loading of .port
   files by the build system (see [build::cert.pl]).
 
+  The symbol, number, is now a legal [type-spec].
+
 
 Heuristic and Efficiency Improvements
 
@@ -98966,12 +98983,18 @@ Bug Fixes
   of [ld] special [ld-skip-proofsp] is non-nil at that time.  Thus,
   that situation no longer disqualifies such a world from supplying
   the [portcullis] commands to a book to be certified without keyword
-  argument :skip-proofs-okp t) of @(tsee certify-book).  Thanks to
-  Sol Swords for pointing out this bug.</p> <h3>Changes at the System
-  Level</h3> <p>The `@('make' target, save-exec, now builds
-  custom-saved_acl2 unconditionally.  Thanks to Grant Jurgensen for
-  pointing out (in GitHub Issue #1422) that there can be untracked
-  implicit dependencies that make this necessary.
+  argument :skip-proofs-okp t of [certify-book].  Thanks to Sol
+  Swords for pointing out this bug.
+
+  Fixed a bug that was causing calls of [wormhole] to signal an error.
+
+
+Changes at the System Level
+
+  The `make' target, save-exec, now builds custom-saved_acl2
+  unconditionally.  Thanks to Grant Jurgensen for pointing out (in
+  GitHub Issue #1422) that there can be untracked implicit
+  dependencies that make this necessary.
 
   Implementations underlying the functions [sys-call], [sys-call+], and
   [sys-call*] have been cleaned up.  In particular, we now expect
@@ -143248,6 +143271,7 @@ Type Specs
     (NOT type)             (NOT (p X))
                            where (p x) is the meaning for type-spec type
     NULL                   (EQ X NIL)
+    NUMBER                 (ACL2-NUMBERP x)
     (OR type1 ... typek)   (OR (p1 X) ... (pk X))
                            where (pj x) is the meaning for type-spec typej
     RATIO                  (AND (RATIONALP X) (NOT (INTEGERP X)))

doc/acl2-code-size.txt

@@ -1,14 +1,14 @@
 Source files (not including doc.lisp):
 ------------------------------------
   CODE LINES:
-  155108 lines,   6925146 characters
+  155138 lines,   6926569 characters
   COMMENT LINES:
-   88537 lines,   5364931 characters
+   88563 lines,   5366489 characters
   BLANK LINES:
-   36597 lines,     36597 characters
+   36607 lines,     36607 characters
   TOTAL:
-  280242 lines,  12326674 characters
+  280308 lines,  12329665 characters
 ------------------------------------
 Documentation (file books/system/doc/acl2-doc.lisp):
-  157695 lines,   6913231 characters
+  157718 lines,   6914450 characters
 ------------------------------------

doc/home-page.html

@@ -152,7 +152,7 @@
 <center>
 <b><a href="mailto:kaufmann@cs.utexas.edu">Matt Kaufmann</a> and <a href="mailto:moore@cs.utexas.edu">J Strother Moore</a></b><br>
 <a href="http://www.utexas.edu">University of Texas at Austin</a><br>
-March 6, 2023
+March 11, 2023
 </center>
 
 <p>