[acl2/acl2] c83b86: [axe] Add a rule.
0 views
Skip to first unread message
Eric W. Smith
Aug 18, 2026, 3:37:57 AM (yesterday) Aug 18
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: c83b868a94256968985e28eac81172fd179e16c5
https://github.com/acl2/acl2/commit/c83b868a94256968985e28eac81172fd179e16c5
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/rules3.lisp
Log Message:
-----------
[axe] Add a rule.
Commit: 061776238905f2a1956eb7b7e20ee8aa66b54af3
https://github.com/acl2/acl2/commit/061776238905f2a1956eb7b7e20ee8aa66b54af3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/unroller.lisp
A books/kestrel/remora/abstract-syntax-haskell.lisp
M books/kestrel/remora/abstract-syntax.lisp
Log Message:
-----------
Merge.
Commit: 9c2850c330ec24673d3b397400ba02bbfd3ac6a4
https://github.com/acl2/acl2/commit/9c2850c330ec24673d3b397400ba02bbfd3ac6a4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/apt/simplify-conjunctions.lisp
Log Message:
-----------
[apt] Improve simplify-conjunctions.
Add :monitor option. Remove guard holders from body before simplifying. Improve theory used for proofs.
Commit: 9c85e01e113f85f79696b51f6f25bd51ab41758d
https://github.com/acl2/acl2/commit/9c85e01e113f85f79696b51f6f25bd51ab41758d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
A books/kestrel/c/transformation/struct-type-split-proofs0.lisp
A books/kestrel/c/transformation/struct-type-split-proofs1.lisp
A books/kestrel/c/transformation/struct-type-split-proofs2.lisp
A books/kestrel/c/transformation/tests/struct-type-split/gso.c
R books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/fresh-variable-operations.lisp
M books/kestrel/remora/identifier-syntax.lisp
A books/kestrel/remora/ispace-equivalence-infrules.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/static-semantics.lisp
A books/kestrel/remora/unicode.lisp
M books/kestrel/remora/unique-names-validation.lisp
A books/kestrel/remora/unique-names-well-formedness.lisp
M books/kestrel/utilities/strings/strings-codes.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser-tests.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
Commit: 518ed70daaab363f2a308e7db7a5d6cb2cad0ce4
https://github.com/acl2/acl2/commit/518ed70daaab363f2a308e7db7a5d6cb2cad0ce4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
Log Message:
-----------
[axe/arm] Add rules.
Commit: 3d6bd011f2d3a5ff157405ca9c4decbc19a84ee5
https://github.com/acl2/acl2/commit/3d6bd011f2d3a5ff157405ca9c4decbc19a84ee5
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/unroller.lisp
Log Message:
-----------
[axe/arm] Add todo.
Commit: 912bc9ff3a1596a6d87a729b8f20bd78fbafd21c
https://github.com/acl2/acl2/commit/912bc9ff3a1596a6d87a729b8f20bd78fbafd21c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/lifter-common.lisp
Log Message:
-----------
[axe] Improve DAG printing.
Allow the description to be nil and improve how the print base is handled.
Compare: https://github.com/acl2/acl2/compare/0179e638c999...912bc9ff3a15
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: c83b868a94256968985e28eac81172fd179e16c5
https://github.com/acl2/acl2/commit/c83b868a94256968985e28eac81172fd179e16c5
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/rules3.lisp
Log Message:
-----------
[axe] Add a rule.
Commit: 061776238905f2a1956eb7b7e20ee8aa66b54af3
https://github.com/acl2/acl2/commit/061776238905f2a1956eb7b7e20ee8aa66b54af3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/unroller.lisp
A books/kestrel/remora/abstract-syntax-haskell.lisp
M books/kestrel/remora/abstract-syntax.lisp
Log Message:
-----------
Merge.
Commit: 9c2850c330ec24673d3b397400ba02bbfd3ac6a4
https://github.com/acl2/acl2/commit/9c2850c330ec24673d3b397400ba02bbfd3ac6a4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/apt/simplify-conjunctions.lisp
Log Message:
-----------
[apt] Improve simplify-conjunctions.
Add :monitor option. Remove guard holders from body before simplifying. Improve theory used for proofs.
Commit: 9c85e01e113f85f79696b51f6f25bd51ab41758d
https://github.com/acl2/acl2/commit/9c85e01e113f85f79696b51f6f25bd51ab41758d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
A books/kestrel/c/transformation/struct-type-split-proofs0.lisp
A books/kestrel/c/transformation/struct-type-split-proofs1.lisp
A books/kestrel/c/transformation/struct-type-split-proofs2.lisp
A books/kestrel/c/transformation/tests/struct-type-split/gso.c
R books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/fresh-variable-operations.lisp
M books/kestrel/remora/identifier-syntax.lisp
A books/kestrel/remora/ispace-equivalence-infrules.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/static-semantics.lisp
A books/kestrel/remora/unicode.lisp
M books/kestrel/remora/unique-names-validation.lisp
A books/kestrel/remora/unique-names-well-formedness.lisp
M books/kestrel/utilities/strings/strings-codes.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser-tests.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
Commit: 518ed70daaab363f2a308e7db7a5d6cb2cad0ce4
https://github.com/acl2/acl2/commit/518ed70daaab363f2a308e7db7a5d6cb2cad0ce4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
Log Message:
-----------
[axe/arm] Add rules.
Commit: 3d6bd011f2d3a5ff157405ca9c4decbc19a84ee5
https://github.com/acl2/acl2/commit/3d6bd011f2d3a5ff157405ca9c4decbc19a84ee5
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/unroller.lisp
Log Message:
-----------
[axe/arm] Add todo.
Commit: 912bc9ff3a1596a6d87a729b8f20bd78fbafd21c
https://github.com/acl2/acl2/commit/912bc9ff3a1596a6d87a729b8f20bd78fbafd21c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/lifter-common.lisp
Log Message:
-----------
[axe] Improve DAG printing.
Allow the description to be nil and improve how the print base is handled.
Compare: https://github.com/acl2/acl2/compare/0179e638c999...912bc9ff3a15
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Eric W. Smith
2:17 PM (6 hours ago) 2:17 PM
to acl2-...@googlegroups.com
Branch: refs/heads/master
https://github.com/acl2/acl2/commit/a4b406f083f1ef6ce0e1a0d09ae496037a121757
Author: Alessandro Coglio <em...@alessandrocoglio.info>
A books/kestrel/remora/ispace-equivalence-infrules.lisp
M books/kestrel/remora/static-semantics.lisp
Log Message:
-----------
[Remora] Rename a file and topic.
Commit: 061776238905f2a1956eb7b7e20ee8aa66b54af3
https://github.com/acl2/acl2/commit/061776238905f2a1956eb7b7e20ee8aa66b54af3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/unroller.lisp
A books/kestrel/remora/abstract-syntax-haskell.lisp
M books/kestrel/remora/abstract-syntax.lisp
Log Message:
-----------
Merge.
Commit: 2d5a9b32d5790e589a63f715ddb2ac09559b5ed7
https://github.com/acl2/acl2/commit/2d5a9b32d5790e589a63f715ddb2ac09559b5ed7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Improve some predicate names.
Commit: 313fbf5280e12f4c9939fdac1cac0c20fae7abac
https://github.com/acl2/acl2/commit/313fbf5280e12f4c9939fdac1cac0c20fae7abac
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Add some explanatory comments.
Commit: 0a336ba3a0c4e0a4d19400417dd9d180d5bd2e10
https://github.com/acl2/acl2/commit/0a336ba3a0c4e0a4d19400417dd9d180d5bd2e10
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Start rules for shape/ispace equivalence.
Commit: 0dcab15ae91d6272b3528f6e2def15066eeac0bf
https://github.com/acl2/acl2/commit/0dcab15ae91d6272b3528f6e2def15066eeac0bf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Add some shape normalization rules.
Commit: 35b9e4c9df71a1ad583a9e38fd679b8f6e3f9ed9
https://github.com/acl2/acl2/commit/35b9e4c9df71a1ad583a9e38fd679b8f6e3f9ed9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Improve some layout and variable names.
Commit: cf06ed65e9aa54d84c06c319b5998ab46fd60fd9
https://github.com/acl2/acl2/commit/cf06ed65e9aa54d84c06c319b5998ab46fd60fd9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Add normalization rules for `++`.
Commit: 939355ead356bac5c7f4f27785539b4c7989e9aa
https://github.com/acl2/acl2/commit/939355ead356bac5c7f4f27785539b4c7989e9aa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Add rules for splice normalization.
Commit: 8b045d1431e9212b93aff61a0138687576041c83
https://github.com/acl2/acl2/commit/8b045d1431e9212b93aff61a0138687576041c83
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Add rules for free monoid properties.
Commit: 79fa093d857cd44b38cd1212cca4cca34bc77419
https://github.com/acl2/acl2/commit/79fa093d857cd44b38cd1212cca4cca34bc77419
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Fix some typos and layout.
Commit: 4d97e525ed332d06e15486fc43a598734906f694
https://github.com/acl2/acl2/commit/4d97e525ed332d06e15486fc43a598734906f694
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Simplify two inference rule names.
Commit: db06304e601c62f76ada4c0953ca7d420b848cab
https://github.com/acl2/acl2/commit/db06304e601c62f76ada4c0953ca7d420b848cab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
We still calculate those events, but we do not submit them to ACL2, we do not
describe them in the user documentation, and we do not expect them in the tests.
This is a step towards eventual removal, but we keep the code around a little
longer, just in case.
Commit: 7f9c70260afb61b02202fd1ddc16aeda38b911b5
https://github.com/acl2/acl2/commit/7f9c70260afb61b02202fd1ddc16aeda38b911b5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Add mising bridge rule.
Commit: 4a7b4a847b1afc72c9e6a4b249f92858bfd0fe9c
https://github.com/acl2/acl2/commit/4a7b4a847b1afc72c9e6a4b249f92858bfd0fe9c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/support.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv/bvminus.lisp
A books/kestrel/remora/abstract-syntax-haskell.lisp
M books/kestrel/remora/abstract-syntax.lisp
https://github.com/acl2/acl2/commit/9efecef4a446f50c88f471657aa6d077a89b2ed5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Tweak for consistent layout.
Commit: c46375845fb36a54cc0a90f739c37eaec2db7928
https://github.com/acl2/acl2/commit/c46375845fb36a54cc0a90f739c37eaec2db7928
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[Remora] Simply two inference rules.
Commit: 0179e638c999bee9cf7fec515bd0e7b1e70b87d7
https://github.com/acl2/acl2/commit/0179e638c999bee9cf7fec515bd0e7b1e70b87d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
M books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/monomorphize.lisp
Commit: dbf80f0247816ad20ef214ec06a2182e2299c991
https://github.com/acl2/acl2/commit/dbf80f0247816ad20ef214ec06a2182e2299c991
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
Commit: 50615d309f20dfdb555270b19706c2b8992c3f35
https://github.com/acl2/acl2/commit/50615d309f20dfdb555270b19706c2b8992c3f35
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/state.lisp
Log Message:
-----------
[arm] Add *fp* constant.
Commit: a460a2eedd32f2c02ec528b5958cd61cb61e2595
https://github.com/acl2/acl2/commit/a460a2eedd32f2c02ec528b5958cd61cb61e2595
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp
Commit: f417e51c25a9e6e296294de1750ce7a452901af7
https://github.com/acl2/acl2/commit/f417e51c25a9e6e296294de1750ce7a452901af7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Remove code now unused.
Commit: 15eed9b3e0391fe0989d264e1f811ff2df6a36b9
https://github.com/acl2/acl2/commit/15eed9b3e0391fe0989d264e1f811ff2df6a36b9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Update some doc.
Commit: ed901e0a58e0a57f686188e35355d0a5b35928a4
https://github.com/acl2/acl2/commit/ed901e0a58e0a57f686188e35355d0a5b35928a4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Remove more code no longer needed.
Commit: 845103b2c056d954ada901a4ad3ba0c4390fccdc
https://github.com/acl2/acl2/commit/845103b2c056d954ada901a4ad3ba0c4390fccdc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Remove code no longer needed.
Commit: 9a661f635c0e2a7b7c8e444845870c98bf4acfbe
https://github.com/acl2/acl2/commit/9a661f635c0e2a7b7c8e444845870c98bf4acfbe
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/package.lsp
Log Message:
-----------
[axe/arm] Extend package.
Commit: 3c55bbdb250e38e540efa9d849ae3b49029be5c0
https://github.com/acl2/acl2/commit/3c55bbdb250e38e540efa9d849ae3b49029be5c0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Update some doc.
Commit: c523eef02b270089845e763aa9c8df6f284b3cbe
https://github.com/acl2/acl2/commit/c523eef02b270089845e763aa9c8df6f284b3cbe
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/state.lisp
M books/kestrel/axe/arm/package.lsp
M books/kestrel/axe/arm/rule-lists.lisp
Commit: 7948b818db60e1be1444ae778b2a3215f9d715f0
https://github.com/acl2/acl2/commit/7948b818db60e1be1444ae778b2a3215f9d715f0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Fix bug with incomplete struct types.
The code was expecting to always find members when looking up structures by tag,
but that is not the case with incomplete struct types, e.g. `struct
incomplete;`. This is now handled properly. The bug manifested as a crash
(internal/implementation error), not as passing unsafe code.
Thanks to Grant Jurgensen for running the checks on an example that exhibited
the problem.
Commit: 296d4ab54a8f56e4404cd82cea3a6c67eff45a22
https://github.com/acl2/acl2/commit/296d4ab54a8f56e4404cd82cea3a6c67eff45a22
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
A books/kestrel/c/transformation/tests/struct-type-split/opaque.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
Log Message:
-----------
[STS] Add test with an incomplete struct type.
This tests the bug fix in the previous commit. This test failed before the fix.
Commit: 70dac4e09c35a5c7a1b3f1db7886d866b6dbf88b
https://github.com/acl2/acl2/commit/70dac4e09c35a5c7a1b3f1db7886d866b6dbf88b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/package.lsp
https://github.com/acl2/acl2/commit/b04e14d343347fee7b854cbec410a0780594c2ee
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/step.lisp
M books/kestrel/arm/tests/simple.lisp
Commit: 32b61c59dea63b6f7e1f9851cbf66c14b15e8b19
https://github.com/acl2/acl2/commit/32b61c59dea63b6f7e1f9851cbf66c14b15e8b19
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/decoder.lisp
Log Message:
-----------
[arm] Add rule.
Commit: b2cd3f0ea63d799db1ebc2d32222d29e81aeb77a
https://github.com/acl2/acl2/commit/b2cd3f0ea63d799db1ebc2d32222d29e81aeb77a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/run-until-return.lisp
Log Message:
-----------
[axe/arm] Add todo.
Commit: 47900492d43bbdad6767fdbac8660cb1c504ed41
https://github.com/acl2/acl2/commit/47900492d43bbdad6767fdbac8660cb1c504ed41
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
A books/kestrel/arm/library-models.lisp
M books/kestrel/arm/memory.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/arm/step.lisp
M books/kestrel/arm/tests/simple.lisp
M books/kestrel/arm/top.lisp
M books/kestrel/axe/arm/package.lsp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/run-until-return.lisp
Start adding support for models of library calls, like the ones in libc.
Also add an oracle component to the state.
Commit: de3d82808c5ba6deb698ff6abb589673a78dc423
https://github.com/acl2/acl2/commit/de3d82808c5ba6deb698ff6abb589673a78dc423
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/package.lsp
Log Message:
-----------
[axe/arm] Extend package.
Commit: aa88537ddb4838fcb1aa514aaf35a8f06227387c
https://github.com/acl2/acl2/commit/aa88537ddb4838fcb1aa514aaf35a8f06227387c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/library-models.lisp
M books/kestrel/arm/step.lisp
Log Message:
-----------
[arm] Add more library models.
Commit: 19a807fea0fa3d52dbb5e4f9f39feac62279f2c8
https://github.com/acl2/acl2/commit/19a807fea0fa3d52dbb5e4f9f39feac62279f2c8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/rules.lisp
Log Message:
-----------
[arm] Add more rules about conditions.
Commit: f47ad3b6e4fcaf5dc6609edeb57aad379984ddde
https://github.com/acl2/acl2/commit/f47ad3b6e4fcaf5dc6609edeb57aad379984ddde
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/axe-rules.lisp
Commit: 8c96d41f9063b195fd717b8d72349a04c90fd722
https://github.com/acl2/acl2/commit/8c96d41f9063b195fd717b8d72349a04c90fd722
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/axe-rules.lisp
Commit: 9c0e2d66e8499ecf8f473485cabb80890b45e866
https://github.com/acl2/acl2/commit/9c0e2d66e8499ecf8f473485cabb80890b45e866
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/axe-rules.lisp
M books/kestrel/axe/arm/run-until-return.lisp
Log Message:
-----------
[axe/arm] Add run-until-reach-pc.
Commit: 9389d7d36a79c60832eebf046c7e19b24480d74b
https://github.com/acl2/acl2/commit/9389d7d36a79c60832eebf046c7e19b24480d74b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/library-models.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/arm/step.lisp
M books/kestrel/axe/arm/axe-rules.lisp
M books/kestrel/axe/arm/package.lsp
Commit: eee6783dbc03317b1e936927d164d26cacb0a730
https://github.com/acl2/acl2/commit/eee6783dbc03317b1e936927d164d26cacb0a730
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
A books/kestrel/axe/arm/run-until-return-common.lisp
M books/kestrel/axe/arm/run-until-return-with-tracing.lisp
M books/kestrel/axe/arm/run-until-return.lisp
Log Message:
-----------
[axe/arm] Refactor.
Compare: https://github.com/acl2/acl2/compare/27abad2efd5f...eee6783dbc03
Home: https://github.com/acl2/acl2
Commit: c83b868a94256968985e28eac81172fd179e16c5
https://github.com/acl2/acl2/commit/c83b868a94256968985e28eac81172fd179e16c5
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/rules3.lisp
Log Message:
-----------
[axe] Add a rule.
Commit: a4b406f083f1ef6ce0e1a0d09ae496037a121757
Commit: c83b868a94256968985e28eac81172fd179e16c5
https://github.com/acl2/acl2/commit/c83b868a94256968985e28eac81172fd179e16c5
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/rules3.lisp
Log Message:
-----------
[axe] Add a rule.
https://github.com/acl2/acl2/commit/a4b406f083f1ef6ce0e1a0d09ae496037a121757
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
R books/kestrel/remora/dimension-equivalence-infrules.lisp
Changed paths:
A books/kestrel/remora/ispace-equivalence-infrules.lisp
M books/kestrel/remora/static-semantics.lisp
Log Message:
-----------
[Remora] Rename a file and topic.
Commit: 061776238905f2a1956eb7b7e20ee8aa66b54af3
https://github.com/acl2/acl2/commit/061776238905f2a1956eb7b7e20ee8aa66b54af3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/unroller.lisp
A books/kestrel/remora/abstract-syntax-haskell.lisp
M books/kestrel/remora/abstract-syntax.lisp
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/2d5a9b32d5790e589a63f715ddb2ac09559b5ed7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Improve some predicate names.
Commit: 313fbf5280e12f4c9939fdac1cac0c20fae7abac
https://github.com/acl2/acl2/commit/313fbf5280e12f4c9939fdac1cac0c20fae7abac
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Add some explanatory comments.
Commit: 0a336ba3a0c4e0a4d19400417dd9d180d5bd2e10
https://github.com/acl2/acl2/commit/0a336ba3a0c4e0a4d19400417dd9d180d5bd2e10
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Start rules for shape/ispace equivalence.
Commit: 0dcab15ae91d6272b3528f6e2def15066eeac0bf
https://github.com/acl2/acl2/commit/0dcab15ae91d6272b3528f6e2def15066eeac0bf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Add some shape normalization rules.
Commit: 35b9e4c9df71a1ad583a9e38fd679b8f6e3f9ed9
https://github.com/acl2/acl2/commit/35b9e4c9df71a1ad583a9e38fd679b8f6e3f9ed9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Improve some layout and variable names.
Commit: cf06ed65e9aa54d84c06c319b5998ab46fd60fd9
https://github.com/acl2/acl2/commit/cf06ed65e9aa54d84c06c319b5998ab46fd60fd9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Add normalization rules for `++`.
Commit: 939355ead356bac5c7f4f27785539b4c7989e9aa
https://github.com/acl2/acl2/commit/939355ead356bac5c7f4f27785539b4c7989e9aa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Add rules for splice normalization.
Commit: 8b045d1431e9212b93aff61a0138687576041c83
https://github.com/acl2/acl2/commit/8b045d1431e9212b93aff61a0138687576041c83
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Add rules for free monoid properties.
Commit: 79fa093d857cd44b38cd1212cca4cca34bc77419
https://github.com/acl2/acl2/commit/79fa093d857cd44b38cd1212cca4cca34bc77419
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Fix some typos and layout.
Commit: 4d97e525ed332d06e15486fc43a598734906f694
https://github.com/acl2/acl2/commit/4d97e525ed332d06e15486fc43a598734906f694
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Simplify two inference rule names.
Commit: db06304e601c62f76ada4c0953ca7d420b848cab
https://github.com/acl2/acl2/commit/db06304e601c62f76ada4c0953ca7d420b848cab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Comment out `-2` events.
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
We still calculate those events, but we do not submit them to ACL2, we do not
describe them in the user documentation, and we do not expect them in the tests.
This is a step towards eventual removal, but we keep the code around a little
longer, just in case.
Commit: 7f9c70260afb61b02202fd1ddc16aeda38b911b5
https://github.com/acl2/acl2/commit/7f9c70260afb61b02202fd1ddc16aeda38b911b5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Add mising bridge rule.
Commit: 4a7b4a847b1afc72c9e6a4b249f92858bfd0fe9c
https://github.com/acl2/acl2/commit/4a7b4a847b1afc72c9e6a4b249f92858bfd0fe9c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/arm/pseudocode.lisp
Changed paths:
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/support.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv/bvminus.lisp
A books/kestrel/remora/abstract-syntax-haskell.lisp
M books/kestrel/remora/abstract-syntax.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
Commit: 9efecef4a446f50c88f471657aa6d077a89b2ed5
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/9efecef4a446f50c88f471657aa6d077a89b2ed5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Tweak for consistent layout.
Commit: c46375845fb36a54cc0a90f739c37eaec2db7928
https://github.com/acl2/acl2/commit/c46375845fb36a54cc0a90f739c37eaec2db7928
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Changed paths:
Log Message:
-----------
[Remora] Simply two inference rules.
Commit: 0179e638c999bee9cf7fec515bd0e7b1e70b87d7
https://github.com/acl2/acl2/commit/0179e638c999bee9cf7fec515bd0e7b1e70b87d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/fresh-variable-operations.lisp
Changed paths:
M books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/monomorphize.lisp
https://github.com/acl2/acl2/commit/dbf80f0247816ad20ef214ec06a2182e2299c991
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Remove some commented-out code and doc.
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Commit: 50615d309f20dfdb555270b19706c2b8992c3f35
https://github.com/acl2/acl2/commit/50615d309f20dfdb555270b19706c2b8992c3f35
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/state.lisp
Log Message:
-----------
[arm] Add *fp* constant.
Commit: a460a2eedd32f2c02ec528b5958cd61cb61e2595
https://github.com/acl2/acl2/commit/a460a2eedd32f2c02ec528b5958cd61cb61e2595
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
Log Message:
-----------
[axe/arm] Improve tracing.
Log Message:
-----------
Commit: f417e51c25a9e6e296294de1750ce7a452901af7
https://github.com/acl2/acl2/commit/f417e51c25a9e6e296294de1750ce7a452901af7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Remove code now unused.
Commit: 15eed9b3e0391fe0989d264e1f811ff2df6a36b9
https://github.com/acl2/acl2/commit/15eed9b3e0391fe0989d264e1f811ff2df6a36b9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Update some doc.
Commit: ed901e0a58e0a57f686188e35355d0a5b35928a4
https://github.com/acl2/acl2/commit/ed901e0a58e0a57f686188e35355d0a5b35928a4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Remove more code no longer needed.
Commit: 845103b2c056d954ada901a4ad3ba0c4390fccdc
https://github.com/acl2/acl2/commit/845103b2c056d954ada901a4ad3ba0c4390fccdc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Remove code no longer needed.
Commit: 9a661f635c0e2a7b7c8e444845870c98bf4acfbe
https://github.com/acl2/acl2/commit/9a661f635c0e2a7b7c8e444845870c98bf4acfbe
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/package.lsp
Log Message:
-----------
[axe/arm] Extend package.
Commit: 3c55bbdb250e38e540efa9d849ae3b49029be5c0
https://github.com/acl2/acl2/commit/3c55bbdb250e38e540efa9d849ae3b49029be5c0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Update some doc.
Commit: c523eef02b270089845e763aa9c8df6f284b3cbe
https://github.com/acl2/acl2/commit/c523eef02b270089845e763aa9c8df6f284b3cbe
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/state.lisp
M books/kestrel/axe/arm/package.lsp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
Log Message:
-----------
Merge.
Log Message:
-----------
Commit: 7948b818db60e1be1444ae778b2a3215f9d715f0
https://github.com/acl2/acl2/commit/7948b818db60e1be1444ae778b2a3215f9d715f0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Fix bug with incomplete struct types.
The code was expecting to always find members when looking up structures by tag,
but that is not the case with incomplete struct types, e.g. `struct
incomplete;`. This is now handled properly. The bug manifested as a crash
(internal/implementation error), not as passing unsafe code.
Thanks to Grant Jurgensen for running the checks on an example that exhibited
the problem.
Commit: 296d4ab54a8f56e4404cd82cea3a6c67eff45a22
https://github.com/acl2/acl2/commit/296d4ab54a8f56e4404cd82cea3a6c67eff45a22
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
A books/kestrel/c/transformation/tests/struct-type-split/opaque.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
Log Message:
-----------
[STS] Add test with an incomplete struct type.
This tests the bug fix in the previous commit. This test failed before the fix.
Commit: 70dac4e09c35a5c7a1b3f1db7886d866b6dbf88b
https://github.com/acl2/acl2/commit/70dac4e09c35a5c7a1b3f1db7886d866b6dbf88b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/package.lsp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
Commit: b04e14d343347fee7b854cbec410a0780594c2ee
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/b04e14d343347fee7b854cbec410a0780594c2ee
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/step.lisp
M books/kestrel/arm/tests/simple.lisp
M books/kestrel/axe/arm/rule-lists.lisp
Log Message:
-----------
[arm] Refactor step.
Log Message:
-----------
Commit: 32b61c59dea63b6f7e1f9851cbf66c14b15e8b19
https://github.com/acl2/acl2/commit/32b61c59dea63b6f7e1f9851cbf66c14b15e8b19
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/decoder.lisp
Log Message:
-----------
[arm] Add rule.
Commit: b2cd3f0ea63d799db1ebc2d32222d29e81aeb77a
https://github.com/acl2/acl2/commit/b2cd3f0ea63d799db1ebc2d32222d29e81aeb77a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/run-until-return.lisp
Log Message:
-----------
[axe/arm] Add todo.
https://github.com/acl2/acl2/commit/47900492d43bbdad6767fdbac8660cb1c504ed41
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
A books/kestrel/arm/library-models.lisp
M books/kestrel/arm/memory.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/arm/step.lisp
M books/kestrel/arm/tests/simple.lisp
M books/kestrel/arm/top.lisp
M books/kestrel/axe/arm/package.lsp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/run-until-return.lisp
M books/kestrel/axe/arm/unroller.lisp
Log Message:
-----------
[axe/arm] Improve ARM32 model.
Log Message:
-----------
Start adding support for models of library calls, like the ones in libc.
Also add an oracle component to the state.
Commit: de3d82808c5ba6deb698ff6abb589673a78dc423
https://github.com/acl2/acl2/commit/de3d82808c5ba6deb698ff6abb589673a78dc423
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/package.lsp
Log Message:
-----------
[axe/arm] Extend package.
Commit: aa88537ddb4838fcb1aa514aaf35a8f06227387c
https://github.com/acl2/acl2/commit/aa88537ddb4838fcb1aa514aaf35a8f06227387c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/library-models.lisp
M books/kestrel/arm/step.lisp
Log Message:
-----------
[arm] Add more library models.
Commit: 19a807fea0fa3d52dbb5e4f9f39feac62279f2c8
https://github.com/acl2/acl2/commit/19a807fea0fa3d52dbb5e4f9f39feac62279f2c8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/rules.lisp
Log Message:
-----------
[arm] Add more rules about conditions.
Commit: f47ad3b6e4fcaf5dc6609edeb57aad379984ddde
https://github.com/acl2/acl2/commit/f47ad3b6e4fcaf5dc6609edeb57aad379984ddde
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/axe-rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
Log Message:
-----------
[axe/arm] Build in more rules.
Log Message:
-----------
Commit: 8c96d41f9063b195fd717b8d72349a04c90fd722
https://github.com/acl2/acl2/commit/8c96d41f9063b195fd717b8d72349a04c90fd722
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/axe-rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
Log Message:
-----------
[axe/arm] Add more constant-openers.
Log Message:
-----------
Commit: 9c0e2d66e8499ecf8f473485cabb80890b45e866
https://github.com/acl2/acl2/commit/9c0e2d66e8499ecf8f473485cabb80890b45e866
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/axe-rules.lisp
M books/kestrel/axe/arm/run-until-return.lisp
Log Message:
-----------
[axe/arm] Add run-until-reach-pc.
Commit: 9389d7d36a79c60832eebf046c7e19b24480d74b
https://github.com/acl2/acl2/commit/9389d7d36a79c60832eebf046c7e19b24480d74b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
M books/kestrel/arm/library-models.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/arm/step.lisp
M books/kestrel/axe/arm/axe-rules.lisp
M books/kestrel/axe/arm/package.lsp
M books/kestrel/axe/arm/rule-lists.lisp
Log Message:
-----------
Merge.
Log Message:
-----------
Commit: eee6783dbc03317b1e936927d164d26cacb0a730
https://github.com/acl2/acl2/commit/eee6783dbc03317b1e936927d164d26cacb0a730
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-18 (Tue, 18 Aug 2026)
Changed paths:
A books/kestrel/axe/arm/run-until-return-common.lisp
M books/kestrel/axe/arm/run-until-return-with-tracing.lisp
M books/kestrel/axe/arm/run-until-return.lisp
Log Message:
-----------
[axe/arm] Refactor.
Compare: https://github.com/acl2/acl2/compare/27abad2efd5f...eee6783dbc03
Eric W. Smith
2:17 PM (6 hours ago) 2:17 PM
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages