From 1db0462df8a3cf1e3c88b0fd8b5bb00f5994d499 Mon Sep 17 00:00:00 2001 From: Matt Kaufmann Date: Sat, 11 Mar 2023 02:11:53 -0600 Subject: [PATCH] Added NUMBER as a type-spec. On proof failure, suggest including apply$ 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 | 4 ++ axioms.lisp | 54 ++++++++++++++++--- basis-a.lisp | 12 ++--- basis-b.lisp | 1 + books/centaur/gl/gl-generic-interp.lisp | 7 ++- books/kestrel/apt/rename-params-tests.lisp | 10 ++-- .../kestrel/utilities/my-get-event-tests.lisp | 6 +-- books/system/doc/acl2-doc.lisp | 29 ++++++++-- books/xdoc/display.lisp | 4 +- doc.lisp | 40 +++++++++++--- doc/acl2-code-size.txt | 10 ++-- doc/home-page.html | 2 +- history-management.lisp | 27 +++++++++- ld.lisp | 24 +++++---- translate.lisp | 4 +- 15 files changed, 178 insertions(+), 56 deletions(-) diff --git a/acl2-fns.lisp b/acl2-fns.lisp index 7312379a3f7..29d13181a8f 100644 --- a/acl2-fns.lisp +++ b/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)) diff --git a/axioms.lisp b/axioms.lisp index 5217ebf5a8b..68e01fe117e 100644 --- a/axioms.lisp +++ b/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 diff --git a/basis-a.lisp b/basis-a.lisp index b7aefe997be..93447703060 100644 --- a/basis-a.lisp +++ b/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,7 +5095,7 @@ 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) @@ -5103,7 +5103,7 @@ (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) diff --git a/basis-b.lisp b/basis-b.lisp index 6ced2f868be..cc41e67cdb0 100644 --- a/basis-b.lisp +++ b/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 diff --git a/books/centaur/gl/gl-generic-interp.lisp b/books/centaur/gl/gl-generic-interp.lisp index 1c1a9fbcd09..82b7139272b 100644 --- a/books/centaur/gl/gl-generic-interp.lisp +++ b/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 diff --git a/books/kestrel/apt/rename-params-tests.lisp b/books/kestrel/apt/rename-params-tests.lisp index 69aa9a403d9..0fc3e79b946 100644 --- a/books/kestrel/apt/rename-params-tests.lisp +++ b/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)) diff --git a/books/kestrel/utilities/my-get-event-tests.lisp b/books/kestrel/utilities/my-get-event-tests.lisp index 9dbbb88d6bb..9fad70f72b0 100644 --- a/books/kestrel/utilities/my-get-event-tests.lisp +++ b/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)) diff --git a/books/system/doc/acl2-doc.lisp b/books/system/doc/acl2-doc.lisp index 56d7cc91c51..841b8b5d3e9 100644 --- a/books/system/doc/acl2-doc.lisp +++ b/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).

+ 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).

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 "

NOTE! New users can ignore these release notes, because the @(see @@ -101739,6 +101743,19 @@ it." ACL2 Error [Failure] in ( THM ...): See :DOC failure. }) +

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.

+ +

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.

+

New Features

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)).

+

The symbol, @('number'), is now a legal @(see type-spec).

+

Heuristic and Efficiency Improvements

Added a “desperation heuristic” 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.

+

Fixed a bug that was causing calls of @(tsee wormhole) to signal an + error.

+

Changes at the System Level

