[acl2/acl2] b57c36: [Remora] Add two library types.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
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: 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/b5a23e7ec0af...00b4e8ab35a3

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

[Alessandro Coglio]

Branch: refs/heads/testing