[acl2/acl2] 5caedd: [bv] Add 2 cancellation rules.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 5caeddee72033edffae78d557339dcd642b72cd0
https://github.com/acl2/acl2/commit/5caeddee72033edffae78d557339dcd642b72cd0
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-12 (Wed, 12 Aug 2026)

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

Log Message:
-----------
[bv] Add 2 cancellation rules.


Commit: 6cb97ffad5fc439f9f049501f9356e330743a52a
https://github.com/acl2/acl2/commit/6cb97ffad5fc439f9f049501f9356e330743a52a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-13 (Thu, 13 Aug 2026)

Changed paths:
M books/kestrel/axe/x86/tests/ndsu/assembly/support.lisp

Log Message:
-----------
[axe/x86] Disable a rule.


Commit: 05e757a8a99f1ad45bdbf81adf7456ceeaa23c3a
https://github.com/acl2/acl2/commit/05e757a8a99f1ad45bdbf81adf7456ceeaa23c3a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-13 (Thu, 13 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-formal-subset.lisp
M books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/proof-generation.lisp

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


Commit: c5d18d90f66ea43a1f2b501236c18dfa0bb8d0a4
https://github.com/acl2/acl2/commit/c5d18d90f66ea43a1f2b501236c18dfa0bb8d0a4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-13 (Thu, 13 Aug 2026)

Changed paths:
M books/kestrel/arithmetic-light/.sys/fl...@useless-runes.lsp
M books/kestrel/arithmetic-light/divide.lisp
M books/kestrel/arithmetic-light/times.lisp
M books/kestrel/arithmetic-light/truncate.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/all-variable-operations.lisp
A books/kestrel/remora/all-variables-under-desugaring.lisp
R books/kestrel/remora/bound-and-free-variable-operations.lisp
A books/kestrel/remora/bound-variable-operations.lisp
A books/kestrel/remora/bound-variables-under-desugaring.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
A books/kestrel/remora/free-variable-operations.lisp
A books/kestrel/remora/free-variables-under-desugaring.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/kestrel/utilities/if.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
M books/kestrel/x86/support-x86.lisp
A books/kestrel/x86/support-x86b.lisp
M books/std/util/definductive.lisp

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


Commit: d1784a07240f7860c689913a0a6f0131ea7b7218
https://github.com/acl2/acl2/commit/d1784a07240f7860c689913a0a6f0131ea7b7218
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-14 (Fri, 14 Aug 2026)

Changed paths:
M books/kestrel/filepath/paths.lisp

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


Commit: d7e68fb2e93030bf5ece6047f07fce434e9c52be
https://github.com/acl2/acl2/commit/d7e68fb2e93030bf5ece6047f07fce434e9c52be
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-16 (Sun, 16 Aug 2026)

Changed paths:
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp

Log Message:
-----------
[axe/arm] Add rules.


Commit: 1d6737c4954fee57589212755a78fd34ae9d49fb
https://github.com/acl2/acl2/commit/1d6737c4954fee57589212755a78fd34ae9d49fb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-16 (Sun, 16 Aug 2026)

Changed paths:
M books/kestrel/axe/make-rewriter-simple.lisp

Log Message:
-----------
[axe] Avoid stack overflows printing huge constants.

This could happen when monitoring a rule one of whose variables was bound to a huge constant list.


Commit: c3940c01b0ada30d8844cbdc5f0c60b099689ec5
https://github.com/acl2/acl2/commit/c3940c01b0ada30d8844cbdc5f0c60b099689ec5
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] Improve unroller.

Simplify the assumptions using each other before lifting. Also, rename :untranslatep option to just :untranslate.


Commit: 06b74e0a190178fe5656c6817edf390aaf0d3e16
https://github.com/acl2/acl2/commit/06b74e0a190178fe5656c6817edf390aaf0d3e16
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)

Changed paths:
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
[axe] Rename :untranslatep options to just :untranslate.


Commit: aefd4216019a58a443b7ebedba0ae5673050bd5d
https://github.com/acl2/acl2/commit/aefd4216019a58a443b7ebedba0ae5673050bd5d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)

Changed paths:
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/support.lisp
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/booleans/booleans.lisp
M books/kestrel/booleans/boolif.lisp

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


Compare: https://github.com/acl2/acl2/compare/aeb37a331f67...aefd4216019a

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

[acl2buildserver]

Branch: refs/heads/master

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

Date: 2026-08-17 (Mon, 17 Aug 2026)

Changed paths:

M books/kestrel/arm/pseudocode.lisp
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

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

Merge commit 'aefd4216019a58a443b7ebedba0ae5673050bd5d' into HEAD


Compare: https://github.com/acl2/acl2/compare/9fe4354715a6...a516e85ca580

[acl2buildserver]

Branch: refs/heads/testing