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