[acl2/acl2] 15843b: [C] Improve some doc.

0 views
Skip to first unread message

acl2buildserver

unread,
Jul 9, 2026, 7:23:03 AM (2 days ago) Jul 9
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 15843b4eadd9c97d74a74566984c81f4fb8c33c6
https://github.com/acl2/acl2/commit/15843b4eadd9c97d74a74566984c81f4fb8c33c6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/kestrel/c/language/abstract-syntax.lisp
M books/kestrel/c/language/static-semantics.lisp

Log Message:
-----------
[C] Improve some doc.


Commit: 6b188f8f48ed22987c511c01f7aabf46de85160e
https://github.com/acl2/acl2/commit/6b188f8f48ed22987c511c01f7aabf46de85160e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/kestrel/c/atc/doc.lisp

Log Message:
-----------
[ATC] Improve some terminology.


Commit: 89102b37a5e61de5784033965391a209092e9f46
https://github.com/acl2/acl2/commit/89102b37a5e61de5784033965391a209092e9f46
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/kestrel/c/atc/generation.lisp

Log Message:
-----------
[ATC] Improve some terminology.


Commit: 5869eeaa0e73c45ee0b1cfeb53199a7ae5e21e43
https://github.com/acl2/acl2/commit/5869eeaa0e73c45ee0b1cfeb53199a7ae5e21e43
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/files.lisp
M books/kestrel/c/syntax/top.lisp

Log Message:
-----------
[C$] Improve some terminology.


Commit: b337dfd23eb5771a7e110cc81f47c2bc5c0f0eb1
https://github.com/acl2/acl2/commit/b337dfd23eb5771a7e110cc81f47c2bc5c0f0eb1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/types-to-tynames.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
[C$] Extend validation annotations.

Annotate `:none` parameter declarators with their type, with `void` as a special
case as described in the documentation.


Commit: 5b39557d63587788c48cd51c11457b21dfe04d49
https://github.com/acl2/acl2/commit/5b39557d63587788c48cd51c11457b21dfe04d49
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/demos/claude/qsort-examples.lisp

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


Commit: 61e855d7463bcee68cce182723c78b918f5812ca
https://github.com/acl2/acl2/commit/61e855d7463bcee68cce182723c78b918f5812ca
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 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: a3ca276121bda9c65109698aed88cad63d369672
https://github.com/acl2/acl2/commit/a3ca276121bda9c65109698aed88cad63d369672
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/kestrel/c/atc/doc.lisp
M books/kestrel/c/atc/generation.lisp
M books/kestrel/c/language/abstract-syntax.lisp
M books/kestrel/c/language/static-semantics.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/files.lisp
M books/kestrel/c/syntax/top.lisp

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


Commit: 5b8aae0caefc7d4d1fb29643f93a8d8d7fd4bbca
https://github.com/acl2/acl2/commit/5b8aae0caefc7d4d1fb29643f93a8d8d7fd4bbca
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/c/atc/doc.lisp
M books/kestrel/c/atc/generation.lisp
M books/kestrel/c/language/abstract-syntax.lisp
M books/kestrel/c/language/static-semantics.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/files.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/types-to-tynames.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
Merge commit 'a3ca276121bda9c65109698aed88cad63d369672' into HEAD


Compare: https://github.com/acl2/acl2/compare/47f6e27db015...5b8aae0caefc

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

acl2buildserver

unread,
Jul 9, 2026, 7:23:37 AM (2 days ago) Jul 9
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Jul 9, 2026, 6:41:10 PM (2 days ago) Jul 9
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Commit: 1ef9743590ebe8d6641e2444050b5a335de5466e
https://github.com/acl2/acl2/commit/1ef9743590ebe8d6641e2444050b5a335de5466e
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-07-08 (Wed, 08 Jul 2026)

Changed paths:
M books/demos/claude/qsort-examples.lisp

