[acl2/acl2] 5cef9b: [axe] Add todos.

0 views

Skip to first unread message

Eric W. Smith

unread,

Nov 25, 2025, 11:18:02 PM (12 days ago) Nov 25

to acl2-...@googlegroups.com

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 5cef9b3f31dc8aa6b1c1f851a66d5e30a65c92f9
https://github.com/acl2/acl2/commit/5cef9b3f31dc8aa6b1c1f851a66d5e30a65c92f9
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-21 (Fri, 21 Nov 2025)

Changed paths:
M books/kestrel/axe/conjunctions-and-disjunctions.lisp

Log Message:
-----------
[axe] Add todos.

Commit: 5cfa67b630d633d8ca1cd4ae8335d739f218b653
https://github.com/acl2/acl2/commit/5cfa67b630d633d8ca1cd4ae8335d739f218b653
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-21 (Fri, 21 Nov 2025)

Changed paths:
M books/kestrel/axe/prove-with-stp-tests.lisp

Log Message:
-----------
[axe] Add some tests.

Commit: 5af94922b425d9a40f3fc76f401d16001e3d9c08
https://github.com/acl2/acl2/commit/5af94922b425d9a40f3fc76f401d16001e3d9c08
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-21 (Fri, 21 Nov 2025)

Changed paths:
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/tag-generation.lisp
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
M books/kestrel/c/language/execution-without-function-calls.lisp
M books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp

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

Commit: e386747a741421e1473839e7c6f1ffdc122f9d92
https://github.com/acl2/acl2/commit/e386747a741421e1473839e7c6f1ffdc122f9d92
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-21 (Fri, 21 Nov 2025)

Changed paths:
M books/kestrel/axe/conjunctions-and-disjunctions.lisp

Log Message:
-----------
[axe] Tweak comments.

Commit: 8e8fcde000c42a860ae7b34b65b311876476f571
https://github.com/acl2/acl2/commit/8e8fcde000c42a860ae7b34b65b311876476f571
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-21 (Fri, 21 Nov 2025)

Changed paths:
M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/node-replacement-array3.lisp
M books/kestrel/axe/prove-with-stp.lisp

Log Message:
-----------
[axe] Improve implementation.

Strengthen axe-conjunctionp and axe-disjunctionp to disallow duplicated elements.

Commit: 76fbcfd732297ba055657b1e9bfca1af7f83bbf8
https://github.com/acl2/acl2/commit/76fbcfd732297ba055657b1e9bfca1af7f83bbf8
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-21 (Fri, 21 Nov 2025)

Changed paths:
M books/kestrel/axe/conjunctions-and-disjunctions.lisp

Log Message:
-----------
[axe] Improve implementation.

Rename dag-item-measure to darg-measure.

Commit: 9d4f4d44695cbbb95fe418dff25580a961590d38
https://github.com/acl2/acl2/commit/9d4f4d44695cbbb95fe418dff25580a961590d38
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-21 (Fri, 21 Nov 2025)

Changed paths:
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/x86/unroller.lisp

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

Commit: bedbb04ef45d23827672b2f05ff54c2673548b26
https://github.com/acl2/acl2/commit/bedbb04ef45d23827672b2f05ff54c2673548b26
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-21 (Fri, 21 Nov 2025)

Changed paths:
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/unroller.lisp
A books/kestrel/utilities/untranslate-dollar-list.lisp
M books/kestrel/x86/package.lsp
M books/kestrel/x86/parsers/parse-executable.lisp
M books/kestrel/x86/parsers/parse-pe-file.lisp

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

Commit: b1361c6443db3dcd9bf58fcee0f8ae2f9a932551
https://github.com/acl2/acl2/commit/b1361c6443db3dcd9bf58fcee0f8ae2f9a932551
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-21 (Fri, 21 Nov 2025)

Changed paths:
M books/build/doc.lisp
M books/kestrel/arm/arm32.lisp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/axe/x86/evaluator-x86.lisp
M books/kestrel/bv-lists/bits-and-bytes-inversions-little.lisp
M books/kestrel/bv-lists/bits-and-bytes-inversions.lisp
M books/kestrel/bv-lists/bits-to-byte-little-rules.lisp
M books/kestrel/bv-lists/packbv-and-unpackbv.lisp
M books/kestrel/bv-lists/packbv-theorems.lisp
M books/kestrel/bv-lists/packbv.lisp
M books/kestrel/bv-lists/packing.lisp
M books/kestrel/bv-lists/unpackbv.lisp
M books/kestrel/bv/bitwise.lisp
M books/kestrel/bv/bvashr.lisp
M books/kestrel/bv/bvcat-rules.lisp
M books/kestrel/bv/bvcat.lisp
M books/kestrel/bv/bvshl.lisp
M books/kestrel/bv/bvsx-rules.lisp
M books/kestrel/bv/if-becomes-bvif-rules.lisp
M books/kestrel/bv/leftrotate-rules.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/leftrotate32.lisp
M books/kestrel/bv/logext.lisp
M books/kestrel/bv/pick-a-bit.lisp
M books/kestrel/bv/putbits.lisp
M books/kestrel/bv/rightrotate.lisp
M books/kestrel/bv/rotate.lisp
M books/kestrel/bv/rtl.lisp
M books/kestrel/bv/rules12.lisp
M books/kestrel/bv/rules6.lisp
M books/kestrel/bv/trim-elim-rules-bv.lisp
M books/kestrel/bv/trim-intro-rules.lisp
M books/kestrel/bv/unsigned-byte-p-forced-rules.lisp
M books/kestrel/crypto/blake/blake2b.lisp
M books/kestrel/crypto/blake/blake2s.lisp
M books/kestrel/crypto/keccak/keccak.lisp
M books/kestrel/ethereum/evm/evm.lisp
M books/kestrel/floats/ieee-floats-as-bvs.lisp
M books/kestrel/floats/rtl.lisp
M books/kestrel/x86/support.lisp
M books/projects/aleo/vm/circuits/axe/blake2s1round.lisp
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp

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

Commit: 45f2449ca2eed632eac700bf8293f6dfbc18c431
https://github.com/acl2/acl2/commit/45f2449ca2eed632eac700bf8293f6dfbc18c431
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-21 (Fri, 21 Nov 2025)

Changed paths:
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/prove-with-stp-tests.lisp

Log Message:
-----------
[axe] Improve extraction of conjunctions and disjunctions.

Commit: 356eaae5425137ca6e308744c178edcb2eb7d61f
https://github.com/acl2/acl2/commit/356eaae5425137ca6e308744c178edcb2eb7d61f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-22 (Sat, 22 Nov 2025)

Changed paths:
M books/kestrel/bv-lists/all-unsigned-byte-p.lisp
M books/kestrel/bv-lists/bv-list-read-chunk-little.lisp
M books/kestrel/bv-lists/bvxor-list.lisp
M books/kestrel/bv-lists/byte-to-bits.lisp
M books/kestrel/bv-lists/bytes-to-bits.lisp
M books/kestrel/bv-lists/packbv-def.lisp
M books/kestrel/bv-lists/packbv-little.lisp
M books/kestrel/bv-lists/packbvs-little.lisp
M books/kestrel/bv-lists/packbvs.lisp
M books/kestrel/bv-lists/unpackbv.lisp
M books/kestrel/bv-lists/unsigned-byte-listp.lisp
M books/kestrel/crypto/blake/blake-256.lisp
M books/kestrel/crypto/ecdsa/deterministic-ecdsa-secp256k1.lisp
M books/kestrel/crypto/sha-2/sha-256.lisp
M books/kestrel/crypto/sha-2/sha-512.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/typed-lists-light/integer-listp.lisp
A books/kestrel/typed-lists-light/integer-listp2.lisp
M books/kestrel/typed-lists-light/top.lisp

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

Commit: 6e8f84e54c26ac9db0361fcedbbcd7e22d278f45
https://github.com/acl2/acl2/commit/6e8f84e54c26ac9db0361fcedbbcd7e22d278f45
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M axioms.lisp
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/tag-generation.lisp
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
M books/kestrel/c/language/execution-without-function-calls.lisp
M books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp
M books/system/doc/acl2-doc.lisp
M books/system/tests/brr-data-log.txt
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M history-management.lisp
M other-events.lisp
M rewrite.lisp

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

Commit: 0129e149bb0c56959c2fc620eb15ba6f1a25912f
https://github.com/acl2/acl2/commit/0129e149bb0c56959c2fc620eb15ba6f1a25912f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/axe/prove-with-stp.lisp

Log Message:
-----------
[axe] Improve printing.

Commit: e97a0e88d08fd09349b3c4d0f0d914675f982385
https://github.com/acl2/acl2/commit/e97a0e88d08fd09349b3c4d0f0d914675f982385
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/axe/prove-with-stp-tests.lisp

Log Message:
-----------
[axe] Add tests.

Commit: 9a9904c51e30de67c8a70b8581b514ec13b1ac92
https://github.com/acl2/acl2/commit/9a9904c51e30de67c8a70b8581b514ec13b1ac92
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/axe/conjunctions-and-disjunctions.lisp

Log Message:
-----------
[axe] Remove done todo.

Commit: e5ce78e5d18b4b6c81e9fb4509d25411600e9b24
https://github.com/acl2/acl2/commit/e5ce78e5d18b4b6c81e9fb4509d25411600e9b24
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/bv-lists/top.lisp

Log Message:
-----------
[bv-lists] Add book to top.lisp

Commit: 70d68a73d755859128eeb4dfde02cbd2bf9a75fe
https://github.com/acl2/acl2/commit/70d68a73d755859128eeb4dfde02cbd2bf9a75fe
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/bv/bif.lisp
M books/kestrel/bv/bit-to-bool.lisp
M books/kestrel/bv/bitnot.lisp
M books/kestrel/bv/bitwise.lisp
M books/kestrel/bv/bitxnor.lisp
M books/kestrel/bv/bool-to-bit.lisp
M books/kestrel/bv/bvnot.lisp
M books/kestrel/bv/rules12.lisp
M books/kestrel/bv/std.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/prime-fields/bv-rules-axe.lisp

Log Message:
-----------
[bv] Reduce includes.

Commit: 9689a5a61686c60eec2fa412c7a869f716ecbd7b
https://github.com/acl2/acl2/commit/9689a5a61686c60eec2fa412c7a869f716ecbd7b
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/doc/practices.lisp
M books/kestrel/axe/axe-rules-mixed.lisp
A books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/rules3.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/x86/package.lsp
M books/kestrel/x86/tools/lifter-support.lisp
M books/quicklisp/top.lisp

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

Commit: f16fee3f81b9936edc0b020f2db5885a0e6f1597
https://github.com/acl2/acl2/commit/f16fee3f81b9936edc0b020f2db5885a0e6f1597
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-25 (Tue, 25 Nov 2025)

Changed paths:
M books/kestrel/bv/bvminus-rules.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/validation-stp.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp

Log Message:
-----------
[bv] Reduce inclusion of bvplus book.

Commit: a313551efed3a18bbbdc9c75b3250c4f2ba9a9ba
https://github.com/acl2/acl2/commit/a313551efed3a18bbbdc9c75b3250c4f2ba9a9ba
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-25 (Tue, 25 Nov 2025)

Changed paths:
M books/kestrel/axe/unguarded-defuns.lisp

Log Message:
-----------
[axe] Reduce includes.

Compare: https://github.com/acl2/acl2/compare/10ecd0cefc42...a313551efed3

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

acl2buildserver

unread,

Nov 26, 2025, 12:52:19 AM (12 days ago) Nov 26

to acl2-...@googlegroups.com

Branch: refs/heads/master

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

Date: 2025-11-25 (Tue, 25 Nov 2025)

Changed paths:

M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/node-replacement-array3.lisp

M books/kestrel/axe/prove-with-stp-tests.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/bv-lists/top.lisp

M books/kestrel/bv/bif.lisp
M books/kestrel/bv/bit-to-bool.lisp
M books/kestrel/bv/bitnot.lisp
M books/kestrel/bv/bitwise.lisp
M books/kestrel/bv/bitxnor.lisp
M books/kestrel/bv/bool-to-bit.lisp

M books/kestrel/bv/bvminus-rules.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvnot.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/rules12.lisp
M books/kestrel/bv/std.lisp
M books/kestrel/bv/validation-stp.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp

M books/kestrel/prime-fields/bv-rules-axe.lisp

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

Merge commit 'a313551efed3a18bbbdc9c75b3250c4f2ba9a9ba' into HEAD

Compare: https://github.com/acl2/acl2/compare/0d043185a65c...e1ac360f5950

acl2buildserver

unread,

Nov 26, 2025, 12:52:38 AM (12 days ago) Nov 26

to acl2-...@googlegroups.com

Branch: refs/heads/testing

acl2buildserver

unread,

Nov 28, 2025, 9:20:20 AM (10 days ago) Nov 28

to acl2-...@googlegroups.com

Branch: refs/heads/testing-acl2s

Commit: fc6b353180667ce8e13de887e5aaf044684c2d69
https://github.com/acl2/acl2/commit/fc6b353180667ce8e13de887e5aaf044684c2d69

Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:

M books/kestrel/axe/rule-lists.lisp

Log Message:
-----------
[axe] Build in equal-of-bvsx-and-constant.

Commit: 6f6bf836d9584e5c2174af1ea782ca72faf10e4c
https://github.com/acl2/acl2/commit/6f6bf836d9584e5c2174af1ea782ca72faf10e4c

Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-25 (Tue, 25 Nov 2025)

Changed paths:

Merge.

Commit: 83dacca7c5b375fb4ea1c774f8d80c0742e8596c
https://github.com/acl2/acl2/commit/83dacca7c5b375fb4ea1c774f8d80c0742e8596c
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/integer-length.lisp

Log Message:
-----------
[arithmetic-light] Add 2 rules.

Commit: e361b2cbde30cd2bc2bfc1d361043966549d13bb
https://github.com/acl2/acl2/commit/e361b2cbde30cd2bc2bfc1d361043966549d13bb
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/array-patterns.lisp

Log Message:
-----------
[bv-lists/axe] Add more rules to shorten arrays.

Commit: 2358dbaa807a25b31971d96b8f5ad1d49f07f055
https://github.com/acl2/acl2/commit/2358dbaa807a25b31971d96b8f5ad1d49f07f055
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/support.lisp

Log Message:
-----------
[axe/x86] Improve rules.

Commit: e1fd756d462cd588bcb3ab5f7bc80d31da045466
https://github.com/acl2/acl2/commit/e1fd756d462cd588bcb3ab5f7bc80d31da045466
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/bv/bvlt.lisp

Log Message:
-----------
[bv] Organize rules.

Commit: 22cc9f8fa90c8f58603d4390585b0a01921ff5bd
https://github.com/acl2/acl2/commit/22cc9f8fa90c8f58603d4390585b0a01921ff5bd
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/rules3.lisp

Log Message:
-----------
[axe] Add todo.

Commit: c2337970409f2467e710dca64843bd9723bc8fe6
https://github.com/acl2/acl2/commit/c2337970409f2467e710dca64843bd9723bc8fe6
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/x86-rules.lisp
A books/kestrel/x86/support64.lisp
M books/kestrel/x86/top.lisp

Log Message:
-----------
[axe/x86] Organize some rules.

Commit: 291f9dee9dfe61322f8117ddd9f7b13f2ed69fbe
https://github.com/acl2/acl2/commit/291f9dee9dfe61322f8117ddd9f7b13f2ed69fbe

Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/integer-length.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv/bvlt.lisp

Log Message:
-----------
Merge commit '22cc9f8fa90c8f58603d4390585b0a01921ff5bd' into HEAD

Commit: afb36f36608395f8d1121e91a1744034150928cd
https://github.com/acl2/acl2/commit/afb36f36608395f8d1121e91a1744034150928cd
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp

Log Message:
-----------
[axe/x86] Comment out rule.

Commit: 4f7504ea70b04a7bd9ed43550aa3f398a6091d2a
https://github.com/acl2/acl2/commit/4f7504ea70b04a7bd9ed43550aa3f398a6091d2a
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/integer-length.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv/bvlt.lisp

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

Commit: 2e73b603578429e91d218415dab9d77d9be0b098
https://github.com/acl2/acl2/commit/2e73b603578429e91d218415dab9d77d9be0b098

Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2025-11-26 (Wed, 26 Nov 2025)

Changed paths:
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/x86-rules.lisp
A books/kestrel/x86/support64.lisp
M books/kestrel/x86/top.lisp

Log Message:
-----------
Merge commit '4f7504ea70b04a7bd9ed43550aa3f398a6091d2a' into HEAD

Compare: https://github.com/acl2/acl2/compare/0d043185a65c...2e73b6035784

Alessandro Coglio

unread,

Dec 1, 2025, 4:21:39 AM (7 days ago) Dec 1

to acl2-...@googlegroups.com

Branch: refs/heads/testing-user-01

Commit: 1c9957a1d0514388a1c5341e98bc23d59e751acd
https://github.com/acl2/acl2/commit/1c9957a1d0514388a1c5341e98bc23d59e751acd
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-23 (Sun, 23 Nov 2025)

Changed paths:
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp

Log Message:
-----------
[aleo] Work around GCL issue.

Commit: 7fc5284692f80077472ed327b016978a1cb9c094
https://github.com/acl2/acl2/commit/7fc5284692f80077472ed327b016978a1cb9c094

Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2025-11-23 (Sun, 23 Nov 2025)

Changed paths:
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp

Log Message:
-----------
Merge commit '1c9957a1d0514388a1c5341e98bc23d59e751acd' into HEAD