The `@('make')' target, @('save-exec'), now builds @('custom-saved_acl2') @@ -143708,6 +143730,7 @@ introduction-to-the-tau-system) for more information about Tau. (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))) diff --git a/books/xdoc/display.lisp b/books/xdoc/display.lisp index efe4c874261..5de2d492fe2 100644 --- a/books/xdoc/display.lisp +++ b/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)) diff --git a/doc.lisp b/doc.lisp index 43c3f415924..c1633a2c356 100644 --- a/doc.lisp +++ b/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.

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. + 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))) diff --git a/doc/acl2-code-size.txt b/doc/acl2-code-size.txt index 5bceecf4e8d..6f6cd84650f 100644 --- a/doc/acl2-code-size.txt +++ b/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 ------------------------------------ diff --git a/doc/home-page.html b/doc/home-page.html index 1c732bb1cec..a377244cc0c 100644 --- a/doc/home-page.html +++ b/doc/home-page.html @@ -152,7 +152,7 @@

Matt Kaufmann and J Strother Moore
University of Texas at Austin
-March 6, 2023 +March 11, 2023

diff --git a/history-management.lisp b/history-management.lisp index d5fb8dcd58a..17e2bcb9895 100644 --- a/history-management.lisp +++ b/history-management.lisp @@ -2407,18 +2407,41 @@ (stringp (car arg)) (character-alistp (cdr arg))))) +(defun collect-definition-rune-fns (fns runes) + (cond ((endp runes) nil) + ((and (eq (caar runes) :definition) + (member-eq (base-symbol (car runes)) fns)) + (cons (base-symbol (car runes)) + (collect-definition-rune-fns fns (cdr runes)))) + (t (collect-definition-rune-fns fns (cdr runes))))) + (defun print-failure1 (erp acc-ttree ctx state) (let ((channel (proofs-co state))) (pprogn (error-fms-channel nil ctx "Failure" - "~@0See :DOC failure.~#1~[~|*NOTE*: Useless-runes were in use and can ~ - affect proof attempts. See :DOC useless-runes-failures.~/~]" + "~@0See :DOC failure.~@1~#2~[~|*NOTE*: Useless-runes were in use and ~ + can affect proof attempts. See :DOC useless-runes-failures.~/~]" (list (cons #\0 (if (tilde-@p erp) erp "")) (cons #\1 + (if (global-val 'projects/apply/base-includedp (w state)) + "" + (let ((loop$-fns (collect-definition-rune-fns + *loop$-special-function-symbols* + (tagged-objects 'lemma acc-ttree)))) + (if loop$-fns + (msg "~|*NOTE*: The definition~#0~[ of ~&0 was~/s ~ + of ~&0 were~] used in the proof attempt, but ~ + a relevant book has not been included. ~ + Consider first evaluating ~x1." + loop$-fns + '(include-book "projects/apply/top" + :dir :system)) + "")))) + (cons #\2 (if (and acc-ttree ; likely non-nil after a proof attempt (not (ld-skip-proofsp state)) (let ((useless-runes diff --git a/ld.lisp b/ld.lisp index ac318128e23..caa7304bda7 100644 --- a/ld.lisp +++ b/ld.lisp @@ -2175,16 +2175,20 @@ :ld-user-stobjs-modified-warning :same)) (defun wormhole-prompt (channel state) - (fmt1 "Wormhole ~s0~sr ~@1~*2" - (list (cons #\0 (f-get-global 'current-package state)) - (cons #\1 (defun-mode-prompt-string state)) - (cons #\r - #+:non-standard-analysis "(r)" - #-:non-standard-analysis "") - (cons #\2 - (list "" ">" ">" ">" - (make-list-ac (- (f-get-global 'ld-level state) 1) nil nil)))) - 0 channel state nil)) + (the2s + (signed-byte 30) + (fmt1 "Wormhole ~s0~sr ~@1~*2" + (list (cons #\0 (f-get-global 'current-package state)) + (cons #\1 (defun-mode-prompt-string state)) + (cons #\r + #+:non-standard-analysis "(r)" + #-:non-standard-analysis "") + (cons #\2 + (list "" ">" ">" ">" + (make-list-ac (- (f-get-global 'ld-level state) 1) + nil + nil)))) + 0 channel state nil))) (defun reset-ld-specials-fn (reset-channels-flg state) diff --git a/translate.lisp b/translate.lisp index b015ec87ebd..3809f14d32d 100644 --- a/translate.lisp +++ b/translate.lisp @@ -10965,9 +10965,7 @@ (kwote summary) summary) str+ - (make-fmt-bindings '(#\0 #\1 #\2 #\3 #\4 - #\5 #\6 #\7 #\8 #\9) - fmt-args) + (make-fmt-bindings *base-10-chars* fmt-args) 'wrld 'state-vars))