[acl2/acl2] 1e7462: [C$] Remove some unneeded forms.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 1e74625284945673cdf6cfd28aea041229522234
https://github.com/acl2/acl2/commit/1e74625284945673cdf6cfd28aea041229522234
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-24 (Tue, 24 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/concrete-syntax.lisp

Log Message:
-----------
[C$] Remove some unneeded forms.


Commit: d43cbb91f7599123c7f186fb678ddce99f5a90cd
https://github.com/acl2/acl2/commit/d43cbb91f7599123c7f186fb678ddce99f5a90cd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-24 (Tue, 24 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/grammar-characters.lisp
M books/kestrel/c/syntax/grammar.lisp

Log Message:
-----------
[C$] Use controlled configuration.


Commit: 57c9a7b1822f980351155d438fdc7416ed2ba820
https://github.com/acl2/acl2/commit/57c9a7b1822f980351155d438fdc7416ed2ba820
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-24 (Tue, 24 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/grammar.lisp

Log Message:
-----------
[C$] Update and improve some doc.


Commit: 7da45c90311766c8d7b63bf1edb293be81a37b70
https://github.com/acl2/acl2/commit/7da45c90311766c8d7b63bf1edb293be81a37b70
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-25 (Wed, 25 Mar 2026)

Changed paths:
M books/projects/hol-in-acl2/examples/eval_poly.defhol
M books/projects/hol-in-acl2/examples/ex1.defhol

Log Message:
-----------
Merge.


Commit: 65a8cdc8e2f1e5b8dfc073dd89628262b2930535
https://github.com/acl2/acl2/commit/65a8cdc8e2f1e5b8dfc073dd89628262b2930535
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-25 (Wed, 25 Mar 2026)

Changed paths:
M books/kestrel/c/language/keywords.lisp

Log Message:
-----------
[C$] Fix typo in keyword lists.


Commit: 71fba40e2ea51a1778f0aa33cc7ba1130b577d24
https://github.com/acl2/acl2/commit/71fba40e2ea51a1778f0aa33cc7ba1130b577d24
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-25 (Wed, 25 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/grammar/all.abnf

Log Message:
-----------
[C$] Differentiate keywords in grammar.


Commit: e42ab0bcd9b485324724dd29bea8a247592af683
https://github.com/acl2/acl2/commit/e42ab0bcd9b485324724dd29bea8a247592af683
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-25 (Wed, 25 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/top.lisp

Log Message:
-----------
[C$] Doc tweak.


Commit: 16cfc0b51b5e69dbe2725e73b4298ada1bb720f8
https://github.com/acl2/acl2/commit/16cfc0b51b5e69dbe2725e73b4298ada1bb720f8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-25 (Wed, 25 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/grammar/all.abnf

Log Message:
-----------
[C$] Improve grammar.

Be more explicit about preprocessing lexemes and (after-preprocessing) lexemes.


Commit: 370ab59f9fc79940a003397b4e9d2d52b54371fc
https://github.com/acl2/acl2/commit/370ab59f9fc79940a003397b4e9d2d52b54371fc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-25 (Wed, 25 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/grammar/all.abnf

Log Message:
-----------
[C$] Extend ABNF grammar.

Add translation items.

Now the grammar is on par with the ASTs.


Compare: https://github.com/acl2/acl2/compare/4b9066a0dbfc...370ab59f9fc7

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

[Alessandro Coglio]

Branch: refs/heads/testing

[acl2buildserver]

Branch: refs/heads/testing-kestrel

Commit: 4b9066a0dbfce1751c523ee76d144f8f2db70a7d
https://github.com/acl2/acl2/commit/4b9066a0dbfce1751c523ee76d144f8f2db70a7d
Author: Matt Kaufmann <matthew.j...@gmail.com>

Date: 2026-03-24 (Tue, 24 Mar 2026)

Changed paths:

M books/projects/hol-in-acl2/examples/eval_poly.defhol
M books/projects/hol-in-acl2/examples/ex1.defhol

Log Message:
-----------

Synchronized hol-in-acl2 translation files with those in https://github.com/HOL-Theorem-Prover/HOL/tree/develop/examples/acl2/hol-to-acl2/examples (comment changes only)

Commit: 74ec7a690d1b456454b237ad18b6fef61261002a
https://github.com/acl2/acl2/commit/74ec7a690d1b456454b237ad18b6fef61261002a
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-03-25 (Wed, 25 Mar 2026)

Changed paths:

M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/axe/arm/rule-lists.lisp

Log Message:
-----------
Merge commit '8f02d0398a62fe90677b7d955bb278d4f8232ef0' into HEAD


Commit: c9f4128e658ba8a7bc7648949ccc976a99390473
https://github.com/acl2/acl2/commit/c9f4128e658ba8a7bc7648949ccc976a99390473
Author: Matt Kaufmann <kauf...@cs.utexas.edu>

Date: 2026-03-25 (Wed, 25 Mar 2026)

Changed paths:

M axioms.lisp

Log Message:
-----------
Fixed a typo in a comment, found by Eric Smith.


Commit: a0b79b6e00bd6ba4e6414f8f44c2c00b4bf5589e
https://github.com/acl2/acl2/commit/a0b79b6e00bd6ba4e6414f8f44c2c00b4bf5589e
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)

Changed paths:
M books/tools/flag.lisp

Log Message:
-----------
Merge commit '842db89780d7acf3deabb4ba2e869aaae1b2bce9' into HEAD


Commit: 778c95fd35e96049a516fd2601e68590def74145
https://github.com/acl2/acl2/commit/778c95fd35e96049a516fd2601e68590def74145
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)

Changed paths:
M books/GNUmakefile
M books/build/cert.pl
M books/build/doc.lisp

Log Message:
-----------
Merge commit 'de69359deaa67b92f32fb8ff7a7d2a007342de21' into HEAD


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


Commit: e7228d909d64f7964f260e59a16a23ead2ed0ca6
https://github.com/acl2/acl2/commit/e7228d909d64f7964f260e59a16a23ead2ed0ca6
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-27 (Fri, 27 Mar 2026)

Changed paths:
M books/kestrel/arm/memory.lisp
M books/kestrel/arrays-2d/bv-arrays-2d.lisp
M books/kestrel/axe/arm/evaluator.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/bv-array-rules.lisp
M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/evaluator-basic.lisp
M books/kestrel/axe/evaluator-support.lisp
M books/kestrel/axe/jvm/evaluator-jvm.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/packbv-axe.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/prove-with-stp2.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/risc-v/evaluator.lisp
M books/kestrel/axe/risc-v/lifter-rules.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/rules1.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/axe/unguarded-defuns2.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/x86-rules.lisp
A books/kestrel/bv-arrays/append-arrays.lisp
A books/kestrel/bv-arrays/array-of-zeros.lisp
A books/kestrel/bv-arrays/array-patterns.lisp
A books/kestrel/bv-arrays/bv-array-clear-range.lisp
A books/kestrel/bv-arrays/bv-array-clear.lisp
A books/kestrel/bv-arrays/bv-array-conversions-gen.lisp
A books/kestrel/bv-arrays/bv-array-conversions.lisp
A books/kestrel/bv-arrays/bv-array-conversions2-tests.lisp
A books/kestrel/bv-arrays/bv-array-conversions2.lisp
A books/kestrel/bv-arrays/bv-array-if.lisp
A books/kestrel/bv-arrays/bv-array-read-chunk-little.lisp
A books/kestrel/bv-arrays/bv-array-read-rules.lisp
A books/kestrel/bv-arrays/bv-array-read.lisp
A books/kestrel/bv-arrays/bv-array-write.lisp
A books/kestrel/bv-arrays/bv-arrayp.lisp
A books/kestrel/bv-arrays/bv-arrays.lisp
A books/kestrel/bv-arrays/tests-top.lisp
A books/kestrel/bv-arrays/top.lisp
R books/kestrel/bv-lists/append-arrays.lisp
R books/kestrel/bv-lists/array-of-zeros.lisp
R books/kestrel/bv-lists/array-patterns.lisp
R books/kestrel/bv-lists/bv-array-clear-range.lisp
R books/kestrel/bv-lists/bv-array-clear.lisp
R books/kestrel/bv-lists/bv-array-conversions-gen.lisp
R books/kestrel/bv-lists/bv-array-conversions.lisp
R books/kestrel/bv-lists/bv-array-conversions2-tests.lisp
R books/kestrel/bv-lists/bv-array-conversions2.lisp
R books/kestrel/bv-lists/bv-array-if.lisp
R books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
R books/kestrel/bv-lists/bv-array-read-rules.lisp
R books/kestrel/bv-lists/bv-array-read.lisp
R books/kestrel/bv-lists/bv-array-write.lisp
R books/kestrel/bv-lists/bv-arrayp.lisp
R books/kestrel/bv-lists/bv-arrays.lisp
M books/kestrel/bv-lists/tests-top.lisp
M books/kestrel/bv-lists/top.lisp
M books/kestrel/bv/arith.lisp
M books/kestrel/crypto/salsa/salsa20.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/java/atj/types-for-bv-fns.lisp
M books/kestrel/jvm/jvm.lisp
M books/kestrel/x86/bytes-loadedp.lisp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/support64.lisp
M books/kestrel/x86/tools/lifter-support.lisp

Log Message:
-----------
Merge commit '0a69673439f54d5163322f85f550bcec6ca20d32' into HEAD


Commit: 4f6f644f7501104e0f02c3d544ec0fb74af15a3d
https://github.com/acl2/acl2/commit/4f6f644f7501104e0f02c3d544ec0fb74af15a3d
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-27 (Fri, 27 Mar 2026)

Changed paths:
M books/GNUmakefile

Log Message:
-----------
Merge commit '6fa0efd89ddbd4c46de13c505d01da00f8b5c519' into HEAD


Compare: https://github.com/acl2/acl2/compare/6fa0efd89ddb...4f6f644f7501