[acl2/acl2] 6dbbec: [axe] Improve and clarify rules for introducing bvlt.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 6dbbec74c3d1e6ee838f84ada43cb7e3d9578685
https://github.com/acl2/acl2/commit/6dbbec74c3d1e6ee838f84ada43cb7e3d9578685
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-16 (Fri, 16 Jan 2026)

Changed paths:
M books/kestrel/axe/bv-intro-rules.lisp

Log Message:
-----------
[axe] Improve and clarify rules for introducing bvlt.


Commit: 7c40bb6018c76e1a8fa419852ace79cf922b629d
https://github.com/acl2/acl2/commit/7c40bb6018c76e1a8fa419852ace79cf922b629d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-16 (Fri, 16 Jan 2026)

Changed paths:
M books/kestrel/axe/hit-counts.lisp

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


Commit: d4380b40703002f7de64d597ba4ef01cc24426bc
https://github.com/acl2/acl2/commit/d4380b40703002f7de64d597ba4ef01cc24426bc
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-18 (Sun, 18 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor.lisp

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


Commit: 0a86e405f43596e81b61b3033ce44062e989dc02
https://github.com/acl2/acl2/commit/0a86e405f43596e81b61b3033ce44062e989dc02
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-18 (Sun, 18 Jan 2026)

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

Log Message:
-----------
[axe/x86] Improve rule-lists.


Commit: eed6ae1d7284f8e9615ec727c047e8eb262864b5
https://github.com/acl2/acl2/commit/eed6ae1d7284f8e9615ec727c047e8eb262864b5
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-19 (Mon, 19 Jan 2026)

Changed paths:
M books/kestrel/axe/equivalence-checker.lisp
R books/kestrel/axe/evaluator-support.lisp
M books/kestrel/axe/evaluator.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/prune-term.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester-rules.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/unroller.acl2
M books/kestrel/axe/x86/unroller.lisp

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


Commit: e85f7af71d5e15f0e98d8938f6978ada1693d6bd
https://github.com/acl2/acl2/commit/e85f7af71d5e15f0e98d8938f6978ada1693d6bd
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-19 (Mon, 19 Jan 2026)

Changed paths:
M books/GNUmakefile
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh
M books/system/doc/acl2-doc.lisp

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


Commit: 7e0b48767bafa89dd6dfe6a1f9ff376f24a7a793
https://github.com/acl2/acl2/commit/7e0b48767bafa89dd6dfe6a1f9ff376f24a7a793
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-19 (Mon, 19 Jan 2026)

Changed paths:
M books/projects/x86isa/machine/cert.acl2
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2

Log Message:
-----------
[X86ISA] Drop unneeded :skip-proofs-okp nil from .acl2 files.

As discussed on Zulip. Nil is the default for :skip-proofs-okp.


Commit: a29f8489845ae5633fb7030c82a59e5e127b8b4c
https://github.com/acl2/acl2/commit/a29f8489845ae5633fb7030c82a59e5e127b8b4c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-19 (Mon, 19 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp

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


Compare: https://github.com/acl2/acl2/compare/fbf51ad20473...a29f8489845a

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

[acl2buildserver]

Branch: refs/heads/master

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

Date: 2026-01-19 (Mon, 19 Jan 2026)

Changed paths:

M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/hit-counts.lisp
M books/kestrel/axe/x86/rule-lists.lisp

M books/projects/x86isa/machine/cert.acl2
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2

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

Merge commit 'a29f8489845ae5633fb7030c82a59e5e127b8b4c' into HEAD


Compare: https://github.com/acl2/acl2/compare/b66c1d0846df...040538c28045

[acl2buildserver]

Branch: refs/heads/testing