Log Message:
-----------
Tweaked a comment
Commit: 232a2c306517b8e9c1bcb5a6accb31a72b99d59d
https://github.com/acl2/acl2/commit/232a2c306517b8e9c1bcb5a6accb31a72b99d59d
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-09 (Thu, 09 Jul 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 'dff7233c1f7ae6e35ed06346191a787563cce2a7' into HEAD


Commit: 47f6e27db0158c05efa4a0c1231f4bf53a9a98bc
https://github.com/acl2/acl2/commit/47f6e27db0158c05efa4a0c1231f4bf53a9a98bc
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/acl2-arrays/bounded-nat-alists.lisp

Log Message:
-----------
Merge commit '744ccdd468d7756b8afe3c030eb8ebe7328bf83b' into HEAD
Commit: b57c36bc9f722f2a5730e9a65861c96506e9a67f
https://github.com/acl2/acl2/commit/b57c36bc9f722f2a5730e9a65861c96506e9a67f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/library-extensions.lisp
A books/kestrel/remora/unit-types.lisp

Log Message:
-----------
[Remora] Add two library types.


Commit: 1ad996abb8f5dfd79596179c294a0a90c34160ef
https://github.com/acl2/acl2/commit/1ad996abb8f5dfd79596179c294a0a90c34160ef
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp

Log Message:
-----------
[Remora] Add slots for closures.

These are not properly populated yet, but we have made expression values and
expression dynamic environments mutually recursive, we have extended the
dimension checking and well-formedness functions accordingly, etc. Evaluation is
currently storing empty environments, but we will populate them propertly next.


Commit: 0afd85b9f84dc2c6d6d50ce85c8830dabfcafc9c
https://github.com/acl2/acl2/commit/0afd85b9f84dc2c6d6d50ce85c8830dabfcafc9c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/expression-values-and-environments.lisp

Log Message:
-----------
[Remora] Fix doc.


Commit: f551f6c30c7c637dfb8c50a39b68dfeba5f40cac
https://github.com/acl2/acl2/commit/f551f6c30c7c637dfb8c50a39b68dfeba5f40cac
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/expression-values-and-environments.lisp

Log Message:
-----------
[Remora] Add op to restrict expression environments.


Commit: e31a5fb5d8091e7f513bd724cdb5ddc9b074293e
https://github.com/acl2/acl2/commit/e31a5fb5d8091e7f513bd724cdb5ddc9b074293e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Properly construct closures in evaluation.


Commit: 8b18ec5f0b3b092302621d6ffcd2a67e769334c9
https://github.com/acl2/acl2/commit/8b18ec5f0b3b092302621d6ffcd2a67e769334c9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Stylistic change.


Commit: b5a23e7ec0af6c70f04d77cebb5f6e34e9e16ba5
https://github.com/acl2/acl2/commit/b5a23e7ec0af6c70f04d77cebb5f6e34e9e16ba5
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/primitive-operation-values.lisp
R books/kestrel/remora/primitives-evaluation-length-tests.lisp
A books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp

Log Message:
-----------
Merge commit '6dfeda83128904e14dd2ee48e3b09da451706707' into HEAD


Commit: 895c1f51a504cccd090b9d86314d24b8f0e0905f
https://github.com/acl2/acl2/commit/895c1f51a504cccd090b9d86314d24b8f0e0905f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/expression-values-and-environments.lisp

Log Message:
-----------
[Remora] Add some theorems.


Commit: cb7165a3144abc9fd92daa30733b07720744dc87
https://github.com/acl2/acl2/commit/cb7165a3144abc9fd92daa30733b07720744dc87
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Have evaluation use closures.


Commit: baffef6555132e8e8f598fa7172fa0ce2a06214a
https://github.com/acl2/acl2/commit/baffef6555132e8e8f598fa7172fa0ce2a06214a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation-tests.lisp

Log Message:
-----------
[Remora] Add test demonstrating closures.


Commit: f7beb434558f330f16109435b91fe3c777129288
https://github.com/acl2/acl2/commit/f7beb434558f330f16109435b91fe3c777129288
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/primitive-operation-values.lisp
R books/kestrel/remora/primitives-evaluation-length-tests.lisp
A books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp

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


Commit: 5a76f81756d51e68193404f06af98c84464e3797
https://github.com/acl2/acl2/commit/5a76f81756d51e68193404f06af98c84464e3797
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation-rules.lisp
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Drop now-unneeded argument.


Commit: 9902dee9da609f9bc08e9dba13490263ae37bc7f
https://github.com/acl2/acl2/commit/9902dee9da609f9bc08e9dba13490263ae37bc7f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp

Log Message:
-----------
[Remora] Add Quan as co-author of file.


Commit: 3cbf7a13474518a808b2591b388a04138b1a02fe
https://github.com/acl2/acl2/commit/3cbf7a13474518a808b2591b388a04138b1a02fe
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp

Log Message:
-----------
[Remora] De-emphasize `:flag-local`.

No need to put it upfront.

And the comments just stated what is known about that directive.


Commit: b487dcb5ec6f9b0a2f74a45b8fae0a8b21e6ae31
https://github.com/acl2/acl2/commit/b487dcb5ec6f9b0a2f74a45b8fae0a8b21e6ae31
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:

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


Commit: 00b4e8ab35a34301ba63fc782e8b7308d119641c
https://github.com/acl2/acl2/commit/00b4e8ab35a34301ba63fc782e8b7308d119641c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-09 (Thu, 09 Jul 2026)

Changed paths:
M books/kestrel/remora/expression-values-and-environments.lisp

Log Message:
-----------
[Remora] Fix XDOC parent.


Compare: https://github.com/acl2/acl2/compare/6dfeda831289...00b4e8ab35a3
Reply all
Reply to author
Forward
0 new messages