Branch: refs/heads/testing-user-01
Commit: 7d6427ff35e131cf45c2eb7e1dfdb9e9a906be9d
https://github.com/acl2/acl2/commit/7d6427ff35e131cf45c2eb7e1dfdb9e9a906be9d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Fix doc.
Commit: a7534ff052076feeca49cf5683a621424f4ea8f6
https://github.com/acl2/acl2/commit/a7534ff052076feeca49cf5683a621424f4ea8f6
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] added other integer operations into primitives-evaluation.lisp
Commit: 08326d494c7177f7a04ce8c433f7cd225056a8da
https://github.com/acl2/acl2/commit/08326d494c7177f7a04ce8c433f7cd225056a8da
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] removed whitespaces
Commit: ec2ad95931d67c9bf07fb2ac834044039f270df5
https://github.com/acl2/acl2/commit/ec2ad95931d67c9bf07fb2ac834044039f270df5
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] fixed guard verification for mod
Commit: 1bdd969cbd82b65522c36dc64b834a8b130234b8
https://github.com/acl2/acl2/commit/1bdd969cbd82b65522c36dc64b834a8b130234b8
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Log Message:
-----------
[C$] Export more symbols.
Commit: 0774f833e58a2e680bd73f5a42d68a204dc368fa
https://github.com/acl2/acl2/commit/0774f833e58a2e680bd73f5a42d68a204dc368fa
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/package.lsp
Log Message:
-----------
[C2C] Avoid a symbol conflict in a package.
Commit: c68d5a70e07db6038228c0f60b3e9c7febc10626
https://github.com/acl2/acl2/commit/c68d5a70e07db6038228c0f60b3e9c7febc10626
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp
Log Message:
-----------
[safestruct] Add checks on types.
Commit: 8d503a62807316761a8c7a7a19b511cb4c0c72a1
https://github.com/acl2/acl2/commit/8d503a62807316761a8c7a7a19b511cb4c0c72a1
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Add a theorem.
Commit: 9613e4e9c94a30e247ee0d5a147b6767fd4658dd
https://github.com/acl2/acl2/commit/9613e4e9c94a30e247ee0d5a147b6767fd4658dd
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[sts] Remove local theorem no longer needed.
Commit: 10bcd62ad9781924cf306754ab2bc32cb5e2089e
https://github.com/acl2/acl2/commit/10bcd62ad9781924cf306754ab2bc32cb5e2089e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
R books/kestrel/c/transformation/struct-safety-checks.lisp
A books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/top.lisp
Log Message:
-----------
[C2C] Rename file.
Commit: b66697489ac3e478f5e1cce94278422ae551a986
https://github.com/acl2/acl2/commit/b66697489ac3e478f5e1cce94278422ae551a986
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Make the checkers specific to STS.
STS = Struct Type Split
Commit: 124c092b1f72ea599a2e3d6f6c737ab8bd2bf6ef
https://github.com/acl2/acl2/commit/124c092b1f72ea599a2e3d6f6c737ab8bd2bf6ef
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safe] Update some links.
Commit: e192548b43fba4134ba7045d952476ce4d3f9941
https://github.com/acl2/acl2/commit/e192548b43fba4134ba7045d952476ce4d3f9941
Author: Matt Kaufmann <
kauf...@cs.utexas.edu>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Improved the reference in :DOC the-method to "Computer-Aided Reasoning: An Approach".
Thanks to Eric Smith for bringing up this issue.
Commit: 2eea7a47a6579dbda42123fd187475a19b42a805
https://github.com/acl2/acl2/commit/2eea7a47a6579dbda42123fd187475a19b42a805
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Merge.
Commit: 190f99755a5685a8557932233469badb67e9ebe0
https://github.com/acl2/acl2/commit/190f99755a5685a8557932233469badb67e9ebe0
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Improve model of box values.
Use ispace values instead of ispaces.
Commit: b45a69b4de52c1815ae55cd50804e4addb32c2a8
https://github.com/acl2/acl2/commit/b45a69b4de52c1815ae55cd50804e4addb32c2a8
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Remove doc that turned out not to be the case.
Commit: 273d7f7658f6ee752ed49e18bff0e30fb053020f
https://github.com/acl2/acl2/commit/273d7f7658f6ee752ed49e18bff0e30fb053020f
Author: Eric McCarthy <
mcca...@kestrel.edu>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/syntax-abstraction.lisp
Log Message:
-----------
[remora] grammar/parser/abstractor no longer produce a shape :dim
Commit: 4381fd3ec2b035c0b2d33b76815afd2d47bedc16
https://github.com/acl2/acl2/commit/4381fd3ec2b035c0b2d33b76815afd2d47bedc16
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/auto-termination/td-cands.lisp
M books/kestrel/c/language/grammar.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/java/language/grammar.lisp
M books/kestrel/json/grammar.lisp
M books/kestrel/remora/grammar.lisp
M books/kestrel/yul/language/grammar-old.lisp
M books/kestrel/yul/language/grammar.lisp
M books/projects/abnf/examples/imap.lisp
M books/projects/abnf/examples/imf.lisp
M books/projects/abnf/examples/pdf.lisp
M books/projects/abnf/examples/uri.lisp
R books/projects/abnf/grammar-definer/deftreeops-doc.lisp
R books/projects/abnf/grammar-definer/deftreeops.lisp
M books/projects/abnf/grammar-definer/top.lisp
A books/projects/abnf/tree-operations/deftreeops-doc.lisp
A books/projects/abnf/tree-operations/deftreeops.lisp
M books/projects/abnf/tree-operations/top.lisp
M books/projects/aleo/leo/early-version/definition/grammar.lisp
M books/projects/aleo/leo/grammar.lisp
M books/projects/aleo/vm/language/early-version/grammar.lisp
M books/projects/aleo/vm/language/grammar.lisp
M books/projects/pfcs/grammar.lisp
Log Message:
-----------
[ABNF] Improve organization.
Put `deftreeops` under tree operations.
Commit: 746c7e36b896714d1f7b50b54ff583a65164c539
https://github.com/acl2/acl2/commit/746c7e36b896714d1f7b50b54ff583a65164c539
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Improve model of box values.
Use a type value instead of a type.
Commit: 22b66c84d2c38e19ecbb81bd600b6925d0218e81
https://github.com/acl2/acl2/commit/22b66c84d2c38e19ecbb81bd600b6925d0218e81
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/package.lsp
Log Message:
-----------
[CPP] Adapt to changes to C$ package.
Commit: eb690428693ca07b6808c6956a943003e265f80d
https://github.com/acl2/acl2/commit/eb690428693ca07b6808c6956a943003e265f80d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Add a theorem.
Commit: 2ec876f945722d030d416c5ab684d54f355fd5da
https://github.com/acl2/acl2/commit/2ec876f945722d030d416c5ab684d54f355fd5da
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Add evaluation of boxes.
Commit: f08acadc62bee538d9b1707b642bb35009d855ff
https://github.com/acl2/acl2/commit/f08acadc62bee538d9b1707b642bb35009d855ff
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Extend constraints on values.
Although a box value is a scalar, its inner value must satisfy dimension
constraints.
Commit: e1ac89851eb88f2b26bfcfd8f37ee1f4e0899c47
https://github.com/acl2/acl2/commit/e1ac89851eb88f2b26bfcfd8f37ee1f4e0899c47
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/syntax-abstraction.lisp
Log Message:
-----------
Merge.
Commit: be7a53303501379433a28557bd0330c2992db04a
https://github.com/acl2/acl2/commit/be7a53303501379433a28557bd0330c2992db04a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Fix some KaTeX.
Commit: 48b26bedca6a9d460fbb7873a2f91542bb9af5a3
https://github.com/acl2/acl2/commit/48b26bedca6a9d460fbb7873a2f91542bb9af5a3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/transformation/package.lsp
R books/kestrel/c/transformation/struct-safety-checks.lisp
A books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/top.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/projects/filesystems/utilities/cpp-syntax/package.lsp
Log Message:
-----------
Merge.
Commit: c84843866f6cbf0ea36bd4c61a0e978aa6522b3f
https://github.com/acl2/acl2/commit/c84843866f6cbf0ea36bd4c61a0e978aa6522b3f
Author: Eric McCarthy <
mcca...@kestrel.edu>
Date: 2026-06-19 (Fri, 19 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
Log Message:
-----------
[remora] remove `shape :dim`
Commit: 28e7d3307276f99967d75201c466f27165867655
https://github.com/acl2/acl2/commit/28e7d3307276f99967d75201c466f27165867655
Author: Yahya Sohail <
ya...@yahyasohail.com>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/fp/logical.lisp
Log Message:
-----------
Fix CMPPS/CMPPD/CMPSS/CMPSD predicate imm8 mask
The CMPPS, CMPPD, CMPSS, and CMPSD instructions use the low 3 bits of
imm8 as a comparison predicate. Bits 3-7 are reserved per the Intel SDM.
The model was reading only the low 2 bits via (n02 imm), so predicates
4-7 (NEQ, NLT, NLE, ORD) collapsed to 0-3 (EQ, LT, LE, UNORD), producing
the inverse of the correct comparison result.
Change (n02 imm) to (n03 imm) in the four predicate-reading locations in
fp/logical.lisp so that bits 2:0 are used as the predicate selector.
Verified by make test in tools/execution/asmtest:
testgen_1332 (CMPPS): 0 mismatches
testgen_1345 (CMPSS): 0 mismatches
testgen_1347 (CMPPD): 0 mismatches
testgen_1351 (CMPSD): 0 mismatches
Commit: 1b905154b1a3f3d3b0edfa7477f62515b7919c9b
https://github.com/acl2/acl2/commit/1b905154b1a3f3d3b0edfa7477f62515b7919c9b
Author: Yahya Sohail <
ya...@yahyasohail.com>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/pshift.lisp
Log Message:
-----------
Fix PSLLDQ/PSRLDQ count>=16 to zero the destination
Per the Intel SDM, if the count operand to PSLLDQ/PSRLDQ is greater than
15, the destination operand is set to all zeros. The SDM pseudocode
sets TEMP := 16 in this case so that the subsequent 128-bit shift
produces zero. The model instead clamped count to 0, making the
instruction a no-op rather than zeroing.
Change the clamp to 16 instead of 0 so the shift produces the
required zero result.
Verified by make test in tools/execution/asmtest:
testgen_666 (PSRLDQ): 0 mismatches
testgen_667 (PSLLDQ): 0 mismatches
Commit: b1d82e368cf64b18f4a7e4c24808ce37d96c8b82
https://github.com/acl2/acl2/commit/b1d82e368cf64b18f4a7e4c24808ce37d96c8b82
Author: Yahya Sohail <
ya...@yahyasohail.com>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/bit.lisp
Log Message:
-----------
Fix LZCNT helper to start search at MSB
The recursive lzcnt helper counts leading zeros by walking bits from the
MSB downward. Its base case fires when the index (i+1) reaches 0, and
its only call site passed an initial i+1 of 0, so the helper returned
the operand-size-bits value immediately for every input.
Change the initial i+1 to (ash operand-size 3) (= bits) so the first
iteration examines bit (bits - 1), the MSB, and decrements toward 0.
Verified by make test in tools/execution/asmtest:
testgen_2025 (LZCNT): 0 mismatches
Commit: 5ac0558f2287a23c5903b25a1dbc25b5e39680b9
https://github.com/acl2/acl2/commit/5ac0558f2287a23c5903b25a1dbc25b5e39680b9
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Add a theorem.
Commit: cee616ac327fc833cc6d713322f79f559e8621d5
https://github.com/acl2/acl2/commit/cee616ac327fc833cc6d713322f79f559e8621d5
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
Log Message:
-----------
[Remora] Add an op on dynamic environments.
Also simplify another one, taking advantage of the new one.
Commit: 0e8a6d085295e2f0a1cd645c646b2642d9af4efa
https://github.com/acl2/acl2/commit/0e8a6d085295e2f0a1cd645c646b2642d9af4efa
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Extend dynamic semantics.
Add evaluation of unbox expressions and bracket expressions.
Commit: e6a178f5c051bc514988bebba26d8937fd9ecc36
https://github.com/acl2/acl2/commit/e6a178f5c051bc514988bebba26d8937fd9ecc36
Author: Matt Kaufmann <
kauf...@cs.utexas.edu>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Fixed bug in :DOC fmx.
Commit: 28037de45bd557570741b2607402ac0f5ca676ab
https://github.com/acl2/acl2/commit/28037de45bd557570741b2607402ac0f5ca676ab
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Extend dynamic semantics.
Add evaluation of non-empty vectors in unboxing.
Empty vectors, like some other evluations, need some additional type
information, which we will add soon.
Commit: 3b5d0dae964689c8baeb11f06c0e6ab3fa1a5d7f
https://github.com/acl2/acl2/commit/3b5d0dae964689c8baeb11f06c0e6ab3fa1a5d7f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-renaming-operations.lisp
Log Message:
-----------
[Remora] Factor some code.
Commit: a6e27844fe2d7211869dc1831ce03531a7d8fa07
https://github.com/acl2/acl2/commit/a6e27844fe2d7211869dc1831ce03531a7d8fa07
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/transformation/package.lsp
R books/kestrel/c/transformation/struct-safety-checks.lisp
A books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/top.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/projects/filesystems/utilities/cpp-syntax/package.lsp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Merge.
Commit: ba051b5e322af1a61e131268af6021d1814225df
https://github.com/acl2/acl2/commit/ba051b5e322af1a61e131268af6021d1814225df
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-renaming-operations.lisp
Log Message:
-----------
[Remora] Shorten some code.
Commit: 722d0e923e8418defe1128adee03e7d72dda0e79
https://github.com/acl2/acl2/commit/722d0e923e8418defe1128adee03e7d72dda0e79
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Extend dynamic semantics.
Add evaluation of `let` expressions.
Still need to add evaluation of bindings, which will be done next.
Commit: fc430b41913a0f902da6152117937a19bdddb87a
https://github.com/acl2/acl2/commit/fc430b41913a0f902da6152117937a19bdddb87a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Merge.
Commit: 71f5457849aa1d525d408f819bbc773d7dd80bce
https://github.com/acl2/acl2/commit/71f5457849aa1d525d408f819bbc773d7dd80bce
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/projects/abnf/grammar-definer/defgrammar-doc.lisp
M books/projects/abnf/grammar-definer/top.lisp
Log Message:
-----------
[ABNF] Improve organization.
Commit: 0c9c6a63221f278f58a18c72b2a645e464026484
https://github.com/acl2/acl2/commit/0c9c6a63221f278f58a18c72b2a645e464026484
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-renaming-operations.lisp
Log Message:
-----------
[Remora] Factor some code.
Commit: 1eefbacbb34b3ed53b76be25da9c4003741278a0
https://github.com/acl2/acl2/commit/1eefbacbb34b3ed53b76be25da9c4003741278a0
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/transformation/package.lsp
R books/kestrel/c/transformation/struct-safety-checks.lisp
A books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/top.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/projects/filesystems/utilities/cpp-syntax/package.lsp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Merge.
Commit: dee059f37c35a6548c18674b46ec14fbc77630d8
https://github.com/acl2/acl2/commit/dee059f37c35a6548c18674b46ec14fbc77630d8
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
Log Message:
-----------
[Remora] Add op on dynamic environments.
Commit: 1658ae819fba378acc37daeefa02727472357a64
https://github.com/acl2/acl2/commit/1658ae819fba378acc37daeefa02727472357a64
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Extend dynamic semantics.
Add evaluation of ispace bindings.
Commit: 9a74b69b30640b763d1df2b14f93c6ca9a886e82
https://github.com/acl2/acl2/commit/9a74b69b30640b763d1df2b14f93c6ca9a886e82
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
Log Message:
-----------
[Remora] Add an op on dynamic environments.
And also use it to simplify another one.
Commit: 5631675f828955d114123235b8e18c5404e4df5d
https://github.com/acl2/acl2/commit/5631675f828955d114123235b8e18c5404e4df5d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Extend dynamic semantics.
Add evaluation of type bindings.
Commit: 8f513499e376b8d0ad962fdb4c80cc71d2d9872e
https://github.com/acl2/acl2/commit/8f513499e376b8d0ad962fdb4c80cc71d2d9872e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-renaming-operations.lisp
Log Message:
-----------
[Remora] Fix no-capture checks in renamings.
The `let` was not handled sequentially. Now it is.
Commit: f5c05e68c9c5f5682499346b38c2e84fbb403128
https://github.com/acl2/acl2/commit/f5c05e68c9c5f5682499346b38c2e84fbb403128
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-operations.lisp
Log Message:
-----------
[Remora] Fix substitution no-capture predicates.
They were handling `let` as if parallel, but it is sequential.
Commit: da83c26547e1264a6b55fe98a06b242cda7bc3ba
https://github.com/acl2/acl2/commit/da83c26547e1264a6b55fe98a06b242cda7bc3ba
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Extend dynamic semantics.
Add evaluation of `val` bindings.
Commit: 1a375210b366e033b3f07b07cf42a06247efdc82
https://github.com/acl2/acl2/commit/1a375210b366e033b3f07b07cf42a06247efdc82
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Extend type checking.
Add checkers for shapes and ispaces.
Commit: dc7ba5efe01fafb2476f9a3c88a019ca4b0d7aef
https://github.com/acl2/acl2/commit/dc7ba5efe01fafb2476f9a3c88a019ca4b0d7aef
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Add evaluation of `fun` bindings.
Commit: a29cb8319949885b7bc360a6d24e6db3c87f53e5
https://github.com/acl2/acl2/commit/a29cb8319949885b7bc360a6d24e6db3c87f53e5
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Add checker for types themselves.
Commit: 237e0f937e7d8a3c31c685d244920b2c351d752b
https://github.com/acl2/acl2/commit/237e0f937e7d8a3c31c685d244920b2c351d752b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Add evaluation of type function bindings.
Commit: 34f28d200d825dd5140afbb420db067a23129ba6
https://github.com/acl2/acl2/commit/34f28d200d825dd5140afbb420db067a23129ba6
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Add evaluation of ispace function bindings.
Commit: 4b851765f758d4a82babde7c6904179f654fc9e6
https://github.com/acl2/acl2/commit/4b851765f758d4a82babde7c6904179f654fc9e6
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Add evaluation of combined function binders.
Commit: e7252dbf93dc8d17820c1c9280885bfb5d83471a
https://github.com/acl2/acl2/commit/e7252dbf93dc8d17820c1c9280885bfb5d83471a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Improve type checking.
Use the new checkers for types and ispaces, subsuming and supplanting the checks
for type and ispace variables in scope.
Commit: 259092ff0f49f22a85688c2bb5841a5a2d5319ff
https://github.com/acl2/acl2/commit/259092ff0f49f22a85688c2bb5841a5a2d5319ff
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
Log Message:
-----------
Merge.
Commit: cc591f7be808372ada385a65a9966005175fb77f
https://github.com/acl2/acl2/commit/cc591f7be808372ada385a65a9966005175fb77f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/kestrel/auto-termination/td-cands.lisp
M books/kestrel/c/language/grammar.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/java/language/grammar.lisp
M books/kestrel/json/grammar.lisp
M books/kestrel/remora/grammar.lisp
M books/kestrel/yul/language/grammar-old.lisp
M books/kestrel/yul/language/grammar.lisp
M books/projects/abnf/examples/imap.lisp
M books/projects/abnf/examples/imf.lisp
M books/projects/abnf/examples/pdf.lisp
M books/projects/abnf/examples/uri.lisp
M books/projects/abnf/grammar-definer/defgrammar-doc.lisp
R books/projects/abnf/grammar-definer/deftreeops-doc.lisp
R books/projects/abnf/grammar-definer/deftreeops.lisp
M books/projects/abnf/grammar-definer/top.lisp
A books/projects/abnf/tree-operations/deftreeops-doc.lisp
A books/projects/abnf/tree-operations/deftreeops.lisp
M books/projects/abnf/tree-operations/top.lisp
M books/projects/aleo/leo/early-version/definition/grammar.lisp
M books/projects/aleo/leo/grammar.lisp
M books/projects/aleo/vm/language/early-version/grammar.lisp
M books/projects/aleo/vm/language/grammar.lisp
M books/projects/pfcs/grammar.lisp
Log Message:
-----------
Merge.
Commit: 2acfa75b050ce8499047d7ffb41b96a0fb5632d3
https://github.com/acl2/acl2/commit/2acfa75b050ce8499047d7ffb41b96a0fb5632d3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/validation-annotations.lisp
Log Message:
-----------
[C$] Add fixtype for type validation information.
This will replace all the validation information fixtypes that are isomorphic to
this one.
Commit: 2f9f13e162e12e079c289f1140f19784d19d2d53
https://github.com/acl2/acl2/commit/2f9f13e162e12e079c289f1140f19784d19d2d53
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C$] Replace some specific validation information.
Commit: 4969c7aac415c38f46eb4a74d6006db2ccf90bbc
https://github.com/acl2/acl2/commit/4969c7aac415c38f46eb4a74d6006db2ccf90bbc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Replace some specific validation information.
Commit: 70f07dc04fe06ebf24184b42730c17f08fc5ec1a
https://github.com/acl2/acl2/commit/70f07dc04fe06ebf24184b42730c17f08fc5ec1a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Replace some specific validation information.
Commit: 6a04798c02585d00838598632744c9c04904297d
https://github.com/acl2/acl2/commit/6a04798c02585d00838598632744c9c04904297d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Replace some specific validation information.
Commit: 90f6e470fadd3660110b67b5894bfca7cf1e43e4
https://github.com/acl2/acl2/commit/90f6e470fadd3660110b67b5894bfca7cf1e43e4
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C$] Replace some specific validation information.
Commit: 8c4386eb1951761d6acfcb0fa4b4add832589a0b
https://github.com/acl2/acl2/commit/8c4386eb1951761d6acfcb0fa4b4add832589a0b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C$] Replace some specific validation information.
Commit: a3d7d0ffa599173748eee8073eb3c40ea333aab6
https://github.com/acl2/acl2/commit/a3d7d0ffa599173748eee8073eb3c40ea333aab6
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[C$] Replace some specific validation information.
Commit: fc233b2258ddbabb4c96f96fe6f60f7a104d63f5
https://github.com/acl2/acl2/commit/fc233b2258ddbabb4c96f96fe6f60f7a104d63f5
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/validation-annotations.lisp
Log Message:
-----------
[C$] Expand some doc.
Commit: 8ce70c9a858aaa0a7144ebf3ba86231e66517370
https://github.com/acl2/acl2/commit/8ce70c9a858aaa0a7144ebf3ba86231e66517370
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/validation-annotations.lisp
Log Message:
-----------
[C$] Add a fixtype for validation information.
Commit: 0be2dbecffb77b2a0647e09829643410b611e93e
https://github.com/acl2/acl2/commit/0be2dbecffb77b2a0647e09829643410b611e93e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/validation-annotations.lisp
Log Message:
-----------
[C$] Move some code within file.
Commit: eeb7253a2b3ed92fdd0342ae5e6e33eb7339da61
https://github.com/acl2/acl2/commit/eeb7253a2b3ed92fdd0342ae5e6e33eb7339da61
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/package.lsp
Log Message:
-----------
[C] Import two symbols.
Commit: 98bff015cf2b8234c8df0a926e1bee40612d4021
https://github.com/acl2/acl2/commit/98bff015cf2b8234c8df0a926e1bee40612d4021
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[C$] Replace some specific validation information.
Commit: 9d4cb6df94caf62408fd3725a3332bc229fc6ca2
https://github.com/acl2/acl2/commit/9d4cb6df94caf62408fd3725a3332bc229fc6ca2
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[C$] Replace some specific validation information.
Commit: 17743952975c04550a3a3d74f09e8b0e4f2ba847
https://github.com/acl2/acl2/commit/17743952975c04550a3a3d74f09e8b0e4f2ba847
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Replace some specific validation information.
Commit: 4257bbff8806b20b8fc0510c4741d26dcba1e92b
https://github.com/acl2/acl2/commit/4257bbff8806b20b8fc0510c4741d26dcba1e92b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/examples/strcpy-safe-induction.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C$] Rename a fixtype.
Commit: 449fc81b52e30e018c5b1e4b2e3b3e9209438aa2
https://github.com/acl2/acl2/commit/449fc81b52e30e018c5b1e4b2e3b3e9209438aa2
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
Log Message:
-----------
[C$] Improve some names.
Commit: 35168d586e5cc350c1e653a72b3e20253a8b2a0a
https://github.com/acl2/acl2/commit/35168d586e5cc350c1e653a72b3e20253a8b2a0a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/package.lsp
Log Message:
-----------
[C] Import a symbol.
Commit: b3bde209de13765f53f6c77f70d0c95ebfd94d1f
https://github.com/acl2/acl2/commit/b3bde209de13765f53f6c77f70d0c95ebfd94d1f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/fty/top.lisp
A books/kestrel/fty/true-list-set.lisp
Log Message:
-----------
[FTY] Add a fixtype of sets of true lists.
Commit: 1e4ca5c435923ee81d805de57272044db2b527e7
https://github.com/acl2/acl2/commit/1e4ca5c435923ee81d805de57272044db2b527e7
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Improve some names.
Commit: 93d0f999e162e3401c44031b3b9dbc8ad4f68e1a
https://github.com/acl2/acl2/commit/93d0f999e162e3401c44031b3b9dbc8ad4f68e1a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Improve some names.
Commit: 89a95aa5232447db1cc278228c040b8814cd6df7
https://github.com/acl2/acl2/commit/89a95aa5232447db1cc278228c040b8814cd6df7
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)
Changed paths:
M books/kestrel/c/package.lsp
M books/kestrel/fty/top.lisp
A books/kestrel/fty/true-list-set.lisp
Log Message:
-----------
Merge.
Commit: 698fddd77fab67dd99d2488869e22a7bb72d3f78
https://github.com/acl2/acl2/commit/698fddd77fab67dd99d2488869e22a7bb72d3f78
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] added popc and updated docs for primitives-evaluation.lisp
Commit: cee19cb94c32629028f0c02edf1fbe4bdc752c2e
https://github.com/acl2/acl2/commit/cee19cb94c32629028f0c02edf1fbe4bdc752c2e
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] added popc and updated docs for primitives-evaluation.lisp
Commit: 97a9e5c925de2a943f9c7c468e083f5dbf3cdfef
https://github.com/acl2/acl2/commit/97a9e5c925de2a943f9c7c468e083f5dbf3cdfef
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] fixed popc in primitves-evaluation.lisp
Commit: 9b45ff9108e72ac477d4dfb45dace5203ba7c437
https://github.com/acl2/acl2/commit/9b45ff9108e72ac477d4dfb45dace5203ba7c437
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] removed zerop in primitives-evaluation.lisp
Commit: f8fa0a585c64520b87e45c0200441fda43c01a66
https://github.com/acl2/acl2/commit/f8fa0a585c64520b87e45c0200441fda43c01a66
Author: Alessandro Coglio <
2409151...@users.noreply.github.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
Merge pull request #1956 from ltmquan/remora
[REMORA] added other integer operations into primitives-evaluation.lisp
Commit: c5a55b978bed20dda90648b015fb7bc885c163bd
https://github.com/acl2/acl2/commit/c5a55b978bed20dda90648b015fb7bc885c163bd
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/package.lsp
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] added check-expr-value-bool in primitives-evaluation.lisp
Commit: 5503b12670ab1307496eae4868c6a4cb9b40af26
https://github.com/acl2/acl2/commit/5503b12670ab1307496eae4868c6a4cb9b40af26
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] added boolean primitives to primitives-evaluation.lisp
Commit: 9da52ad7ec266e0ecae713ef5da0740171f77a79
https://github.com/acl2/acl2/commit/9da52ad7ec266e0ecae713ef5da0740171f77a79
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] fixed bug in prim-bool-to-float in primitives-evaluation.lisp
Commit: 438cb04e0d20254b41edcd1b4cacfee10625edbd
https://github.com/acl2/acl2/commit/438cb04e0d20254b41edcd1b4cacfee10625edbd
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/arithmetic-light/times.lisp
Log Message:
-----------
[arithmetic-light] Add a rule.
Commit: 056fdb2cd8aecf861c866ab01f24866c1d5a3c45
https://github.com/acl2/acl2/commit/056fdb2cd8aecf861c866ab01f24866c1d5a3c45
Author: Alessandro Coglio <
2409151...@users.noreply.github.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/package.lsp
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
Merge pull request #1958 from ltmquan/remora
REMORA - Adding boolean primitives
Commit: d6080e02ee0adf38e5a531f8d9f249fdda4a987c
https://github.com/acl2/acl2/commit/d6080e02ee0adf38e5a531f8d9f249fdda4a987c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Improve some doc.
Commit: 1fbcd97d91c466e7ab9c91df84074d94c369125a
https://github.com/acl2/acl2/commit/1fbcd97d91c466e7ab9c91df84074d94c369125a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/static-environments.lisp
Log Message:
-----------
[Remora] Improve a name.
For consistency with upcoming extensions.
Commit: cd6679b8bbda8240361a7257909c7bc49e09af48
https://github.com/acl2/acl2/commit/cd6679b8bbda8240361a7257909c7bc49e09af48
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Add model of primitive ops as values.
Commit: 8a0422e67eb04a351c485fab189ee35e1b5f0e8e
https://github.com/acl2/acl2/commit/8a0422e67eb04a351c485fab189ee35e1b5f0e8e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/projects/abnf/top.lisp
Log Message:
-----------
[ABNF] Improve top-level doc.
Commit: 2c797caa7970f2fec27fcb0f657f41fc5e35ecde
https://github.com/acl2/acl2/commit/2c797caa7970f2fec27fcb0f657f41fc5e35ecde
Author: Yahya Sohail <
ya...@yahyasohail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
Log Message:
-----------
Fix VPOR VEX dispatch operation code
The VEX-encoded VPOR dispatch entries passed the XOR opcode constant instead of the OR opcode constant, causing the model to compute XMM9 ^ XMM10 (XOR) rather than XMM9 | XMM10 (OR) for every VPOR invocation.
Change the two (operation . #x5) entries to (operation . #.*OP-OR*) in inst-listing.lisp so that VEX-encoded VPOR performs a bitwise OR, using the symbolic constant used elsewhere in the instruction table.
Verified by make test in tools/execution/asmtest:
testgen_2555 (VPOR): 0 mismatches
Commit: 4bb7ddb6d91cb870b58eab4badfb5a145d693dcf
https://github.com/acl2/acl2/commit/4bb7ddb6d91cb870b58eab4badfb5a145d693dcf
Author: Yahya Sohail <
ya...@yahyasohail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
Log Message:
-----------
Preserve flags in shifts/rotates when count is zero
Per the Intel SDM, when the shift count is 0 no flags are affected for
SAL/SHL/SAR/SHR (sal:sar:shl:shr:551), SHLD/SHRD (shld:119, shrd:119),
and RCL/RCR/ROL/ROR (rcl:rcr:rol:ror:584). The spec functions in
shifts-spec.lisp and rotates-spec.lisp already handled the count=0
case for most instructions, but ROL/ROR marked OF as undefined for
src=0, contradicting the SDM ("For ROL and ROR instructions, if the
masked count is 0, the flags are not affected").
This commit:
1. Fixes rol-spec-gen and ror-spec-gen so their (src=0) branch
returns (mv input-rflags 0) instead of marking OF as undefined.
2. Removes the count=0 short-circuit at the dispatch sites in
x86-sal/sar/shl/shr/rcl/rcr/rol/ror and x86-shld/shrd. The
flag-preservation logic now lives entirely in the spec functions
(where the comment on each function notes the count=0 case), per
the review feedback that the dispatch site should not duplicate
flag computation.
The result of removing the short-circuit is functionally identical to
the prior behavior for SAL/SHL/SAR/SHR/RCL/RCR/SHLD/SHRD (whose spec
functions already returned (mv input-rflags 0) for count=0) and a
behavior fix for ROL/ROR.
Verified by make test in tools/execution/asmtest (after
cert.pl on
top and asmtest):
ROL/ROR (no specific count=0 tests, but full-suite ROL/ROR
snippets report 0 mismatches):
testgen_365 (ROL r8b, imm8): 0
testgen_367 (ROL r64, imm8): 0
testgen_377 (ROR r8b, imm8): 0
testgen_378 (ROR r64, imm8): 0
testgen_397 (ROR r8b, CL): 0
testgen_399 (ROR r64, CL): 0
Sal/shl/sar/shr/shld/shrd (count=0 cascade mismatches from prior
instructions in the loop remain, per the PR description):
testgen_429 (SHL r8b): count=0 mismatches eliminated
testgen_433 (SHL r64): 0
testgen_435 (SHL r32): 0
testgen_445 (SHR r8b): count=0 mismatches eliminated
testgen_447 (SHR r32): 0
testgen_457 (SAR r8b): count=0 mismatches eliminated
testgen_459 (SAR r64): 0
testgen_1642 (SHRD): 0
testgen_1646 (SHLD): 0
Other PR fixes still pass:
testgen_1332 (CMPPS): 0
testgen_1345 (CMPSS): 0
testgen_1347 (CMPPD): 0
testgen_1351 (CMPSD): 0
testgen_666 (PSRLDQ): 0
testgen_667 (PSLLDQ): 0
testgen_2025 (LZCNT): 0
testgen_2555 (VPOR): 0
Commit: a2fefce3fdc125bca8abf3f776f2184beca8d653
https://github.com/acl2/acl2/commit/a2fefce3fdc125bca8abf3f776f2184beca8d653
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/projects/abnf/grammar-definer/top.lisp
M books/projects/abnf/grammar-parser/top.lisp
M books/projects/abnf/grammar-printer/top.lisp
M books/projects/abnf/notation/top.lisp
Log Message:
-----------
[ABNF] XDOC hierarchy tweaks.
Commit: c7511d43260f0c9ae4e22b585d81dfdd0838a62b
https://github.com/acl2/acl2/commit/c7511d43260f0c9ae4e22b585d81dfdd0838a62b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-renaming-operations.lisp
Log Message:
-----------
[Remora] Fix handling of `let` in ispace variable renaming.
Commit: dba385deb1e5b95255a6abfcf18e0e0b28ee1041
https://github.com/acl2/acl2/commit/dba385deb1e5b95255a6abfcf18e0e0b28ee1041
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-renaming-operations.lisp
Log Message:
-----------
[Remora] Fix handling of `let` in type variable renaming.
Commit: 4c2cc0ddf8966fb9f1a31374fb1436a7889c37b6
https://github.com/acl2/acl2/commit/4c2cc0ddf8966fb9f1a31374fb1436a7889c37b6
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-renaming-operations.lisp
Log Message:
-----------
[Remora] Fix handling of `let` in expression variable renaming.
Commit: f0c623058d1252f235262ca118f71b0be01c030c
https://github.com/acl2/acl2/commit/f0c623058d1252f235262ca118f71b0be01c030c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-operations.lisp
Log Message:
-----------
[Remora] Fix handling of `let` in ispace variable substitution.
Commit: e1dd78d12836ac641300d32d38bc7aae4123c80d
https://github.com/acl2/acl2/commit/e1dd78d12836ac641300d32d38bc7aae4123c80d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/static-environments.lisp
Log Message:
-----------
[Remora] Improve initial static environment.
Now it consists of the selection of primitive operations whose dynamic semantics
is in `primitives-evaluation.lisp`. The exact names are taken by the
`RemoraPrelude.hs` file in the Haskell implementation of Remora.
Commit: a6e0b85943ee7d84dc4aeb0cd8633cb838078f6e
https://github.com/acl2/acl2/commit/a6e0b85943ee7d84dc4aeb0cd8633cb838078f6e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Align the model of primitive operation values.
This is now consistent with the ones in `primitives-evaluation.lisp` and the
ones in the initial static environment (see `primop-types`).
Commit: 01d4b00572aa4a7add29d52b2a1f422f80374ca2
https://github.com/acl2/acl2/commit/01d4b00572aa4a7add29d52b2a1f422f80374ca2
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/package.lsp
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
Merge.
Commit: 1214e99af8ab2941c92cd8c173f610e7ea35fe02
https://github.com/acl2/acl2/commit/1214e99af8ab2941c92cd8c173f610e7ea35fe02
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-operations.lisp
Log Message:
-----------
[Remora] Fix handling of `let` in type variable substitution.
Commit: 178bae66cbbc6156409d38bff89128e2fbba29dc
https://github.com/acl2/acl2/commit/178bae66cbbc6156409d38bff89128e2fbba29dc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-operations.lisp
Log Message:
-----------
[Remora] Fix handling of `let` in expression variable substitution.
Commit: f9cdc1ae777ab2a3ae74813d5c5f539df6896664
https://github.com/acl2/acl2/commit/f9cdc1ae777ab2a3ae74813d5c5f539df6896664
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Extend primitive operation types and values.
Align to latest `primitives-evaluation.lisp`.
Commit: 0cfab1ba781dd45aa82a0f9c4433dbc60166841c
https://github.com/acl2/acl2/commit/0cfab1ba781dd45aa82a0f9c4433dbc60166841c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Extend model of expression values.
Add a summand for primitive operations. Minimally extend evaluation machinery to
certify, but proper handling of primitive operations will be added in upcoming
commits.
Commit: 4649f0e23b13dadd0d1a8af34ee3c1996ae7055f
https://github.com/acl2/acl2/commit/4649f0e23b13dadd0d1a8af34ee3c1996ae7055f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Add type checking of bracket expressions.
Commit: 441fac232f86b97f0806a9a411fad99b059e53dd
https://github.com/acl2/acl2/commit/441fac232f86b97f0806a9a411fad99b059e53dd
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/package.lsp
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
Merge.
Commit: 33855b26ecbbeb3e1e519c1641e6960a9bf58da6
https://github.com/acl2/acl2/commit/33855b26ecbbeb3e1e519c1641e6960a9bf58da6
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/static-environments.lisp
Log Message:
-----------
[Remora] Improve a variable name.
Commit: 10bcffad7257cb9fc63c218807b0be60da2404a3
https://github.com/acl2/acl2/commit/10bcffad7257cb9fc63c218807b0be60da2404a3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
Log Message:
-----------
[Remora] Define the initial dynamic environment.
This contains the (current) primitive operations.
Commit: b0b796f95f9fce3e042df6ad67f8ebab4c8c882c
https://github.com/acl2/acl2/commit/b0b796f95f9fce3e042df6ad67f8ebab4c8c882c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Add mapping of primitive ops to their arities.
Commit: 9dbb0929caf2ab0762769218ff586ecdf35a6e98
https://github.com/acl2/acl2/commit/9dbb0929caf2ab0762769218ff586ecdf35a6e98
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/crypto/sha-3/sha-3.lisp
Log Message:
-----------
[sha-3] Clean up a bit.
Commit: 33136a011d37097886e548e5110d1c768d5a6fbe
https://github.com/acl2/acl2/commit/33136a011d37097886e548e5110d1c768d5a6fbe
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Factor some type-checking code.
This is in preparation for an extension, but it has the added benefit of
obviating the need for a specific lemma with slightly large hints.
Commit: 052609bd649b9ceb0adbffffbf6cfe62a34f35f2
https://github.com/acl2/acl2/commit/052609bd649b9ceb0adbffffbf6cfe62a34f35f2
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[Remora] Add top-level primitive op evaluator.
Commit: 798cf70870b63896175fa7dfa4a572011e9a747a
https://github.com/acl2/acl2/commit/798cf70870b63896175fa7dfa4a572011e9a747a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Factor some type-checking code.
This is for an upcoming extension.
Commit: 85feba13a8cd5c81a2ef8014bed92dff50340cb4
https://github.com/acl2/acl2/commit/85feba13a8cd5c81a2ef8014bed92dff50340cb4
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Factor some type-checking code.
To support an upcoming extension.
Commit: 3c6846ef5d967e8a27ce02948046f2e51b03ae3e
https://github.com/acl2/acl2/commit/3c6846ef5d967e8a27ce02948046f2e51b03ae3e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Avoid deferring some guard proofs.
Commit: 6d3825d8a6a87fa4b0fb22856db2cd29af8326c3
https://github.com/acl2/acl2/commit/6d3825d8a6a87fa4b0fb22856db2cd29af8326c3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Add type checking of combine applications.
Commit: c84f27ba7da7b6059a7cc1c9e97bc75f2215bed5
https://github.com/acl2/acl2/commit/c84f27ba7da7b6059a7cc1c9e97bc75f2215bed5
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Remove some now-unneeded doc.
Commit: b5e292de3b867084a538076f2b6fb99e25947707
https://github.com/acl2/acl2/commit/b5e292de3b867084a538076f2b6fb99e25947707
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Generalize some dynamic semantics code.
Instead of just looking for a representative lambda abstraction in a function
array, we also look for a primitive operation. We add code to treat them
uniformly.
Commit: 7ec08c21246005762781c72502ff230526cb654a
https://github.com/acl2/acl2/commit/7ec08c21246005762781c72502ff230526cb654a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/static-environments.lisp
Log Message:
-----------
[Remora] Add a result fixtype.
Commit: 1ecaefed3fdb1cb3c21602b6009f3d3a657551e8
https://github.com/acl2/acl2/commit/1ecaefed3fdb1cb3c21602b6009f3d3a657551e8
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Add type checking of most let bindings.
Commit: 597fbd286612ecefc04f0a8c8705a099c98908bc
https://github.com/acl2/acl2/commit/597fbd286612ecefc04f0a8c8705a099c98908bc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Complete evaluation of primitive ops.
Connect the machinery to the main evaluation functions.
Commit: 84466e477888b5de82291ad1f6ee7aafbf4f55e3
https://github.com/acl2/acl2/commit/84466e477888b5de82291ad1f6ee7aafbf4f55e3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Some cleanup.
Commit: 6798217219c807c9538ec2e31630cc4059b10021
https://github.com/acl2/acl2/commit/6798217219c807c9538ec2e31630cc4059b10021
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Avoid a theorem by enabling an existing rule.
Commit: 9c3fa975f72b765e697c0bb4524ea0cf041c1fa1
https://github.com/acl2/acl2/commit/9c3fa975f72b765e697c0bb4524ea0cf041c1fa1
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/nat-lists.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Factor library theorem.
Commit: fded670186a5d942ba860c17d4bbf0fb6f4ca76a
https://github.com/acl2/acl2/commit/fded670186a5d942ba860c17d4bbf0fb6f4ca76a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Shorten a function name.
Commit: daaa1619ce2d19f432ed44c0cc27d90bc72aae46
https://github.com/acl2/acl2/commit/daaa1619ce2d19f432ed44c0cc27d90bc72aae46
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
Log Message:
-----------
Merge.
Commit: d32054e3ebbf26df997e99a44703b2cb08a29d72
https://github.com/acl2/acl2/commit/d32054e3ebbf26df997e99a44703b2cb08a29d72
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/projects/abnf/grammar-definer/top.lisp
M books/projects/abnf/grammar-parser/top.lisp
M books/projects/abnf/grammar-printer/top.lisp
M books/projects/abnf/notation/top.lisp
M books/projects/abnf/top.lisp
Log Message:
-----------
Merge.
Commit: 977d26eabbf7a99f2b6d6bd3cd2fb579a9af9ad1
https://github.com/acl2/acl2/commit/977d26eabbf7a99f2b6d6bd3cd2fb579a9af9ad1
Author: Eric McCarthy <
bend...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/package.lsp
M books/kestrel/remora/printer.lisp
Log Message:
-----------
[remora] Refactor prettyprinter so it goes through unicode codepoints. Probably improves layout for some non-ASCII identifiers. Makes upcoming round-trip proofs easier.
Commit: 03fd017016cc56a9f08ac4bff030c2595e428d25
https://github.com/acl2/acl2/commit/03fd017016cc56a9f08ac4bff030c2595e428d25
Author: Eric McCarthy <
bend...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/printer.lisp
Log Message:
-----------
[remora] fix some xdoc and add xdoc for macro pdoc-ascii
Commit: cd0f0951a7da750dc44e2f0bafd949488eec32ff
https://github.com/acl2/acl2/commit/cd0f0951a7da750dc44e2f0bafd949488eec32ff
Author: Eric McCarthy <
bend...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/printer.lisp
Log Message:
-----------
[remora] fix more xdoc
Commit: 39e12b30477263ef223237e744f7c3a994502e3d
https://github.com/acl2/acl2/commit/39e12b30477263ef223237e744f7c3a994502e3d
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/x86/alt-defs.lisp
Log Message:
-----------
[x86] Fix alt-def proof.
Commit: cc0d7099c8b83229adbd795a3131b72fb04b6472
https://github.com/acl2/acl2/commit/cc0d7099c8b83229adbd795a3131b72fb04b6472
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/nat-lists.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/values.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/projects/abnf/grammar-definer/top.lisp
M books/projects/abnf/grammar-parser/top.lisp
M books/projects/abnf/grammar-printer/top.lisp
M books/projects/abnf/notation/top.lisp
M books/projects/abnf/top.lisp
Log Message:
-----------
Merge.
Commit: fe21eab8621ef72e3b2aa505a3c0c564d3bca634
https://github.com/acl2/acl2/commit/fe21eab8621ef72e3b2aa505a3c0c564d3bca634
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
A books/projects/abnf/tree-operations/acl2-customization.lsp
Log Message:
-----------
[ABNF] Add customization file to subdir.
Commit: d6b95d911ea5f22b0c1458d2042066777470af96
https://github.com/acl2/acl2/commit/d6b95d911ea5f22b0c1458d2042066777470af96
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/projects/abnf/notation/semantics.lisp
A books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/abnf/tree-operations/top.lisp
Log Message:
-----------
[ABNF] Move some tree ops to a new file/topic.
Commit: 2fbc9ff0c8e5c9973cba459fb839fd787e7e0541
https://github.com/acl2/acl2/commit/2fbc9ff0c8e5c9973cba459fb839fd787e7e0541
Author: Eric McCarthy <
bend...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
A books/kestrel/terms-light/doc.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term-tests.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-proofs.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-tests.lisp
A books/kestrel/terms-light/simple-untranslate-in-term.lisp
Log Message:
-----------
[terms-light] add simple-untranslate-in-term
Commit: a42412fd5fedef0f5cea871a6427d75f7d86bee1
https://github.com/acl2/acl2/commit/a42412fd5fedef0f5cea871a6427d75f7d86bee1
Author: Eric McCarthy <
bend...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/top-doc.lisp
Log Message:
-----------
[terms-light] connect xdoc to manual
Commit: b01b45d43f21611b863f07895452c9ea9de20d4d
https://github.com/acl2/acl2/commit/b01b45d43f21611b863f07895452c9ea9de20d4d
Author: Eric McCarthy <
bend...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
A books/kestrel/terms-light/doc.acl2
M books/kestrel/terms-light/doc.lisp
Log Message:
-----------
[terms-light] load C portcullis so doc reference works
Commit: eaa850a338ba1894363c56c350ffbd99d7f96e0e
https://github.com/acl2/acl2/commit/eaa850a338ba1894363c56c350ffbd99d7f96e0e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/extra-grammatical-restrictions.lisp
Log Message:
-----------
[Remora] Adapt to ABNF library changes.
Commit: 78ea53e2a60ab2d74fbfbe89340d729810a10970
https://github.com/acl2/acl2/commit/78ea53e2a60ab2d74fbfbe89340d729810a10970
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
Log Message:
-----------
[Remora] Add a fixtype.
Commit: a121585bcf6b74948310e50200260d11c36e10d6
https://github.com/acl2/acl2/commit/a121585bcf6b74948310e50200260d11c36e10d6
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
Log Message:
-----------
[Remora] Add some derived fixtypes.
Commit: 7bd22ea11267a1c7cafd6dde37eb0f3350f26249
https://github.com/acl2/acl2/commit/7bd22ea11267a1c7cafd6dde37eb0f3350f26249
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/rules.lisp
Log Message:
-----------
[bv] Move and improve a rule.
Commit: 6d688a1eacdba2741980565fece052ecab6bd2da
https://github.com/acl2/acl2/commit/6d688a1eacdba2741980565fece052ecab6bd2da
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Generalize static environments.
Instead of just sets of ispace and type variables, use maps from ispace and type
variables to optional ispaces and optional types. These are equivalent to sets
when the optional ispaces and types are absent, but they will be present in an
upcoming extension to handle `let`s of ispaces and types.
Commit: ffa75ee4b479e0f30ffed4a873e9d5a03a2b1103
https://github.com/acl2/acl2/commit/ffa75ee4b479e0f30ffed4a873e9d5a03a2b1103
Author: Eric McCarthy <
bend...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/terms-light/doc.lisp
M books/kestrel/terms-light/top.lisp
Log Message:
-----------
[terms-light] add more xdoc for terms-light utilities; include new files (except doc.lisp) in top.lisp
Commit: 5ed3d52fd91433329c6a314f7d12147a60c640b2
https://github.com/acl2/acl2/commit/5ed3d52fd91433329c6a314f7d12147a60c640b2
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
Log Message:
-----------
[Remora] Add a type annotation to the ASTs.
This is the type of the body of a lambda. The type is optional, because there is
no concrete syntax for it. It will be calculated by type checking.
Commit: f64e8259ddf1cff4c37ce27e1d51222f6beae320
https://github.com/acl2/acl2/commit/f64e8259ddf1cff4c37ce27e1d51222f6beae320
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/leftrotate32.lisp
M books/kestrel/bv/sbvlt.lisp
Log Message:
-----------
[bv] Add a few rules.
Commit: e3f880256dea579e614190daeb8b0cb9f7ce62bb
https://github.com/acl2/acl2/commit/e3f880256dea579e614190daeb8b0cb9f7ce62bb
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
Log Message:
-----------
[axe] Reduce includes.
Commit: 7a67604db2bab0126221a24448d57e0825311978
https://github.com/acl2/acl2/commit/7a67604db2bab0126221a24448d57e0825311978
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp
Log Message:
-----------
[axe/arm] Add a rule.
Commit: 7a43e37e81c7ccc0122036ec6d888b808bbda381
https://github.com/acl2/acl2/commit/7a43e37e81c7ccc0122036ec6d888b808bbda381
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
A books/kestrel/terms-light/doc.acl2
A books/kestrel/terms-light/doc.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term-tests.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-proofs.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-tests.lisp
A books/kestrel/terms-light/simple-untranslate-in-term.lisp
M books/kestrel/terms-light/top.lisp
M books/kestrel/top-doc.lisp
Log Message:
-----------
Merge.
Commit: 0195851704745971cfef8387172a2fa461c6fa88
https://github.com/acl2/acl2/commit/0195851704745971cfef8387172a2fa461c6fa88
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[C$] Keep to 80 columns.
Commit: 84da6ce4be738014f8973db71a203faa888f107d
https://github.com/acl2/acl2/commit/84da6ce4be738014f8973db71a203faa888f107d
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/types-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[C$] Add :unknown-builtin type
Commit: e6a8c4bcb772af557c594d0eef6584339056ad20
https://github.com/acl2/acl2/commit/e6a8c4bcb772af557c594d0eef6584339056ad20
Author: Eric McCarthy <
bend...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formed.lisp
Log Message:
-----------
[remora] update wf-ast-p to alow empty array and frame
Commit: 996e5aeb4b77122645622e529b8df624eee1ce21
https://github.com/acl2/acl2/commit/996e5aeb4b77122645622e529b8df624eee1ce21
Author: Eric McCarthy <
bend...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formed.lisp
Log Message:
-----------
[remora] in wf-ast-p, remove grammar non-emptiness requirements for :array and :frame
Commit: fb3eed579f18a362f6c9f4f26e92f0f414bd2edf
https://github.com/acl2/acl2/commit/fb3eed579f18a362f6c9f4f26e92f0f414bd2edf
Author: Yahya Sohail <
ya...@yahyasohail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/x86/alt-defs.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
Log Message:
-----------
Merge pull request #1957 from yaso9/x86isa-testgen-bug-fixes
x86isa: Fix 5 real model bugs in asmtest (CMPPS/PD/SS/SD, shifts, PSLLDQ/PSRLDQ, LZCNT, VPOR)
Commit: 703070e6f1dfbbb62de0f8d7d2d4b326f422c264
https://github.com/acl2/acl2/commit/703070e6f1dfbbb62de0f8d7d2d4b326f422c264
Author: ACL2 Build Server <
acl2bui...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/types-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
Merge commit '84da6ce4be738014f8973db71a203faa888f107d' into HEAD
Commit: 9b8be5833795f184e6f4d4b5a89378c6b54b9f44
https://github.com/acl2/acl2/commit/9b8be5833795f184e6f4d4b5a89378c6b54b9f44
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Log Message:
-----------
[C$] Export more symbols.
Commit: 6848e2c6c42df05614045a2492f5a865654f1a9b
https://github.com/acl2/acl2/commit/6848e2c6c42df05614045a2492f5a865654f1a9b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Improve doc and code.
Commit: 243dfab47d8aad22cee7176740da319cfbf6862f
https://github.com/acl2/acl2/commit/243dfab47d8aad22cee7176740da319cfbf6862f
Author: ACL2 Build Server <
acl2bui...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formed.lisp
Log Message:
-----------
Merge commit '996e5aeb4b77122645622e529b8df624eee1ce21' into HEAD
Commit: b80c81a4e83c26ff84cd3d4f32a5b46db609f153
https://github.com/acl2/acl2/commit/b80c81a4e83c26ff84cd3d4f32a5b46db609f153
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[C$] Fix doc typos.
Commit: 7cd3d071f8bdfb36a068235b9ba4da15f40d81bf
https://github.com/acl2/acl2/commit/7cd3d071f8bdfb36a068235b9ba4da15f40d81bf
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Improve model of lambda values.
Add a slot for an optional type value for the body, mirroring the AST.
Commit: 66220cb5906744f11043a657000cacb280e6858e
https://github.com/acl2/acl2/commit/66220cb5906744f11043a657000cacb280e6858e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Extend evaluation of lambdas.
Have it populate the optional type value slot.
Commit: 4e9b0c0e2b8faebf1652350fcdb94005171b9bc8
https://github.com/acl2/acl2/commit/4e9b0c0e2b8faebf1652350fcdb94005171b9bc8
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Add some code to handle ispace/type bindings.
These are functions to expand ispaces and types according to the maps in the
static environment.
Commit: 56f7e21d0308daf2dab567b580c721aa597aff6d
https://github.com/acl2/acl2/commit/56f7e21d0308daf2dab567b580c721aa597aff6d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Improve a definition.
Commit: e7f6bf072ac5f92e567bc28aba4db3242211e3f6
https://github.com/acl2/acl2/commit/e7f6bf072ac5f92e567bc28aba4db3242211e3f6
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Add mapping from primitive ops to their type values.
This is more general, and will subsume some of the other mappings.
Commit: 41a9c9bf91c91ed2e82643f35eacfb4e931124b5
https://github.com/acl2/acl2/commit/41a9c9bf91c91ed2e82643f35eacfb4e931124b5
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Add two more helper functions.
Commit: 634e0ce9b69c991bf82875d615f67deaf9b5b0b7
https://github.com/acl2/acl2/commit/634e0ce9b69c991bf82875d615f67deaf9b5b0b7
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Expand some doc.
Commit: a0c4a7cd6d9c593800ccb331aa51e453587c5bad
https://github.com/acl2/acl2/commit/a0c4a7cd6d9c593800ccb331aa51e453587c5bad
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Add two theorems and simplify a definition.
Now the arity of a primitive operation can be derived from its type.
Commit: 4870815b671d15f8334e2f717f798d149803573e
https://github.com/acl2/acl2/commit/4870815b671d15f8334e2f717f798d149803573e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Expand some doc.
Commit: 4f01bf61798c21ff69ec385b8ff83e8d0b1cf8e8
https://github.com/acl2/acl2/commit/4f01bf61798c21ff69ec385b8ff83e8d0b1cf8e8
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
Merge.
Commit: 0ca04219037c0f73cc25b029fc7b392ed1e704ac
https://github.com/acl2/acl2/commit/0ca04219037c0f73cc25b029fc7b392ed1e704ac
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/projects/abnf/notation/semantics.lisp
A books/projects/abnf/tree-operations/acl2-customization.lsp
A books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/abnf/tree-operations/top.lisp
Log Message:
-----------
Merge.
Commit: f6f7eed604b68ee8bd70192aee5081c191d7988a
https://github.com/acl2/acl2/commit/f6f7eed604b68ee8bd70192aee5081c191d7988a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/types-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
A books/kestrel/terms-light/doc.acl2
A books/kestrel/terms-light/doc.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term-tests.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-proofs.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-tests.lisp
A books/kestrel/terms-light/simple-untranslate-in-term.lisp
M books/kestrel/terms-light/top.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/x86/alt-defs.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
Log Message:
-----------
Merge.
Commit: ef9c1ec3776e57ff59f31af8ddd1640054533856
https://github.com/acl2/acl2/commit/ef9c1ec3776e57ff59f31af8ddd1640054533856
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Factor some code.
Commit: 41ee22b3ea62cb18d250c127b9420c2a6a04919f
https://github.com/acl2/acl2/commit/41ee22b3ea62cb18d250c127b9420c2a6a04919f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Start expanding tyeps and ispaces.
Commit: 02dfcd4bbd8b4ba009b1ac292c13b13238e4eadb
https://github.com/acl2/acl2/commit/02dfcd4bbd8b4ba009b1ac292c13b13238e4eadb
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/types-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/values.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/x86/alt-defs.lisp
M books/projects/abnf/notation/semantics.lisp
A books/projects/abnf/tree-operations/acl2-customization.lsp
A books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/abnf/tree-operations/top.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
Log Message:
-----------
Merge.
Commit: 4871385bfdb0c63128669456876a5bf1b08e7973
https://github.com/acl2/acl2/commit/4871385bfdb0c63128669456876a5bf1b08e7973
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/axe/rules3.lisp
Log Message:
-----------
[axe] Keep rule disabled.
Commit: ba3c1008d84de70bb4e839c4ac58f08dbf4b4a4c
https://github.com/acl2/acl2/commit/ba3c1008d84de70bb4e839c4ac58f08dbf4b4a4c
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] added 8 float operations to primitives-evaluation.lisp
Commit: ee7dd7ccdf3ee86a5edb3a52f1270f2944a7fb44
https://github.com/acl2/acl2/commit/ee7dd7ccdf3ee86a5edb3a52f1270f2944a7fb44
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] updated doc in primitives-evaluation.lisp
Commit: 5552e7785efcb4c1898ca634a6b31b3fdb240680
https://github.com/acl2/acl2/commit/5552e7785efcb4c1898ca634a6b31b3fdb240680
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] updated doc in primitives-evaluation.lisp
Commit: 4f76df36e1a9b07bf33a9642e7c53cff492bdfc1
https://github.com/acl2/acl2/commit/4f76df36e1a9b07bf33a9642e7c53cff492bdfc1
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] added all float ops into primitives-evaluation.lisp
Commit: dcd68e1d67450c5df1af061bc30216a53a5e2cdb
https://github.com/acl2/acl2/commit/dcd68e1d67450c5df1af061bc30216a53a5e2cdb
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
[REMORA] added float ops across remora
Commit: e22d4e5cfc0f7d92b95e45818f624ebb9712b96b
https://github.com/acl2/acl2/commit/e22d4e5cfc0f7d92b95e45818f624ebb9712b96b
Author: ltmquan <
ltmqu...@gmail.com>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/primitives-evaluation.lisp
Log Message:
-----------
[REMORA] updated doc in primitives-evaluation.lisp
Commit: 767e586a17b38c403cb2c9b3b9732c51b2602d1b
https://github.com/acl2/acl2/commit/767e586a17b38c403cb2c9b3b9732c51b2602d1b
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[C2C] Fix typo in struct-type-split
Memberp expressions were accidentally being transformed into member
expressions in some situations. This was a copy/paste error.
Commit: 858b874ae0321bc9ece93d3d96394d2d6d6fec3d
https://github.com/acl2/acl2/commit/858b874ae0321bc9ece93d3d96394d2d6d6fec3d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Add another type expansion.
Commit: e4fb623603df0c16cb2bb009489f339b69a6afe4
https://github.com/acl2/acl2/commit/e4fb623603df0c16cb2bb009489f339b69a6afe4
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/arithmetic-light/times.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/leftrotate32.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/sbvlt.lisp
M books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/types-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/crypto/sha-3/sha-3.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/values.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
A books/kestrel/terms-light/doc.acl2
A books/kestrel/terms-light/doc.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term-tests.lisp
A books/kestrel/terms-light/reconstruct-and-untranslate-term.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-proofs.lisp
A books/kestrel/terms-light/simple-untranslate-in-term-tests.lisp
A books/kestrel/terms-light/simple-untranslate-in-term.lisp
M books/kestrel/terms-light/top.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/x86/alt-defs.lisp
M books/projects/abnf/notation/semantics.lisp
A books/projects/abnf/tree-operations/acl2-customization.lsp
A books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/abnf/tree-operations/top.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
Log Message:
-----------
Merge.
Commit: 33907ec421d78f70d53cfd55d84c6561832672e9
https://github.com/acl2/acl2/commit/33907ec421d78f70d53cfd55d84c6561832672e9
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Generalize some code.
Commit: c09e2efbba98816a08a63492c0f933a945ba3e2b
https://github.com/acl2/acl2/commit/c09e2efbba98816a08a63492c0f933a945ba3e2b
Author: Alessandro Coglio <
2409151...@users.noreply.github.com>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
Merge pull request #1959 from ltmquan/remora
REMORA - Adding 8 float operations into `primitives-evaluation.lisp`
Commit: 08f4d1ac084e572fc83b51e95f644596fbc2a9a5
https://github.com/acl2/acl2/commit/08f4d1ac084e572fc83b51e95f644596fbc2a9a5
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Expand types in another place.
Commit: 6919ff5ff5a1862499ef92a531aabf6871d6c900
https://github.com/acl2/acl2/commit/6919ff5ff5a1862499ef92a531aabf6871d6c900
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Add remaining type expansions.
Commit: 4b98ebc5bf2f7df77fa07f31890365bf17f4b43b
https://github.com/acl2/acl2/commit/4b98ebc5bf2f7df77fa07f31890365bf17f4b43b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Add another supporting operation.
Commit: 208d39e8867ccc9ab0f706e4ac3d95850fcc20ac
https://github.com/acl2/acl2/commit/208d39e8867ccc9ab0f706e4ac3d95850fcc20ac
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Handle empty principal frames in applications.
Commit: 65205441c3b686a3d966323a70c1430ff3b71320
https://github.com/acl2/acl2/commit/65205441c3b686a3d966323a70c1430ff3b71320
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[C2C] Make sts-print-warnings tail-recursive
Commit: 5ecbed745cee652b9eacb7af90842c795ed73a87
https://github.com/acl2/acl2/commit/5ecbed745cee652b9eacb7af90842c795ed73a87
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Document a critical type-checking invariant.
Commit: 061354055f9ba590d80c1ffa4b6458fcf5882dd9
https://github.com/acl2/acl2/commit/061354055f9ba590d80c1ffa4b6458fcf5882dd9
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/values.lisp
Log Message:
-----------
[Remora] Align code to doc.
Commit: 28a9bcc5c19d10cc727e0e4461311b3875bf4062
https://github.com/acl2/acl2/commit/28a9bcc5c19d10cc727e0e4461311b3875bf4062
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add type substitution with auto-alpha-rename.
This is an initial version. It has an avoid set (which could be set to nil at
the top level), which is not ideal.
We also add a helper, and a couple of supporting theorems.
Commit: 4ff0cee3410036af4b6deb2e7364654298d5d22d
https://github.com/acl2/acl2/commit/4ff0cee3410036af4b6deb2e7364654298d5d22d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add some important doc.
Commit: deb40a96fa1b1afd31e9c71f9f0decc2513200fc
https://github.com/acl2/acl2/commit/deb40a96fa1b1afd31e9c71f9f0decc2513200fc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/static-environments.lisp
Log Message:
-----------
[Remora] Add some ops on static environments.
Commit: 897f1c1eecedc3c03e61c1929fe686be07d04ecd
https://github.com/acl2/acl2/commit/897f1c1eecedc3c03e61c1929fe686be07d04ecd
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Complete type checking for `let`.
Commit: 74be596754bd911b2a8d7f4a33df893c28bd6b1d
https://github.com/acl2/acl2/commit/74be596754bd911b2a8d7f4a33df893c28bd6b1d
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[C2C] Re-validate after STS transformation
Commit: a50d1472c7434dfe8708dba7e2cced19dfd20c86
https://github.com/acl2/acl2/commit/a50d1472c7434dfe8708dba7e2cced19dfd20c86
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Tweak some doc.
Commit: 08b39c60bfeb481ee7e43e1249dd4f2174fcdf4b
https://github.com/acl2/acl2/commit/08b39c60bfeb481ee7e43e1249dd4f2174fcdf4b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
Log Message:
-----------
[Remora] Add an optional AST type annotation.
This is for unboxing expressions.
Commit: e579b51678d8fdcddb6897c05d8b33ed0114ba68
https://github.com/acl2/acl2/commit/e579b51678d8fdcddb6897c05d8b33ed0114ba68
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[C2C] Report the file path in struct-type-split errors
When a translation unit cannot be transformed, the error now names the
translation unit it came from. Add a filepath field to sts-split-state,
set per translation unit in sts-split-trans-units, and wrap the errors
surfacing from sts-check-completions and trans-unit-sts-split with the
file path via a new sts-error-in-translation-unit helper. Ensemble-level
errors (struct lookup, C17 check, input processing, re-validation) are
left unchanged.
Commit: d283f4ab550c93c51f5e352feaee32459303f003
https://github.com/acl2/acl2/commit/d283f4ab550c93c51f5e352feaee32459303f003
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add wrappers for type auto-alpha substitutions.
The `deffold-map` functions are now auxiliary ones, because of the extra avoid
set input. We provide wrappers that only take the AST and the substitution,
initializing the avoid set to empty.
Commit: d669e35fe2f3adb273bc8b73bc5f2e7579d8cb35
https://github.com/acl2/acl2/commit/d669e35fe2f3adb273bc8b73bc5f2e7579d8cb35
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
Log Message:
-----------
[C$] Fix argument order in nat-to-iconst
The calls to signed-byte-p and unsigned-byte-p passed the numeric value
as the bit width and the byte count as the value, so the representability
checks were backwards: small values such as 1 through 3 were reported as
unrepresentable, and the length suffix did not depend on the value's
magnitude. Compare the value against the implementation environment's
INT_MAX, LONG_MAX, LLONG_MAX, and ULLONG_MAX instead.
Commit: 8825e437ae97ddcbf66238e27c8b207d1c982ef3
https://github.com/acl2/acl2/commit/8825e437ae97ddcbf66238e27c8b207d1c982ef3
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
A books/kestrel/c/syntax/tests/types-to-tynames.lisp
M books/kestrel/c/syntax/top.lisp
A books/kestrel/c/syntax/types-to-tynames.lisp
Log Message:
-----------
[C$] Add type-to-tyname conversion utility
Add types-to-tynames.lisp, which converts a validator type into an
abstract syntax type name (tyname) for pretty-printing. It handles
scalar, pointer, array, function, and tagged and untagged structure and
union types, reconstructing the members for the untagged case, and
returns an error for types with no source-level representation
(enumeration and unknown types). Array sizes are built with
nat-to-iconst, so the conversion takes an implementation environment.
Also add a test book and include the new book in top.lisp.
Commit: e7d7f834c670c363ee46f4807da611ff97c8ead0
https://github.com/acl2/acl2/commit/e7d7f834c670c363ee46f4807da611ff97c8ead0
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/utilities/context-msg.lisp
M books/kestrel/c/transformation/utilities/print-to-str.lisp
Log Message:
-----------
[C2C] Add type printing and context-message utilities
Add print-type-to-str and context-msg-type, which render a validator
type as a type name by converting it with type-to-tyname and printing
the result. Both fall back gracefully (an error flag, or the raw type in
the message) when the type has no source-level representation.
Commit: e97adafdbf17dc6287ad57b22dd6e6b4a7a0a007
https://github.com/acl2/acl2/commit/e97adafdbf17dc6287ad57b22dd6e6b4a7a0a007
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[C2C] Render types as type names in struct-type-split messages
Use context-msg-type to print the offending type as a type name in the
error messages of sts-check-type, instead of dumping the raw type with
~x. Store the implementation environment in sts-split-state so it is
available for the conversion.
Commit: 8d175c3ef63b34149579430cf7db2ef5311b9484
https://github.com/acl2/acl2/commit/8d175c3ef63b34149579430cf7db2ef5311b9484
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Extend evaluation.
Handle unboxing expressions with empty frames.
Commit: fff5dd352ad7372e195defc59ee6d0022c5ed803
https://github.com/acl2/acl2/commit/fff5dd352ad7372e195defc59ee6d0022c5ed803
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add auto-alpha-renaming ispace substitution ops.
Commit: d4fea1c2234ed7518abdaa06cc922bc53991d44c
https://github.com/acl2/acl2/commit/d4fea1c2234ed7518abdaa06cc922bc53991d44c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/arithmetic-light/times.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/leftrotate32.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/sbvlt.lisp
M books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/types-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/crypto/sha-3/sha-3.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/values.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/x86/alt-defs.lisp
M books/projects/abnf/notation/semantics.lisp
A books/projects/abnf/tree-operations/acl2-customization.lsp
A books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/abnf/tree-operations/top.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
Log Message:
-----------
Merge.
Commit: 180972a0e64f9042e09a4e384ebdfb687b16c04c
https://github.com/acl2/acl2/commit/180972a0e64f9042e09a4e384ebdfb687b16c04c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
Merge.
Commit: 5d3fdd60a65c76eb3a6cb2af84bbef003c586d10
https://github.com/acl2/acl2/commit/5d3fdd60a65c76eb3a6cb2af84bbef003c586d10
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
A books/kestrel/c/syntax/tests/types-to-tynames.lisp
M books/kestrel/c/syntax/top.lisp
A books/kestrel/c/syntax/types-to-tynames.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/utilities/context-msg.lisp
M books/kestrel/c/transformation/utilities/print-to-str.lisp
Log Message:
-----------
Merge.
Commit: e6ec4b8a1887fc8671b2c67aa535ddedbdb48ba3
https://github.com/acl2/acl2/commit/e6ec4b8a1887fc8671b2c67aa535ddedbdb48ba3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/bound-and-free-variable-operations.lisp
Log Message:
-----------
[Remora] Add an operation about bound variables.
Commit: 491437fe2af91b421ec7455c933b768ed5c63cb6
https://github.com/acl2/acl2/commit/491437fe2af91b421ec7455c933b768ed5c63cb6
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Add more auto-alpha-rename operations.
These are for substitutions of expression variables.
Commit: cb0c09ae2d2deb753f64c46a3703bc5fa4cbf76d
https://github.com/acl2/acl2/commit/cb0c09ae2d2deb753f64c46a3703bc5fa4cbf76d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Update some doc.
Commit: 9c677a3b87b81c91e40d39bcf95259f771316cf4
https://github.com/acl2/acl2/commit/9c677a3b87b81c91e40d39bcf95259f771316cf4
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
A books/kestrel/c/syntax/tests/types-to-tynames.lisp
M books/kestrel/c/syntax/top.lisp
A books/kestrel/c/syntax/types-to-tynames.lisp
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/utilities/context-msg.lisp
M books/kestrel/c/transformation/utilities/print-to-str.lisp
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/values.lisp
Log Message:
-----------
Merge.
Commit: dbd7fbae7ad6fb8a1388db045dfb1895ac3bb66c
https://github.com/acl2/acl2/commit/dbd7fbae7ad6fb8a1388db045dfb1895ac3bb66c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Improve type checker.
Auto-alpha-rename variables, instead of returning an error when there may be a
variable capture.
Commit: 0a24a658f963909ab518d839520b2567310fc05d
https://github.com/acl2/acl2/commit/0a24a658f963909ab518d839520b2567310fc05d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
A books/kestrel/c/syntax/tests/types-to-tynames.lisp
M books/kestrel/c/syntax/top.lisp
A books/kestrel/c/syntax/types-to-tynames.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/utilities/context-msg.lisp
M books/kestrel/c/transformation/utilities/print-to-str.lisp
Log Message:
-----------
Merge.
Commit: 745d3bdbb7f2d9b1a62f3311c21853f9c237d37a
https://github.com/acl2/acl2/commit/745d3bdbb7f2d9b1a62f3311c21853f9c237d37a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[C$] Improve a function name.
Commit: b4168021284af946e1ab0ea07faaee9215cb0202
https://github.com/acl2/acl2/commit/b4168021284af946e1ab0ea07faaee9215cb0202
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Stop at translation units.
Update and improve some doc.
Commit: afda80b07f8fe1caddffe29067220b8fe779c425
https://github.com/acl2/acl2/commit/afda80b07f8fe1caddffe29067220b8fe779c425
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Expand some doc.
Commit: 51c08081642ef77ce52c413c145e84481a90430e
https://github.com/acl2/acl2/commit/51c08081642ef77ce52c413c145e84481a90430e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Move op to more general place.
Commit: ece1f0a84f57e18401c945b8e0ecc39754f5c00c
https://github.com/acl2/acl2/commit/ece1f0a84f57e18401c945b8e0ecc39754f5c00c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/fty/string-string-map.lisp
Log Message:
-----------
[FTY] Add a theorem.
Commit: 6db009170e13de276d82dda047443df03dc4d61d
https://github.com/acl2/acl2/commit/6db009170e13de276d82dda047443df03dc4d61d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Add some AST ops.
Commit: 93f41349a8ea71d745bcc0b3c1b73ae47c44fac4
https://github.com/acl2/acl2/commit/93f41349a8ea71d745bcc0b3c1b73ae47c44fac4
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Shorten some doc.
Commit: ce3bccf25a911b4d6b328fb6c400dcda59f0541a
https://github.com/acl2/acl2/commit/ce3bccf25a911b4d6b328fb6c400dcda59f0541a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Improve two function names.
Commit: 18df5f29aaa9391325663eccf4104d8a97806e06
https://github.com/acl2/acl2/commit/18df5f29aaa9391325663eccf4104d8a97806e06
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
[Remora] Improve file layout.
Commit: 986f8db1cc08a69770f1439cd60692da0206ede9
https://github.com/acl2/acl2/commit/986f8db1cc08a69770f1439cd60692da0206ede9
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/variable-renaming-alpha-operations.lisp
Log Message:
-----------
[Remora] Add capture-avoiding renaming ops.
Commit: 6ee3a7889b6d8c3d2b993d8bd76d34e54ed35fd7
https://github.com/acl2/acl2/commit/6ee3a7889b6d8c3d2b993d8bd76d34e54ed35fd7
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Improve type checker.
Use capture-avoiding renaming.
Commit: 07a1e9e4cc50afa3eff67ebb0ba905e0f405bc06
https://github.com/acl2/acl2/commit/07a1e9e4cc50afa3eff67ebb0ba905e0f405bc06
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-24 (Wed, 24 Jun 2026)
Changed paths:
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
Log Message:
-----------
[Remora] Update two XDOC links.
Commit: 802f1fa794648e58ebbbed12e9bbf5a9a882aca2
https://github.com/acl2/acl2/commit/802f1fa794648e58ebbbed12e9bbf5a9a882aca2
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
A books/kestrel/c/syntax/tests/types-to-tynames.lisp
M books/kestrel/c/syntax/top.lisp
A books/kestrel/c/syntax/types-to-tynames.lisp
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/utilities/context-msg.lisp
M books/kestrel/c/transformation/utilities/print-to-str.lisp
M books/kestrel/fty/string-string-map.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/values.lisp
A books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
Merge.
Commit: bf9cc3c38c3825fd5e91b8c230aa0c757865da30
https://github.com/acl2/acl2/commit/bf9cc3c38c3825fd5e91b8c230aa0c757865da30
Author: Eric Smith <
ews...@gmail.com>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
A books/kestrel/x86/register-readers-and-writers-8-16.acl2
A books/kestrel/x86/register-readers-and-writers-8-16.lisp
M books/kestrel/x86/register-readers-and-writers32.lisp
M books/kestrel/x86/register-readers-and-writers64.lisp
Log Message:
-----------
[x86] Add 8-bit and 16-bit register readers.
These are regarded as just abbreviations. This change was prompted by some work that NDSU is doing.
Commit: c2eb93766a07e53803dbc24c79791db9632a83dc
https://github.com/acl2/acl2/commit/c2eb93766a07e53803dbc24c79791db9632a83dc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/fty/string-string-map.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-checking.lisp
A books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
Log Message:
-----------
Merge.
Commit: ea7ffc00c77b56071c2cd65c5bccdc71a3fc66cd
https://github.com/acl2/acl2/commit/ea7ffc00c77b56071c2cd65c5bccdc71a3fc66cd
Author: Stephen Westfold <
west...@kestrel.edu>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/quicklisp/base-raw.lsp
M books/quicklisp/dexador-raw.lsp
M books/quicklisp/dexador.lisp
M books/quicklisp/top.lisp
M books/quicklisp/update-libs.lsp
A books/quicklisp/usocket-raw.lsp
A books/quicklisp/usocket.lisp
M books/quicklisp/zippy-raw.lsp
M books/quicklisp/zippy.lisp
Log Message:
-----------
Merge pull request #1953 from acl2/cleanup-quicklisp
Cleanup quicklisp; make usocket available as an individual package
Commit: f0d8441db91871e24166b732a61df6a13f0dbf6b
https://github.com/acl2/acl2/commit/f0d8441db91871e24166b732a61df6a13f0dbf6b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/remora/static-environments.lisp
Log Message:
-----------
[Remora] Remove outdated doc.
Commit: ab44a102ed5d73c710229c348bba6f7f546a3cd9
https://github.com/acl2/acl2/commit/ab44a102ed5d73c710229c348bba6f7f546a3cd9
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/values.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
Log Message:
-----------
[Remora] Make some AST types optional.
These are the types of the parameters of a lambda abstraction, or a `let`
function binding, or a `let` combined function binding. Although the concrete
syntax requires it currently, they may become optional at some point in the
concrete syntax as well, once there is a practical type inference.
Our initial motivation for this relaxation is to be able to desugar `let`s,
which was previously not possible due to the requirements that all parameters
have types. We have not changed desugaring to do that yet though, as this commit
is already a fairly large change.
Commit: af8187f6530d78c4fa783d3671769063afe3aaef
https://github.com/acl2/acl2/commit/af8187f6530d78c4fa783d3671769063afe3aaef
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
A books/kestrel/x86/register-readers-and-writers-8-16.acl2
A books/kestrel/x86/register-readers-and-writers-8-16.lisp
M books/kestrel/x86/register-readers-and-writers32.lisp
M books/kestrel/x86/register-readers-and-writers64.lisp
M books/quicklisp/base-raw.lsp
M books/quicklisp/dexador-raw.lsp
M books/quicklisp/dexador.lisp
M books/quicklisp/top.lisp
M books/quicklisp/update-libs.lsp
A books/quicklisp/usocket-raw.lsp
A books/quicklisp/usocket.lisp
M books/quicklisp/zippy-raw.lsp
M books/quicklisp/zippy.lisp
Log Message:
-----------
Merge.
Commit: 12efa14761d84432814429aa69416f549c74284b
https://github.com/acl2/acl2/commit/12efa14761d84432814429aa69416f549c74284b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/remora/static-environments.lisp
Log Message:
-----------
Merge.
Commit: 2a1f0d4b5dde370e0f7beb4b791c8e18d379b90d
https://github.com/acl2/acl2/commit/2a1f0d4b5dde370e0f7beb4b791c8e18d379b90d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
A books/kestrel/x86/register-readers-and-writers-8-16.acl2
A books/kestrel/x86/register-readers-and-writers-8-16.lisp
M books/kestrel/x86/register-readers-and-writers32.lisp
M books/kestrel/x86/register-readers-and-writers64.lisp
M books/quicklisp/base-raw.lsp
M books/quicklisp/dexador-raw.lsp
M books/quicklisp/dexador.lisp
M books/quicklisp/top.lisp
M books/quicklisp/update-libs.lsp
A books/quicklisp/usocket-raw.lsp
A books/quicklisp/usocket.lisp
M books/quicklisp/zippy-raw.lsp
M books/quicklisp/zippy.lisp
Log Message:
-----------
Merge.
Commit: 7e10528fbf9c96479dd1e08a56394b0f0b337288
https://github.com/acl2/acl2/commit/7e10528fbf9c96479dd1e08a56394b0f0b337288
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Explain a naming choice.
Commit: 51cba6231454743af0ed8a8c18e76903388a4541
https://github.com/acl2/acl2/commit/51cba6231454743af0ed8a8c18e76903388a4541
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/built-ins.lisp
Log Message:
-----------
[C$] Remote outdated doc.
Commit: 9160df1877e5075ea53f5d6684f4f908cd6d9906
https://github.com/acl2/acl2/commit/9160df1877e5075ea53f5d6684f4f908cd6d9906
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Allow array and member expresions.
Commit: 3ed6c6cf5b537c84033c8de4ce7a10650f44f2dc
https://github.com/acl2/acl2/commit/3ed6c6cf5b537c84033c8de4ce7a10650f44f2dc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Allow most unary expressions.
Commit: 17b1705a46611f727890e1c9e64e0b960b40cbbf
https://github.com/acl2/acl2/commit/17b1705a46611f727890e1c9e64e0b960b40cbbf
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/built-ins.lisp
M books/kestrel/c/syntax/disambiguation.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
[C$] Improve XDOC hierarchy.
Commit: e99696375852012c2839e4043500b04d897db1f3
https://github.com/acl2/acl2/commit/e99696375852012c2839e4043500b04d897db1f3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Refactor some code.
Commit: a57fab55a90969bda56c432d376c1d85c1d89dac
https://github.com/acl2/acl2/commit/a57fab55a90969bda56c432d376c1d85c1d89dac
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Document a possible extension.
Commit: d389312872ed6f547f79e01aa5ee96afd9660592
https://github.com/acl2/acl2/commit/d389312872ed6f547f79e01aa5ee96afd9660592
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Allow most `sizeof` and `alignof`.
These are the type name variants, not the unary expressions (done in the
previous commit).
Commit: afaa263ff53a624a296e87d29ae72d54f61f6e76
https://github.com/acl2/acl2/commit/afaa263ff53a624a296e87d29ae72d54f61f6e76
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Refine checks on cast expressions.
Commit: 9ae6aec3ffd3f16ef82cb7bf307cfd3022e6e26a
https://github.com/acl2/acl2/commit/9ae6aec3ffd3f16ef82cb7bf307cfd3022e6e26a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Refactor some code.
Commit: c79f10112c9b804717bd996f43f4ec56d2b160bf
https://github.com/acl2/acl2/commit/c79f10112c9b804717bd996f43f4ec56d2b160bf
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/values.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
Log Message:
-----------
Merge.
Commit: 7df7a67f2c9859fd498a33233fb98dfe800a718e
https://github.com/acl2/acl2/commit/7df7a67f2c9859fd498a33233fb98dfe800a718e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Document a 'todo'.
Commit: cd07b6014c6c11e8bc7c1d67e0ffa24b52fadee0
https://github.com/acl2/acl2/commit/cd07b6014c6c11e8bc7c1d67e0ffa24b52fadee0
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/built-ins.lisp
M books/kestrel/c/syntax/disambiguation.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
Merge.
Commit: ecacc1b2fa2ae21770273a72f6c004b9c3d9b666
https://github.com/acl2/acl2/commit/ecacc1b2fa2ae21770273a72f6c004b9c3d9b666
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Refine checks on binary expressions.
Commit: d2ea2ea25d891e4091c04837d56ed9a1df1a3587
https://github.com/acl2/acl2/commit/d2ea2ea25d891e4091c04837d56ed9a1df1a3587
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-06-25 (Thu, 25 Jun 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Log Message:
-----------
[STS safety] Factor and refine some checks.
Compare:
https://github.com/acl2/acl2/compare/c47f381a7d85...d2ea2ea25d89