[acl2/acl2] 83d184: Avoid errors from ACL2(p) run that used waterfall-...
0 views
Skip to first unread message
MattKaufmann
Mar 1, 2026, 8:04:04 PM (3 days ago) Mar 1
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 83d184694c7e506b14fa4cb990921faabf0e9291
https://github.com/acl2/acl2/commit/83d184694c7e506b14fa4cb990921faabf0e9291
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-03-01 (Sun, 01 Mar 2026)
Changed paths:
M books/kestrel/risc-v/executable/execution-executable.lisp
M books/projects/python/embedding/types.lisp
M books/workshops/2025/manjrekar/examples/imul64/imul64-proof.lisp
M books/workshops/2025/manjrekar/examples/imul8/imul8-proof.lisp
Log Message:
-----------
Avoid errors from ACL2(p) run that used waterfall-parallelism.
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 83d184694c7e506b14fa4cb990921faabf0e9291
https://github.com/acl2/acl2/commit/83d184694c7e506b14fa4cb990921faabf0e9291
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-03-01 (Sun, 01 Mar 2026)
Changed paths:
M books/kestrel/risc-v/executable/execution-executable.lisp
M books/projects/python/embedding/types.lisp
M books/workshops/2025/manjrekar/examples/imul64/imul64-proof.lisp
M books/workshops/2025/manjrekar/examples/imul8/imul8-proof.lisp
Log Message:
-----------
Avoid errors from ACL2(p) run that used waterfall-parallelism.
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
MattKaufmann
Mar 1, 2026, 8:04:38 PM (3 days ago) Mar 1
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Mar 2, 2026, 5:17:21 PM (2 days ago) Mar 2
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
https://github.com/acl2/acl2/commit/6ec4e13c5538b87d6b5363cfec0927d7250d1ed6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/arm/doc.lisp
Log Message:
-----------
[arm] Fix xdoc parents.
Commit: 0a918f5e2e9c49d98df566ee87bb2ba64789768e
https://github.com/acl2/acl2/commit/0a918f5e2e9c49d98df566ee87bb2ba64789768e
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/arm/doc.lisp
Log Message:
-----------
Merge commit '6ec4e13c5538b87d6b5363cfec0927d7250d1ed6' into HEAD
Commit: f333c7fc9ea602bbf203831af7c1a3104d517d55
https://github.com/acl2/acl2/commit/f333c7fc9ea602bbf203831af7c1a3104d517d55
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
Log Message:
-----------
[X86ISA] Add MOVD/Q to MMX register.
Commit: 5577f228f921b568ef0d4dd6fbfdaf4ba982cc3a
https://github.com/acl2/acl2/commit/5577f228f921b568ef0d4dd6fbfdaf4ba982cc3a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
Log Message:
-----------
[X86ISA] Add MOVD/Q from MMX register.
Commit: 129b731c3c860195b31ba2f84c2205af92aaceb3
https://github.com/acl2/acl2/commit/129b731c3c860195b31ba2f84c2205af92aaceb3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/core.lisp
Log Message:
-----------
[obags] Fix 3 obag ops, and improve obag doc.
Oddly, those 3 operations neglected to apply a needed deletion to the tail, in
order to keep things "in sync". The operations were taken from osets, and meant
to be adapted to obags (via that deletion), but that adaptation did not
happen. Thanks to Grant Jurgensen for noticing and reporting the issue.
Also improve some documentation.
Also remove some stray documentation text (another indication that somehow the
file had not been properly finalized).
Commit: 1702a4d94e3695cf59e5fee072c8026cbf7d607e
https://github.com/acl2/acl2/commit/1702a4d94e3695cf59e5fee072c8026cbf7d607e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
Log Message:
-----------
[X86ISA] Add PCMPEQB/W/D (MMX variants).
Commit: e5a0f7ff9a1f9da382cad02c674f18278b21d3df
https://github.com/acl2/acl2/commit/e5a0f7ff9a1f9da382cad02c674f18278b21d3df
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
Log Message:
-----------
[X86ISA] Add PCMPGTB/W/D (MMX variants).
Commit: 904278885116354eab8265595bb908e89f45d2ea
https://github.com/acl2/acl2/commit/904278885116354eab8265595bb908e89f45d2ea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/pcmp.lisp
Log Message:
-----------
[X86ISA] Minor edits for stylistic consistency.
Commit: bb0b4c95887272a4be837d69b01e36237580fbdc
https://github.com/acl2/acl2/commit/bb0b4c95887272a4be837d69b01e36237580fbdc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/tests.lisp
Log Message:
-----------
[obags] Add some tests.
Commit: 2014436d42ae5be2c60460fed1557a53341d4131
https://github.com/acl2/acl2/commit/2014436d42ae5be2c60460fed1557a53341d4131
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/core.lisp
Log Message:
-----------
[obags] Add a bag sum operation.
Commit: ff7dd08f959ae717c0ef02023149f6c03e970a49
https://github.com/acl2/acl2/commit/ff7dd08f959ae717c0ef02023149f6c03e970a49
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/tests.lisp
Log Message:
-----------
[obags] Add some tests.
Commit: 9431757cf3cc09f390fab06ca7b3a1115f744916
https://github.com/acl2/acl2/commit/9431757cf3cc09f390fab06ca7b3a1115f744916
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/utilities/defstobj-plus-tests.lisp
Log Message:
-----------
[utilities] Add a test of defstobj+
Commit: 4a49f87bbb77149c9ab04f86dccf8f836d7b07b8
https://github.com/acl2/acl2/commit/4a49f87bbb77149c9ab04f86dccf8f836d7b07b8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/core.lisp
M books/std/obags/tests.lisp
Log Message:
-----------
[obags] Reorder some operations within a file.
Commit: 667172fb641cdde3748e2c98f57fc1f9230e4f50
https://github.com/acl2/acl2/commit/667172fb641cdde3748e2c98f57fc1f9230e4f50
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/utilities/defstobj-plus-tests.lisp
Log Message:
-----------
Merge commit '9431757cf3cc09f390fab06ca7b3a1115f744916' into HEAD
Commit: e0bafa162c4170e3952940b166e1c4446b41d27d
https://github.com/acl2/acl2/commit/e0bafa162c4170e3952940b166e1c4446b41d27d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/core.lisp
Log Message:
-----------
[obags] Add some validation theorems.
Commit: 4a374d7bce820d9961f8e9ef0040d156c40ac747
https://github.com/acl2/acl2/commit/4a374d7bce820d9961f8e9ef0040d156c40ac747
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/utilities/defstobj-plus-tests.lisp
Log Message:
-----------
Merge.
Commit: cbb7831b9eb85e4cf49cbd84a89a3abe64bc9bab
https://github.com/acl2/acl2/commit/cbb7831b9eb85e4cf49cbd84a89a3abe64bc9bab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/95fed79a868b...cbb7831b9eb8
Home: https://github.com/acl2/acl2
Commit: 83d184694c7e506b14fa4cb990921faabf0e9291
https://github.com/acl2/acl2/commit/83d184694c7e506b14fa4cb990921faabf0e9291
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-03-01 (Sun, 01 Mar 2026)
Changed paths:
M books/kestrel/risc-v/executable/execution-executable.lisp
M books/projects/python/embedding/types.lisp
M books/workshops/2025/manjrekar/examples/imul64/imul64-proof.lisp
M books/workshops/2025/manjrekar/examples/imul8/imul8-proof.lisp
Log Message:
-----------
Avoid errors from ACL2(p) run that used waterfall-parallelism.
Commit: 6ec4e13c5538b87d6b5363cfec0927d7250d1ed6
Commit: 83d184694c7e506b14fa4cb990921faabf0e9291
https://github.com/acl2/acl2/commit/83d184694c7e506b14fa4cb990921faabf0e9291
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-03-01 (Sun, 01 Mar 2026)
Changed paths:
M books/kestrel/risc-v/executable/execution-executable.lisp
M books/projects/python/embedding/types.lisp
M books/workshops/2025/manjrekar/examples/imul64/imul64-proof.lisp
M books/workshops/2025/manjrekar/examples/imul8/imul8-proof.lisp
Log Message:
-----------
Avoid errors from ACL2(p) run that used waterfall-parallelism.
https://github.com/acl2/acl2/commit/6ec4e13c5538b87d6b5363cfec0927d7250d1ed6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/arm/doc.lisp
Log Message:
-----------
[arm] Fix xdoc parents.
Commit: 0a918f5e2e9c49d98df566ee87bb2ba64789768e
https://github.com/acl2/acl2/commit/0a918f5e2e9c49d98df566ee87bb2ba64789768e
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/arm/doc.lisp
Log Message:
-----------
Merge commit '6ec4e13c5538b87d6b5363cfec0927d7250d1ed6' into HEAD
Commit: f333c7fc9ea602bbf203831af7c1a3104d517d55
https://github.com/acl2/acl2/commit/f333c7fc9ea602bbf203831af7c1a3104d517d55
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
Log Message:
-----------
[X86ISA] Add MOVD/Q to MMX register.
Commit: 5577f228f921b568ef0d4dd6fbfdaf4ba982cc3a
https://github.com/acl2/acl2/commit/5577f228f921b568ef0d4dd6fbfdaf4ba982cc3a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
Log Message:
-----------
[X86ISA] Add MOVD/Q from MMX register.
Commit: 129b731c3c860195b31ba2f84c2205af92aaceb3
https://github.com/acl2/acl2/commit/129b731c3c860195b31ba2f84c2205af92aaceb3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/core.lisp
Log Message:
-----------
[obags] Fix 3 obag ops, and improve obag doc.
Oddly, those 3 operations neglected to apply a needed deletion to the tail, in
order to keep things "in sync". The operations were taken from osets, and meant
to be adapted to obags (via that deletion), but that adaptation did not
happen. Thanks to Grant Jurgensen for noticing and reporting the issue.
Also improve some documentation.
Also remove some stray documentation text (another indication that somehow the
file had not been properly finalized).
Commit: 1702a4d94e3695cf59e5fee072c8026cbf7d607e
https://github.com/acl2/acl2/commit/1702a4d94e3695cf59e5fee072c8026cbf7d607e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
Log Message:
-----------
[X86ISA] Add PCMPEQB/W/D (MMX variants).
Commit: e5a0f7ff9a1f9da382cad02c674f18278b21d3df
https://github.com/acl2/acl2/commit/e5a0f7ff9a1f9da382cad02c674f18278b21d3df
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
Log Message:
-----------
[X86ISA] Add PCMPGTB/W/D (MMX variants).
Commit: 904278885116354eab8265595bb908e89f45d2ea
https://github.com/acl2/acl2/commit/904278885116354eab8265595bb908e89f45d2ea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/pcmp.lisp
Log Message:
-----------
[X86ISA] Minor edits for stylistic consistency.
Commit: bb0b4c95887272a4be837d69b01e36237580fbdc
https://github.com/acl2/acl2/commit/bb0b4c95887272a4be837d69b01e36237580fbdc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/tests.lisp
Log Message:
-----------
[obags] Add some tests.
Commit: 2014436d42ae5be2c60460fed1557a53341d4131
https://github.com/acl2/acl2/commit/2014436d42ae5be2c60460fed1557a53341d4131
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/core.lisp
Log Message:
-----------
[obags] Add a bag sum operation.
Commit: ff7dd08f959ae717c0ef02023149f6c03e970a49
https://github.com/acl2/acl2/commit/ff7dd08f959ae717c0ef02023149f6c03e970a49
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/tests.lisp
Log Message:
-----------
[obags] Add some tests.
Commit: 9431757cf3cc09f390fab06ca7b3a1115f744916
https://github.com/acl2/acl2/commit/9431757cf3cc09f390fab06ca7b3a1115f744916
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/utilities/defstobj-plus-tests.lisp
Log Message:
-----------
[utilities] Add a test of defstobj+
Commit: 4a49f87bbb77149c9ab04f86dccf8f836d7b07b8
https://github.com/acl2/acl2/commit/4a49f87bbb77149c9ab04f86dccf8f836d7b07b8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/core.lisp
M books/std/obags/tests.lisp
Log Message:
-----------
[obags] Reorder some operations within a file.
Commit: 667172fb641cdde3748e2c98f57fc1f9230e4f50
https://github.com/acl2/acl2/commit/667172fb641cdde3748e2c98f57fc1f9230e4f50
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/utilities/defstobj-plus-tests.lisp
Log Message:
-----------
Merge commit '9431757cf3cc09f390fab06ca7b3a1115f744916' into HEAD
Commit: e0bafa162c4170e3952940b166e1c4446b41d27d
https://github.com/acl2/acl2/commit/e0bafa162c4170e3952940b166e1c4446b41d27d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/std/obags/core.lisp
Log Message:
-----------
[obags] Add some validation theorems.
Commit: 4a374d7bce820d9961f8e9ef0040d156c40ac747
https://github.com/acl2/acl2/commit/4a374d7bce820d9961f8e9ef0040d156c40ac747
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/utilities/defstobj-plus-tests.lisp
Log Message:
-----------
Merge.
Commit: cbb7831b9eb85e4cf49cbd84a89a3abe64bc9bab
https://github.com/acl2/acl2/commit/cbb7831b9eb85e4cf49cbd84a89a3abe64bc9bab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/95fed79a868b...cbb7831b9eb8
acl2buildserver
Mar 3, 2026, 12:17:56 PM (2 days ago) Mar 3
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Commit: 7f63d2bf2d4355494d0755ecf039391c4b83c5e6
https://github.com/acl2/acl2/commit/7f63d2bf2d4355494d0755ecf039391c4b83c5e6
M books/projects/x86isa/machine/instructions/fp/logical.lisp
A books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
Log Message:
-----------
[X86ISA] Refactor some code.
Move the SSE and VEX bitwise logical operations to a separate file.
Commit: d443b2591d38d4a51403b38fb204049a6ff6a663
https://github.com/acl2/acl2/commit/d443b2591d38d4a51403b38fb204049a6ff6a663
Log Message:
-----------
[X86ISA] Add PAND/PANDN/POR/PXOR (MMX variants).
Commit: c1b77f47710a91a9209afd13f344fabd86a6d9c2
https://github.com/acl2/acl2/commit/c1b77f47710a91a9209afd13f344fabd86a6d9c2
Author: Matt Kaufmann <matthew.j...@gmail.com>
M books/kestrel/auto-termination/README
M books/kestrel/auto-termination/td-cands.acl2
M books/kestrel/auto-termination/td-cands.lisp
M books/projects/acl2-in-hol/tests/inputs/PKGS.lsp
M books/projects/acl2-in-hol/tests/inputs/PKGS.sml
M books/projects/hol-in-acl2/acl2/hol.lisp
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/milawa/ACL2/bootstrap/level11/waterfall-steps.lisp
M books/projects/milawa/ACL2/bootstrap/level5/update-clause-bldr.lisp
M books/projects/milawa/ACL2/bootstrap/level9/add-equality.lisp
M books/projects/milawa/ACL2/bootstrap/level9/eqdatabasep.lisp
M books/projects/milawa/ACL2/bootstrap/logic/disjoin-formulas.lisp
M books/projects/milawa/ACL2/bootstrap/logic/proofp-3-provablep.lisp
M books/projects/milawa/ACL2/interface/pcert.lisp
M books/projects/set-theory/foldr.lisp
M books/projects/set-theory/ordinals.lisp
M books/system/check-system-guards.lisp
M books/system/pseudo-good-worldp.lisp
Log Message:
-----------
Tweaked set-theory and hol-in-acl2 libraries. Tweaked a comment in books/system/check-system-guards.lisp. Updated termination database (specifically, *td-candidates*). Fixed a bug in the pseudo-good-worldp check (evaluator-check-inputs is not a global-value), and removed some ttags books from that check. Fixed Milawa issues.
One Milawa issue was a minor bug: fms! was called on an :object
channel, which needed to be a :character channel (and it now is). The
other Milawa issues had to do with violations of redundancy, and I
just hacked my way past them with a sequence of "make" commands with
target milawa-test-extended (in the books/ direcotry), until the last
one concluded successfully.
Commit: d9151ad522126f512fbaf53faa38b21e3ce5b309
https://github.com/acl2/acl2/commit/d9151ad522126f512fbaf53faa38b21e3ce5b309
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-exprs.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-array.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/dargp.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-term-into-dag-array-basic.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
Merge commit '05b9401249e38e6d04a697609905e1723dc1078c' into HEAD
Commit: 5bc88b3ddafd7f98d05952234f038ea234a38a77
https://github.com/acl2/acl2/commit/5bc88b3ddafd7f98d05952234f038ea234a38a77
Author: Matt Kaufmann <matthew.j...@gmail.com>
Commit: 459cfff321d689df16355b2c3d8b28e862c975e2
https://github.com/acl2/acl2/commit/459cfff321d689df16355b2c3d8b28e862c975e2
A books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/top.lisp
Log Message:
-----------
[X86ISA] Refactor some code.
Move packed shifts into new file.
Commit: a76fd6246a389abb535d85b4d3b58993636449b4
https://github.com/acl2/acl2/commit/a76fd6246a389abb535d85b4d3b58993636449b4
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
Log Message:
-----------
[X86ISA] Move PSLLDQ/PSLRDQ to more appropriate file.
Commit: 8a6d50a0da4d776acf24d48394d34c00ec22484e
https://github.com/acl2/acl2/commit/8a6d50a0da4d776acf24d48394d34c00ec22484e
Log Message:
-----------
[X86ISA] Fix comment.
Commit: 1d2c19ba0cc6ad94ce5a0762966cd5ba67d22780
https://github.com/acl2/acl2/commit/1d2c19ba0cc6ad94ce5a0762966cd5ba67d22780
Log Message:
-----------
[X86ISA] Refactor some code.
In the packed shift SSE instructions, extract and use a separate macro to
generate the specification functions, so they can be used for other variants of
these instructions (e.g. MMX, upcoming).
Commit: 85ac411190522bbc64f5163eb5559b69e6184a23
https://github.com/acl2/acl2/commit/85ac411190522bbc64f5163eb5559b69e6184a23
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-exprs.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-array.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/dargp.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-term-into-dag-array-basic.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/utilities/defstobj-plus-tests.lisp
Commit: 92345c45e845b2a727f9cf8c622577448f4f1070
https://github.com/acl2/acl2/commit/92345c45e845b2a727f9cf8c622577448f4f1070
Author: Matt Kaufmann <matthew.j...@gmail.com>
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-exprs.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-array.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/dargp.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-term-into-dag-array-basic.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
Merge
Commit: 8c74b41b232be665d13fe68b08def77ef4504109
https://github.com/acl2/acl2/commit/8c74b41b232be665d13fe68b08def77ef4504109
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
A books/projects/x86isa/machine/instructions/logical.lisp
A books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
Log Message:
-----------
Merge commit '85ac411190522bbc64f5163eb5559b69e6184a23' into HEAD
Commit: d11d37f135688869d9e75c7ab16694d961366a2a
https://github.com/acl2/acl2/commit/d11d37f135688869d9e75c7ab16694d961366a2a
Changed paths:
M books/kestrel/axe/dag-exprs.lisp
A books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
Merge commit '97c61ed56c2f5b12a4da2611d08a693a81d336a4' into HEAD
Compare: https://github.com/acl2/acl2/compare/97c61ed56c2f...d11d37f13568
Home: https://github.com/acl2/acl2
Commit: 83d184694c7e506b14fa4cb990921faabf0e9291
https://github.com/acl2/acl2/commit/83d184694c7e506b14fa4cb990921faabf0e9291
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-03-01 (Sun, 01 Mar 2026)
Changed paths:
M books/kestrel/risc-v/executable/execution-executable.lisp
M books/projects/python/embedding/types.lisp
M books/workshops/2025/manjrekar/examples/imul64/imul64-proof.lisp
M books/workshops/2025/manjrekar/examples/imul8/imul8-proof.lisp
Log Message:
-----------
Avoid errors from ACL2(p) run that used waterfall-parallelism.
Commit: 83d184694c7e506b14fa4cb990921faabf0e9291
https://github.com/acl2/acl2/commit/83d184694c7e506b14fa4cb990921faabf0e9291
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-03-01 (Sun, 01 Mar 2026)
Changed paths:
M books/kestrel/risc-v/executable/execution-executable.lisp
M books/projects/python/embedding/types.lisp
M books/workshops/2025/manjrekar/examples/imul64/imul64-proof.lisp
M books/workshops/2025/manjrekar/examples/imul8/imul8-proof.lisp
Log Message:
-----------
Avoid errors from ACL2(p) run that used waterfall-parallelism.
https://github.com/acl2/acl2/commit/7f63d2bf2d4355494d0755ecf039391c4b83c5e6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/fp/logical.lisp
A books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
Log Message:
-----------
[X86ISA] Refactor some code.
Move the SSE and VEX bitwise logical operations to a separate file.
Commit: d443b2591d38d4a51403b38fb204049a6ff6a663
https://github.com/acl2/acl2/commit/d443b2591d38d4a51403b38fb204049a6ff6a663
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/logical.lisp
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
Log Message:
-----------
[X86ISA] Add PAND/PANDN/POR/PXOR (MMX variants).
Commit: c1b77f47710a91a9209afd13f344fabd86a6d9c2
https://github.com/acl2/acl2/commit/c1b77f47710a91a9209afd13f344fabd86a6d9c2
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/GNUmakefile
Changed paths:
M books/kestrel/auto-termination/README
M books/kestrel/auto-termination/td-cands.acl2
M books/kestrel/auto-termination/td-cands.lisp
M books/projects/acl2-in-hol/tests/inputs/PKGS.lsp
M books/projects/acl2-in-hol/tests/inputs/PKGS.sml
M books/projects/hol-in-acl2/acl2/hol.lisp
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/milawa/ACL2/bootstrap/level11/waterfall-steps.lisp
M books/projects/milawa/ACL2/bootstrap/level5/update-clause-bldr.lisp
M books/projects/milawa/ACL2/bootstrap/level9/add-equality.lisp
M books/projects/milawa/ACL2/bootstrap/level9/eqdatabasep.lisp
M books/projects/milawa/ACL2/bootstrap/logic/disjoin-formulas.lisp
M books/projects/milawa/ACL2/bootstrap/logic/proofp-3-provablep.lisp
M books/projects/milawa/ACL2/interface/pcert.lisp
M books/projects/set-theory/foldr.lisp
M books/projects/set-theory/ordinals.lisp
M books/system/check-system-guards.lisp
M books/system/pseudo-good-worldp.lisp
Log Message:
-----------
Tweaked set-theory and hol-in-acl2 libraries. Tweaked a comment in books/system/check-system-guards.lisp. Updated termination database (specifically, *td-candidates*). Fixed a bug in the pseudo-good-worldp check (evaluator-check-inputs is not a global-value), and removed some ttags books from that check. Fixed Milawa issues.
One Milawa issue was a minor bug: fms! was called on an :object
channel, which needed to be a :character channel (and it now is). The
other Milawa issues had to do with violations of redundancy, and I
just hacked my way past them with a sequence of "make" commands with
target milawa-test-extended (in the books/ direcotry), until the last
one concluded successfully.
Commit: d9151ad522126f512fbaf53faa38b21e3ce5b309
https://github.com/acl2/acl2/commit/d9151ad522126f512fbaf53faa38b21e3ce5b309
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-exprs.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-array.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/dargp.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-term-into-dag-array-basic.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
Merge commit '05b9401249e38e6d04a697609905e1723dc1078c' into HEAD
Commit: 5bc88b3ddafd7f98d05952234f038ea234a38a77
https://github.com/acl2/acl2/commit/5bc88b3ddafd7f98d05952234f038ea234a38a77
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/arm/doc.lisp
M books/kestrel/utilities/defstobj-plus-tests.lisp
Changed paths:
M books/kestrel/arm/doc.lisp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/std/obags/core.lisp
M books/std/obags/tests.lisp
Log Message:
-----------
Merge
M books/std/obags/tests.lisp
Log Message:
-----------
Commit: 459cfff321d689df16355b2c3d8b28e862c975e2
https://github.com/acl2/acl2/commit/459cfff321d689df16355b2c3d8b28e862c975e2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
A books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/top.lisp
Log Message:
-----------
[X86ISA] Refactor some code.
Move packed shifts into new file.
Commit: a76fd6246a389abb535d85b4d3b58993636449b4
https://github.com/acl2/acl2/commit/a76fd6246a389abb535d85b4d3b58993636449b4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/pshift.lisp
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
Log Message:
-----------
[X86ISA] Move PSLLDQ/PSLRDQ to more appropriate file.
Commit: 8a6d50a0da4d776acf24d48394d34c00ec22484e
https://github.com/acl2/acl2/commit/8a6d50a0da4d776acf24d48394d34c00ec22484e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/pshift.lisp
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
Log Message:
-----------
[X86ISA] Fix comment.
Commit: 1d2c19ba0cc6ad94ce5a0762966cd5ba67d22780
https://github.com/acl2/acl2/commit/1d2c19ba0cc6ad94ce5a0762966cd5ba67d22780
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/pshift.lisp
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
Log Message:
-----------
[X86ISA] Refactor some code.
In the packed shift SSE instructions, extract and use a separate macro to
generate the specification functions, so they can be used for other variants of
these instructions (e.g. MMX, upcoming).
Commit: 85ac411190522bbc64f5163eb5559b69e6184a23
https://github.com/acl2/acl2/commit/85ac411190522bbc64f5163eb5559b69e6184a23
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-exprs.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-array.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/dargp.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-term-into-dag-array-basic.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/utilities/defstobj-plus-tests.lisp
M books/std/obags/core.lisp
M books/std/obags/tests.lisp
Log Message:
-----------
Merge.
M books/std/obags/tests.lisp
Log Message:
-----------
Commit: 92345c45e845b2a727f9cf8c622577448f4f1070
https://github.com/acl2/acl2/commit/92345c45e845b2a727f9cf8c622577448f4f1070
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)
Changed paths:
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
Changed paths:
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-exprs.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-array.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/dargp.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-term-into-dag-array-basic.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
Merge
Commit: 8c74b41b232be665d13fe68b08def77ef4504109
https://github.com/acl2/acl2/commit/8c74b41b232be665d13fe68b08def77ef4504109
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
A books/projects/x86isa/machine/instructions/logical.lisp
A books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
Log Message:
-----------
Merge commit '85ac411190522bbc64f5163eb5559b69e6184a23' into HEAD
Commit: d11d37f135688869d9e75c7ab16694d961366a2a
https://github.com/acl2/acl2/commit/d11d37f135688869d9e75c7ab16694d961366a2a
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)
Changed paths:
M books/kestrel/axe/dag-exprs.lisp
A books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
Merge commit '97c61ed56c2f5b12a4da2611d08a693a81d336a4' into HEAD
Compare: https://github.com/acl2/acl2/compare/97c61ed56c2f...d11d37f13568
Reply all
Reply to author
Forward
0 new messages