[acl2/acl2] f3211d: [X86ISA] Move inclusion of raw Lisp code to tools/...

[Eric W. Smith]

Branch: refs/heads/x86isa-raw-lisp
Home: https://github.com/acl2/acl2
Commit: f3211d76e40db670c47c8997756aed6c10ca372b
https://github.com/acl2/acl2/commit/f3211d76e40db670c47c8997756aed6c10ca372b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/projects/x86isa/machine/cert.acl2
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/tools/execution/top.lisp

Log Message:
-----------
[X86ISA] Move inclusion of raw Lisp code to tools/execution/top.

This should allow the use of with-supporters to cherrypick certain definitions from the model. It also reduces the scope of some trust tags.



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

[Eric W. Smith]

Branch: refs/heads/testing-kestrel

Home: https://github.com/acl2/acl2
Commit: f3211d76e40db670c47c8997756aed6c10ca372b
https://github.com/acl2/acl2/commit/f3211d76e40db670c47c8997756aed6c10ca372b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/projects/x86isa/machine/cert.acl2
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/tools/execution/top.lisp

Log Message:
-----------
[X86ISA] Move inclusion of raw Lisp code to tools/execution/top.

This should allow the use of with-supporters to cherrypick certain definitions from the model. It also reduces the scope of some trust tags.

Commit: 2ddf53120d6e83bb02b5a2c398510eac34938418
https://github.com/acl2/acl2/commit/2ddf53120d6e83bb02b5a2c398510eac34938418
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>
Date: 2026-01-16 (Fri, 16 Jan 2026)

Changed paths:
M books/projects/x86isa/machine/cert.acl2
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/tools/execution/top.lisp

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

Merge pull request #1895 from acl2/x86isa-raw-lisp

[X86ISA] Move inclusion of raw Lisp code to tools/execution/top.

Compare: https://github.com/acl2/acl2/compare/82c02e583fc3...2ddf53120d6e

[Eric W. Smith]

Branch: refs/heads/master

[Eric W. Smith]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-user-01

Home: https://github.com/acl2/acl2
Commit: f3211d76e40db670c47c8997756aed6c10ca372b
https://github.com/acl2/acl2/commit/f3211d76e40db670c47c8997756aed6c10ca372b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-14 (Wed, 14 Jan 2026)

Changed paths:
M books/projects/x86isa/machine/cert.acl2
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/tools/execution/top.lisp

Log Message:
-----------
[X86ISA] Move inclusion of raw Lisp code to tools/execution/top.

This should allow the use of with-supporters to cherrypick certain definitions from the model. It also reduces the scope of some trust tags.

Commit: 789d3696f057fecbbd08f237cdcabd53ae405f30
https://github.com/acl2/acl2/commit/789d3696f057fecbbd08f237cdcabd53ae405f30
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-15 (Thu, 15 Jan 2026)

Changed paths:
M books/kestrel/axe/equivalence-checker.lisp

Log Message:
-----------
[axe] Improve equivalence-checker.

Remove a skip-proofs and reduce includes.


Commit: 11dea2d2fea54ec4da62cc629222c9b7fd04e81e
https://github.com/acl2/acl2/commit/11dea2d2fea54ec4da62cc629222c9b7fd04e81e
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-15 (Thu, 15 Jan 2026)

Changed paths:
A books/kestrel/axe/evaluator-support.lisp
M books/kestrel/axe/evaluator.lisp
M books/kestrel/axe/top.lisp

Log Message:
-----------
[axe] Factor out evaluator support material.


Commit: 8f4d65e21be59702c444ab97257a3595bc031f92
https://github.com/acl2/acl2/commit/8f4d65e21be59702c444ab97257a3595bc031f92
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-15 (Thu, 15 Jan 2026)

Changed paths:
M books/kestrel/axe/x86/unroller.acl2
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
[axe/x86] Avoid having the unroller depend on skip-proofs.


Commit: 82c02e583fc3edadec38bdc5d147db351d15afa6
https://github.com/acl2/acl2/commit/82c02e583fc3edadec38bdc5d147db351d15afa6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-15 (Thu, 15 Jan 2026)

Changed paths:
M books/kestrel/axe/x86/tester.lisp

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


Commit: 58fcb9d1df9378fbef49089e23ecdb74032f22bb
https://github.com/acl2/acl2/commit/58fcb9d1df9378fbef49089e23ecdb74032f22bb
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-01-16 (Fri, 16 Jan 2026)

Changed paths:

M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Take theorem from library.

Commit: 2ddf53120d6e83bb02b5a2c398510eac34938418
https://github.com/acl2/acl2/commit/2ddf53120d6e83bb02b5a2c398510eac34938418
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>
Date: 2026-01-16 (Fri, 16 Jan 2026)

Changed paths:
M books/projects/x86isa/machine/cert.acl2
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/tools/execution/top.lisp

Log Message:
-----------
Merge pull request #1895 from acl2/x86isa-raw-lisp

[X86ISA] Move inclusion of raw Lisp code to tools/execution/top.

Commit: 63e2609dd99cae5bcf8e1f4d3fcd22f99c76e7f4
https://github.com/acl2/acl2/commit/63e2609dd99cae5bcf8e1f4d3fcd22f99c76e7f4
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-01-16 (Fri, 16 Jan 2026)

Changed paths:

M books/kestrel/c/syntax/preprocessor-lexemes.lisp

Log Message:
-----------
[C$] Add some theorems.


Commit: 4fd8c076e7bb8ea87061f2e7eb0774b2a7ee8706
https://github.com/acl2/acl2/commit/4fd8c076e7bb8ea87061f2e7eb0774b2a7ee8706
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-01-16 (Fri, 16 Jan 2026)

Changed paths:

M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Initial code for macro argument replacement.


Commit: ff74946d2f511b1f3b406115a7871ab65163aa5b
https://github.com/acl2/acl2/commit/ff74946d2f511b1f3b406115a7871ab65163aa5b
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-01-16 (Fri, 16 Jan 2026)

Changed paths:
M books/projects/x86isa/machine/cert.acl2
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/tools/execution/top.lisp

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

Merge.


Compare: https://github.com/acl2/acl2/compare/f087c86ee898...ff74946d2f51