[acl2/acl2] 2102c7: [axe/x86] Comment out unneeded rules.

[Eric W. Smith]

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

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

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


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

Changed paths:
M books/kestrel/utilities/if.lisp

Log Message:
-----------
[utilities] Add a rule about IF.


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

Changed paths:
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

Log Message:
-----------
[x86] Refactor to reduce includes of read-and-write book.


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

Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
A books/kestrel/c/transformation/tests/struct-type-split/self-ref-checks.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

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


Commit: 6c629373f294b2061e30f5f0e785e25ffd422529
https://github.com/acl2/acl2/commit/6c629373f294b2061e30f5f0e785e25ffd422529
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: fb4962296524ef7c228a0ab106a68189034a4835
https://github.com/acl2/acl2/commit/fb4962296524ef7c228a0ab106a68189034a4835
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

Log Message:
-----------
[arithmetic-light] Add/improve various rules.

Especially to handle negative values better (e.g., in cancellation and linear rules).


Compare: https://github.com/acl2/acl2/compare/817659a7a9a3...fb4962296524

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

[Eric W. Smith]

Branch: refs/heads/master

[Eric W. Smith]

Branch: refs/heads/testing