Commit: d3d0e0c2ff496e6516e361c81445f3e29ddb7dfc
https://github.com/acl2/acl2/commit/d3d0e0c2ff496e6516e361c81445f3e29ddb7dfc

Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:

M books/kestrel/axe/rules3.lisp

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

[axe] Add comment.

Commit: 79280215d45c627fe422669582d7524b626a9b0d
https://github.com/acl2/acl2/commit/79280215d45c627fe422669582d7524b626a9b0d

Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:

A books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/x86/package.lsp

Log Message:
-----------
[axe] Pull out common lists of imported symbols.

Commit: c5df6ce95d51ae90561aa961118a0420bfcb61b3
https://github.com/acl2/acl2/commit/c5df6ce95d51ae90561aa961118a0420bfcb61b3
Author: Grant Jurgensen <gr...@jurgensen.dev>

Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
[doc] Update best-practices advice on predicates

Provide more concrete advice on naming predicates.

Commit: cd539c07efb92686f81e0b63618ff5599fc7b04c
https://github.com/acl2/acl2/commit/cd539c07efb92686f81e0b63618ff5599fc7b04c
Author: Grant Jurgensen <gr...@jurgensen.dev>

Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:

M books/quicklisp/top.lisp

Log Message:
-----------
[doc] Update osicat build failure advice

Replace advice with a more succinct command.

Commit: 2e3b4d982d3b24adb2c9313b3c331c742ac5ad2f
https://github.com/acl2/acl2/commit/2e3b4d982d3b24adb2c9313b3c331c742ac5ad2f

Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:

M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/x86/package.lsp

Log Message:
-----------
[axe] Continue improving packages.

Commit: 238b8848f159ba0de72d656b9613279c964ddb36
https://github.com/acl2/acl2/commit/238b8848f159ba0de72d656b9613279c964ddb36

Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/doc/practices.lisp

M books/quicklisp/top.lisp

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

Commit: cebe6962b86cd850f0a82bf18362b1f64d8f8723
https://github.com/acl2/acl2/commit/cebe6962b86cd850f0a82bf18362b1f64d8f8723

Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:

M books/kestrel/x86/tools/lifter-support.lisp

Log Message:
-----------
[axe/x86] Improve lifter.

Support :rip as the output-indicator, to allow extracting the final program counter.

Commit: aba164d76db88e385ad7bd646f2236c408b18fbb
https://github.com/acl2/acl2/commit/aba164d76db88e385ad7bd646f2236c408b18fbb

Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:

M books/kestrel/axe/rules3.lisp
M books/kestrel/bv/bvuminus.lisp

Log Message:
-----------
[bv] Add some rules.

These include commutativity rules for bvplus that treat bvuminus as invisible, and other related rules.

Commit: 602526fe68856bd4f48ab56577fcd0e3efd95817
https://github.com/acl2/acl2/commit/602526fe68856bd4f48ab56577fcd0e3efd95817

Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:

M books/kestrel/axe/axe-rules-mixed.lisp

Log Message:
-----------
[axe] Tweak hints.

Commit: 10ecd0cefc427785d8a96940b26e63c31c8ab2bd
https://github.com/acl2/acl2/commit/10ecd0cefc427785d8a96940b26e63c31c8ab2bd

Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:

M books/kestrel/x86/tools/lifter-support.lisp

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

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

Date: 2025-11-25 (Tue, 25 Nov 2025)

Changed paths:

M axioms.lisp
M books/system/doc/acl2-doc.lisp
M defthm.lisp

M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

M rewrite.lisp

Log Message:
-----------
Fixed bugs involving large arrays not created by defstobj due to :non-executable t and in :pr.

Quoting :DOC note-8-7:

Fixed a bug that was causing errors for [stobj]s introduced with
[defstobj] keyword argument :non-executable t in the presence of
large arrays. This should not have caused an error, since that
keyword argument prevents attempts at contructing the stobj (with
its arrays).

Fixed a bug in :[pr] to work on function symbols introduced by
[defstobj] (GitHub Issue 1851). Thanks to David Taylor for
reporting this bug.

Quoting an implementation-level comment in (defxdoc note-8-7 ...):

; Fixed function find-rules-of-rune to work on runes introduced by defstobj.
; This is related to the fix for :pr: both use a new function,
; world-to-next-non-deeper-event, in place of world-to-next-event.

Commit: 4f6e129b834256cb458eb00e8a2d9a554c005eef
https://github.com/acl2/acl2/commit/4f6e129b834256cb458eb00e8a2d9a554c005eef