[acl2/acl2] 190f99: [Remora] Improve model of box values.
0 views
Skip to first unread message
Alessandro Coglio
Jun 20, 2026, 7:08:55 PM (3 days ago) Jun 20
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
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: 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: 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: 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: 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.
Compare: https://github.com/acl2/acl2/compare/c84843866f6c...cc591f7be808
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
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: 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: 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: 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: 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.
Compare: https://github.com/acl2/acl2/compare/c84843866f6c...cc591f7be808
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Jun 20, 2026, 8:24:57 PM (3 days ago) Jun 20
to acl2-...@googlegroups.com
Alessandro Coglio
Jun 20, 2026, 8:25:38 PM (3 days ago) Jun 20
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages