[acl2/acl2] 6d1c44: [arm] Add BFC and BFI instructions.
0 views
Skip to first unread message
Eric W. Smith
Mar 25, 2026, 5:02:59 PM (3 days ago) Mar 25
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 6d1c444711ed579a58ad46699b73cf96efc9c74f
https://github.com/acl2/acl2/commit/6d1c444711ed579a58ad46699b73cf96efc9c74f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-24 (Tue, 24 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/axe/arm/rule-lists.lisp
Log Message:
-----------
[arm] Add BFC and BFI instructions.
Commit: dda708ba6ce53f302688fdd01ea614af444d3537
https://github.com/acl2/acl2/commit/dda708ba6ce53f302688fdd01ea614af444d3537
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-24 (Tue, 24 Mar 2026)
Changed paths:
M books/kestrel/arm/pseudocode.lisp
Log Message:
-----------
[arm] Organize some material.
To match the order in the spec.
Commit: 4b342fdad3b8ced29383b54aced37ffb982b031f
https://github.com/acl2/acl2/commit/4b342fdad3b8ced29383b54aced37ffb982b031f
Author: Eric Smith <ews...@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:
-----------
[arm] Add more instruction models.
Also improve error handling and remove extra spaces in some encodings.
Commit: 4faa06f4f5f292e8291b731452d7d649acb61fb7
https://github.com/acl2/acl2/commit/4faa06f4f5f292e8291b731452d7d649acb61fb7
Author: Eric Smith <ews...@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
Log Message:
-----------
[arm] Add more instruction models.
Also fix error handling.
Commit: 8f02d0398a62fe90677b7d955bb278d4f8232ef0
https://github.com/acl2/acl2/commit/8f02d0398a62fe90677b7d955bb278d4f8232ef0
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-25 (Wed, 25 Mar 2026)
Changed paths:
M books/kestrel/arm/instructions.lisp
Log Message:
-----------
[arm] Tweak bit constants.
Compare: https://github.com/acl2/acl2/compare/4ec3e0c988bd...8f02d0398a62
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 6d1c444711ed579a58ad46699b73cf96efc9c74f
https://github.com/acl2/acl2/commit/6d1c444711ed579a58ad46699b73cf96efc9c74f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-24 (Tue, 24 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/axe/arm/rule-lists.lisp
Log Message:
-----------
[arm] Add BFC and BFI instructions.
Commit: dda708ba6ce53f302688fdd01ea614af444d3537
https://github.com/acl2/acl2/commit/dda708ba6ce53f302688fdd01ea614af444d3537
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-24 (Tue, 24 Mar 2026)
Changed paths:
M books/kestrel/arm/pseudocode.lisp
Log Message:
-----------
[arm] Organize some material.
To match the order in the spec.
Commit: 4b342fdad3b8ced29383b54aced37ffb982b031f
https://github.com/acl2/acl2/commit/4b342fdad3b8ced29383b54aced37ffb982b031f
Author: Eric Smith <ews...@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:
-----------
[arm] Add more instruction models.
Also improve error handling and remove extra spaces in some encodings.
Commit: 4faa06f4f5f292e8291b731452d7d649acb61fb7
https://github.com/acl2/acl2/commit/4faa06f4f5f292e8291b731452d7d649acb61fb7
Author: Eric Smith <ews...@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
Log Message:
-----------
[arm] Add more instruction models.
Also fix error handling.
Commit: 8f02d0398a62fe90677b7d955bb278d4f8232ef0
https://github.com/acl2/acl2/commit/8f02d0398a62fe90677b7d955bb278d4f8232ef0
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-25 (Wed, 25 Mar 2026)
Changed paths:
M books/kestrel/arm/instructions.lisp
Log Message:
-----------
[arm] Tweak bit constants.
Compare: https://github.com/acl2/acl2/compare/4ec3e0c988bd...8f02d0398a62
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
acl2buildserver
Mar 25, 2026, 6:32:46 PM (3 days ago) Mar 25
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: 74ec7a690d1b456454b237ad18b6fef61261002a
https://github.com/acl2/acl2/commit/74ec7a690d1b456454b237ad18b6fef61261002a
Author: ACL2 Build Server <acl2bui...@gmail.com>
Compare: https://github.com/acl2/acl2/compare/370ab59f9fc7...74ec7a690d1b
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
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:
-----------
Compare: https://github.com/acl2/acl2/compare/370ab59f9fc7...74ec7a690d1b
acl2buildserver
Mar 25, 2026, 6:33:37 PM (3 days ago) Mar 25
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
1:58 AM (5 hours ago) 1:58 AM
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: c13d5a7cc275db1bb68ddb830baeebb545ab6b84
https://github.com/acl2/acl2/commit/c13d5a7cc275db1bb68ddb830baeebb545ab6b84
M books/tools/flag.lisp
Log Message:
-----------
[make-flag] Fix error handling.
Approved by Sol via Zulip message.
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: 842db89780d7acf3deabb4ba2e869aaae1b2bce9
https://github.com/acl2/acl2/commit/842db89780d7acf3deabb4ba2e869aaae1b2bce9
Commit: c9f4128e658ba8a7bc7648949ccc976a99390473
https://github.com/acl2/acl2/commit/c9f4128e658ba8a7bc7648949ccc976a99390473
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Log Message:
-----------
Fixed a typo in a comment, found by Eric Smith.
Commit: a0b79b6e00bd6ba4e6414f8f44c2c00b4bf5589e
https://github.com/acl2/acl2/commit/a0b79b6e00bd6ba4e6414f8f44c2c00b4bf5589e
Changed paths:
M books/tools/flag.lisp
Log Message:
-----------
Merge commit '842db89780d7acf3deabb4ba2e869aaae1b2bce9' into HEAD
Commit: 7086e841711b263366bb385872bc1d4fb40cfa58
https://github.com/acl2/acl2/commit/7086e841711b263366bb385872bc1d4fb40cfa58
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)
Changed paths:
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/bv/arith.lisp
Log Message:
-----------
[bv] Drop unneeded rule.
Also tweak a rule.
Commit: f33a0a9f2af987a8eda420f5604265eb41625e6f
https://github.com/acl2/acl2/commit/f33a0a9f2af987a8eda420f5604265eb41625e6f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)
Changed paths:
M books/kestrel/axe/rules1.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
M books/kestrel/bv-lists/bv-array-read.lisp
M books/kestrel/x86/read-and-write.lisp
Log Message:
-----------
[bv-lists] Small improvements.
Commit: de69359deaa67b92f32fb8ff7a7d2a007342de21
https://github.com/acl2/acl2/commit/de69359deaa67b92f32fb8ff7a7d2a007342de21
Author: Eric McCarthy <mcca...@kestrel.edu>
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:
-----------
[build] Add sbcl-only as a cert_param
Commit: 778c95fd35e96049a516fd2601e68590def74145
https://github.com/acl2/acl2/commit/778c95fd35e96049a516fd2601e68590def74145
Changed paths:
M books/GNUmakefile
M books/build/cert.pl
M books/build/doc.lisp
Log Message:
-----------
Merge commit 'de69359deaa67b92f32fb8ff7a7d2a007342de21' into HEAD
Commit: e73abde9d4f16c09c906e370c10829fa8742a0fb
https://github.com/acl2/acl2/commit/e73abde9d4f16c09c906e370c10829fa8742a0fb
Author: Eric Smith <ews...@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: 4302f71be44093574bd1fa24660c2c059b6e94a4
https://github.com/acl2/acl2/commit/4302f71be44093574bd1fa24660c2c059b6e94a4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)
Changed paths:
M books/kestrel/bv-lists/array-patterns.lisp
Log Message:
-----------
[bv-lists] Improve rule.
Commit: de7c60533906fe51cf71e8a95274904e620ddc7b
https://github.com/acl2/acl2/commit/de7c60533906fe51cf71e8a95274904e620ddc7b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)
Changed paths:
M books/kestrel/axe/rules1.lisp
Log Message:
-----------
[axe] Continue cleaning up file.
Commit: 5ae77decda4dbd607acb1dc5e36d4fe849fdf16f
https://github.com/acl2/acl2/commit/5ae77decda4dbd607acb1dc5e36d4fe849fdf16f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)
Changed paths:
M books/GNUmakefile
Log Message:
-----------
[books/GNUmakefile] Make it an error when a book needs ACL2(r) but also needs non-ACL2(r).
Commit: 0a69673439f54d5163322f85f550bcec6ca20d32
https://github.com/acl2/acl2/commit/0a69673439f54d5163322f85f550bcec6ca20d32
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 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/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/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:
-----------
[bv-arrays] Split out bv-array material into new library.
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
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: 6fa0efd89ddbd4c46de13c505d01da00f8b5c519
https://github.com/acl2/acl2/commit/6fa0efd89ddbd4c46de13c505d01da00f8b5c519
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/GNUmakefile
Log Message:
-----------
Merge pull request #1923 from acl2/r-and-non-r
[books/GNUmakefile] Make it an error when a book needs ACL2(r) but also needs non-ACL2(r).
Commit: 4f6f644f7501104e0f02c3d544ec0fb74af15a3d
https://github.com/acl2/acl2/commit/4f6f644f7501104e0f02c3d544ec0fb74af15a3d
Changed paths:
M books/GNUmakefile
Log Message:
-----------
Merge commit '6fa0efd89ddbd4c46de13c505d01da00f8b5c519' into HEAD
Commit: e4fe49d47c1d99def555c4e7db89736455051912
https://github.com/acl2/acl2/commit/e4fe49d47c1d99def555c4e7db89736455051912
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/defobject.lisp
M books/kestrel/c/atc/input-processing.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/top.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/output-files.lisp
Log Message:
-----------
[ATC] [C$] Fix some format strings.
Commit: bb91299021a58f8683eabae1dad871a3d2aa2cfd
https://github.com/acl2/acl2/commit/bb91299021a58f8683eabae1dad871a3d2aa2cfd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/input-processing.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/syntax/token-concatenation.lisp
Log Message:
-----------
[ATC] [C$] Fix typos in error messages.
Commit: 7d1472710a84b287d3e0704c85b347c948271f91
https://github.com/acl2/acl2/commit/7d1472710a84b287d3e0704c85b347c948271f91
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Fix pretty-printer.
Print `enum` instead of `union` for an enum. It was a copy-and-paste error.
Commit: e18c9cdfeb6fb5ef08c52ec4b4594c672be4248b
https://github.com/acl2/acl2/commit/e18c9cdfeb6fb5ef08c52ec4b4594c672be4248b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Fix check in pretty-printer.
This should be the same in abstract declarators as it is for (non-abstract)
declarators.
Commit: 4d6e7abc6ea4d37c658c126cf7aa492288701595
https://github.com/acl2/acl2/commit/4d6e7abc6ea4d37c658c126cf7aa492288701595
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Remove stray parenthesis in pretty-printed string.
Commit: e8903eb3bd59ca389e7de15bd689a2da7fb0b7ec
https://github.com/acl2/acl2/commit/e8903eb3bd59ca389e7de15bd689a2da7fb0b7ec
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Fix bug in pretty-printer.
Two expected expression grades were swapped.
Commit: 1f6dc459b46e0646c2ae3bbbf0b84f63cde1e453
https://github.com/acl2/acl2/commit/1f6dc459b46e0646c2ae3bbbf0b84f63cde1e453
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Fix format string.
Commit: 9469ff8beec009a5219e5f5f709d26342872242b
https://github.com/acl2/acl2/commit/9469ff8beec009a5219e5f5f709d26342872242b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Fix bug in pretty-printer.
It was neglecting to print the expression of a `case` label.
Commit: 8506b7af6ad2534fd714b3359ad3fbf347fb085a
https://github.com/acl2/acl2/commit/8506b7af6ad2534fd714b3359ad3fbf347fb085a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/hdwallet/wallet.lisp
Log Message:
-----------
[HD wallet] Fix error message.
Commit: fe53840676f5868533b4c29346748022fac155f3
https://github.com/acl2/acl2/commit/fe53840676f5868533b4c29346748022fac155f3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/hdwallet/wallet.lisp
Log Message:
-----------
[HD wallet] Fix typo in doc.
Commit: 538902e3b5008bc68f19f13382b5371c1cd24371
https://github.com/acl2/acl2/commit/538902e3b5008bc68f19f13382b5371c1cd24371
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/hdwallet/wallet.lisp
Log Message:
-----------
[HD wallet] Update file header.
Commit: 463cc13def310fb90c54535d5e82523366e98149
https://github.com/acl2/acl2/commit/463cc13def310fb90c54535d5e82523366e98149
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/fty/fty-omap.lisp
Log Message:
-----------
[FTY] Fix two error messages.
Commit: 8aba42e698e704a735da9f25ec7af6c43f0163d3
https://github.com/acl2/acl2/commit/8aba42e698e704a735da9f25ec7af6c43f0163d3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/soft/defequal.lisp
Log Message:
-----------
[SOFT] Fix some error messages.
Commit: 6601af64e44b136f5e6ae1d80e52925db138ee60
https://github.com/acl2/acl2/commit/6601af64e44b136f5e6ae1d80e52925db138ee60
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/solidity/boolean-operations.lisp
Log Message:
-----------
[Solidity] Fix repeated word in doc.
Compare: https://github.com/acl2/acl2/compare/370ab59f9fc7...6601af64e44b
https://github.com/acl2/acl2/commit/c13d5a7cc275db1bb68ddb830baeebb545ab6b84
M books/tools/flag.lisp
Log Message:
-----------
[make-flag] Fix error handling.
Approved by Sol via Zulip message.
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
https://github.com/acl2/acl2/commit/842db89780d7acf3deabb4ba2e869aaae1b2bce9
Author: Eric Smith <ews...@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.
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:
-----------
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
Changed paths:
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: 7086e841711b263366bb385872bc1d4fb40cfa58
https://github.com/acl2/acl2/commit/7086e841711b263366bb385872bc1d4fb40cfa58
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)
Changed paths:
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/bv/arith.lisp
Log Message:
-----------
[bv] Drop unneeded rule.
Also tweak a rule.
Commit: f33a0a9f2af987a8eda420f5604265eb41625e6f
https://github.com/acl2/acl2/commit/f33a0a9f2af987a8eda420f5604265eb41625e6f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)
Changed paths:
M books/kestrel/axe/rules1.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
M books/kestrel/bv-lists/bv-array-read.lisp
M books/kestrel/x86/read-and-write.lisp
Log Message:
-----------
[bv-lists] Small improvements.
Commit: de69359deaa67b92f32fb8ff7a7d2a007342de21
https://github.com/acl2/acl2/commit/de69359deaa67b92f32fb8ff7a7d2a007342de21
Author: Eric McCarthy <mcca...@kestrel.edu>
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:
-----------
[build] Add sbcl-only as a cert_param
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: e73abde9d4f16c09c906e370c10829fa8742a0fb
https://github.com/acl2/acl2/commit/e73abde9d4f16c09c906e370c10829fa8742a0fb
Author: Eric Smith <ews...@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: 4302f71be44093574bd1fa24660c2c059b6e94a4
https://github.com/acl2/acl2/commit/4302f71be44093574bd1fa24660c2c059b6e94a4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)
Changed paths:
M books/kestrel/bv-lists/array-patterns.lisp
Log Message:
-----------
[bv-lists] Improve rule.
Commit: de7c60533906fe51cf71e8a95274904e620ddc7b
https://github.com/acl2/acl2/commit/de7c60533906fe51cf71e8a95274904e620ddc7b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)
Changed paths:
M books/kestrel/axe/rules1.lisp
Log Message:
-----------
[axe] Continue cleaning up file.
Commit: 5ae77decda4dbd607acb1dc5e36d4fe849fdf16f
https://github.com/acl2/acl2/commit/5ae77decda4dbd607acb1dc5e36d4fe849fdf16f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 Mar 2026)
Changed paths:
M books/GNUmakefile
Log Message:
-----------
[books/GNUmakefile] Make it an error when a book needs ACL2(r) but also needs non-ACL2(r).
Commit: 0a69673439f54d5163322f85f550bcec6ca20d32
https://github.com/acl2/acl2/commit/0a69673439f54d5163322f85f550bcec6ca20d32
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-26 (Thu, 26 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/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/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:
-----------
[bv-arrays] Split out bv-array material into new library.
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: 6fa0efd89ddbd4c46de13c505d01da00f8b5c519
https://github.com/acl2/acl2/commit/6fa0efd89ddbd4c46de13c505d01da00f8b5c519
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/GNUmakefile
Log Message:
-----------
Merge pull request #1923 from acl2/r-and-non-r
[books/GNUmakefile] Make it an error when a book needs ACL2(r) but also needs non-ACL2(r).
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
Commit: e4fe49d47c1d99def555c4e7db89736455051912
https://github.com/acl2/acl2/commit/e4fe49d47c1d99def555c4e7db89736455051912
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/defobject.lisp
M books/kestrel/c/atc/input-processing.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/top.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/output-files.lisp
Log Message:
-----------
[ATC] [C$] Fix some format strings.
Commit: bb91299021a58f8683eabae1dad871a3d2aa2cfd
https://github.com/acl2/acl2/commit/bb91299021a58f8683eabae1dad871a3d2aa2cfd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/input-processing.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/syntax/token-concatenation.lisp
Log Message:
-----------
[ATC] [C$] Fix typos in error messages.
Commit: 7d1472710a84b287d3e0704c85b347c948271f91
https://github.com/acl2/acl2/commit/7d1472710a84b287d3e0704c85b347c948271f91
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Fix pretty-printer.
Print `enum` instead of `union` for an enum. It was a copy-and-paste error.
Commit: e18c9cdfeb6fb5ef08c52ec4b4594c672be4248b
https://github.com/acl2/acl2/commit/e18c9cdfeb6fb5ef08c52ec4b4594c672be4248b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Fix check in pretty-printer.
This should be the same in abstract declarators as it is for (non-abstract)
declarators.
Commit: 4d6e7abc6ea4d37c658c126cf7aa492288701595
https://github.com/acl2/acl2/commit/4d6e7abc6ea4d37c658c126cf7aa492288701595
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Remove stray parenthesis in pretty-printed string.
Commit: e8903eb3bd59ca389e7de15bd689a2da7fb0b7ec
https://github.com/acl2/acl2/commit/e8903eb3bd59ca389e7de15bd689a2da7fb0b7ec
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Fix bug in pretty-printer.
Two expected expression grades were swapped.
Commit: 1f6dc459b46e0646c2ae3bbbf0b84f63cde1e453
https://github.com/acl2/acl2/commit/1f6dc459b46e0646c2ae3bbbf0b84f63cde1e453
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Fix format string.
Commit: 9469ff8beec009a5219e5f5f709d26342872242b
https://github.com/acl2/acl2/commit/9469ff8beec009a5219e5f5f709d26342872242b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printer.lisp
Log Message:
-----------
[ATC] Fix bug in pretty-printer.
It was neglecting to print the expression of a `case` label.
Commit: 8506b7af6ad2534fd714b3359ad3fbf347fb085a
https://github.com/acl2/acl2/commit/8506b7af6ad2534fd714b3359ad3fbf347fb085a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/hdwallet/wallet.lisp
Log Message:
-----------
[HD wallet] Fix error message.
Commit: fe53840676f5868533b4c29346748022fac155f3
https://github.com/acl2/acl2/commit/fe53840676f5868533b4c29346748022fac155f3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/hdwallet/wallet.lisp
Log Message:
-----------
[HD wallet] Fix typo in doc.
Commit: 538902e3b5008bc68f19f13382b5371c1cd24371
https://github.com/acl2/acl2/commit/538902e3b5008bc68f19f13382b5371c1cd24371
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/hdwallet/wallet.lisp
Log Message:
-----------
[HD wallet] Update file header.
Commit: 463cc13def310fb90c54535d5e82523366e98149
https://github.com/acl2/acl2/commit/463cc13def310fb90c54535d5e82523366e98149
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/fty/fty-omap.lisp
Log Message:
-----------
[FTY] Fix two error messages.
Commit: 8aba42e698e704a735da9f25ec7af6c43f0163d3
https://github.com/acl2/acl2/commit/8aba42e698e704a735da9f25ec7af6c43f0163d3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/soft/defequal.lisp
Log Message:
-----------
[SOFT] Fix some error messages.
Commit: 6601af64e44b136f5e6ae1d80e52925db138ee60
https://github.com/acl2/acl2/commit/6601af64e44b136f5e6ae1d80e52925db138ee60
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-27 (Fri, 27 Mar 2026)
Changed paths:
M books/kestrel/solidity/boolean-operations.lisp
Log Message:
-----------
[Solidity] Fix repeated word in doc.
Compare: https://github.com/acl2/acl2/compare/370ab59f9fc7...6601af64e44b
Reply all
Reply to author
Forward
0 new messages