[acl2/acl2] 045c9b: Made reader fixes as per Eric McCarthy, improving ...

[MattKaufmann]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 045c9b28cba1422dc2c45234f6e8171a344ccc76
https://github.com/acl2/acl2/commit/045c9b28cba1422dc2c45234f6e8171a344ccc76
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-03-27 (Fri, 27 Mar 2026)

Changed paths:
M acl2-check.lisp
M acl2-fns.lisp
M acl2.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Made reader fixes as per Eric McCarthy, improving how SBCL reads symbols and fixing a soundness bug in upcasing character 255. Also improved a check to cover char-downcase and char-upcase, pertaining to tht soundness bug. Also made a change that may inhibit some warnings during the build (when loading and compiling acl2-fns.lisp).

Quoting :DOC note-8-8:

(SBCL only) Modified SBCL to avoid its ``readtable normalization''
feature for reading symbols containing Unicode characters. This
avoids cases that otherwise create non-ACL2 characters in the
resulting [symbol-name]. Thanks to Eric McCarthy, who provided a
solution as well as the following raw Lisp example; see also {the
Zulip discussion of this issue |
https://acl2.zulip.kestrel.institute/#narrow/channel/19-general/topic/Non-ASCII.20characters.20in.20ACL2.20source.20files/near/40162}.

(char-code (char (symbol-name (read-from-string
(format nil "~c" (code-char 181))))
0))
=> 924 ; GREEK CAPITAL LETTER MU

Fixed a soundness bug caused by creation of a character that is not
an ACL2 character. All ACL2 characters have codes less than 256,
but the expression (char-code (char-upcase (code-char 255)))
evaluated to 376 in ACL2 built on every host Lisp except GCL.
Thanks to Eric McCarthy for {pointing out this bug as well as code
relevant to a fix |
https://acl2.zulip.kestrel.institute/#narrow/channel/19-general/topic/Non-ASCII.20characters.20in.20ACL2.20source.20files/near/40162}.



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/testing