[acl2/acl2] e6ea9d: [Remora] More precise references in doc.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: e6ea9d433ecf9f7afe7cd9ebf25aa2a0db6138ee
https://github.com/acl2/acl2/commit/e6ea9d433ecf9f7afe7cd9ebf25aa2a0db6138ee
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-10 (Fri, 10 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax.lisp
M books/kestrel/remora/top.lisp

Log Message:
-----------
[Remora] More precise references in doc.


Commit: 5530ee5c3f485651c0b23b45f9e5eca1e6e24606
https://github.com/acl2/acl2/commit/5530ee5c3f485651c0b23b45f9e5eca1e6e24606
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-10 (Fri, 10 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
[Remora] Expand some doc.


Commit: 6a5228bbf201cafac1bdbd3fd1a4f89af7db5ad6
https://github.com/acl2/acl2/commit/6a5228bbf201cafac1bdbd3fd1a4f89af7db5ad6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-10 (Fri, 10 Apr 2026)

Changed paths:
M books/kestrel/fty/defresult.lisp

Log Message:
-----------
[FTY] Fix bug in `ok` binder.

This was erroneously doing something that only the `okf` binder should do.


Commit: 868537867c3e6d2d7a9569aeeda9593142232402
https://github.com/acl2/acl2/commit/868537867c3e6d2d7a9569aeeda9593142232402
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-10 (Fri, 10 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
[Remora] More uniform fixtype field name.


Commit: 8b1049bca191c9362ba66af14dda8dcf73561d97
https://github.com/acl2/acl2/commit/8b1049bca191c9362ba66af14dda8dcf73561d97
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
[Remora] Generate additional theorems.


Commit: cb8142e23cf84aaff6c49ae5d00629c95414cb11
https://github.com/acl2/acl2/commit/cb8142e23cf84aaff6c49ae5d00629c95414cb11
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Import more symbols into the package.


Commit: 3e5d0a17bd46b7019c5ebdfbed30b97d5bf57361
https://github.com/acl2/acl2/commit/3e5d0a17bd46b7019c5ebdfbed30b97d5bf57361
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
A books/kestrel/remora/abstract-syntax-trees.lisp
R books/kestrel/remora/abstract-syntax.lisp
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Import symbols into package.


Commit: a7aa1125c1b683603232e6a8271a6b497f81ca13
https://github.com/acl2/acl2/commit/a7aa1125c1b683603232e6a8271a6b497f81ca13
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
A books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
[Remora] Articulate structure for abstract syntax.

Introduce a separate topic/file for ASTs, with abstract syntax as an
over-arching topic/file. This in preparation for extensions.


Commit: a1efa4a6e3829ec9c63f5358a03d9a79d57bb950
https://github.com/acl2/acl2/commit/a1efa4a6e3829ec9c63f5358a03d9a79d57bb950
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp

Log Message:
-----------
[Remora] Add some simple derived fixtypes.


Commit: 9d092de07a6221634aacb7b5aa21d2c00ffd34a6
https://github.com/acl2/acl2/commit/9d092de07a6221634aacb7b5aa21d2c00ffd34a6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
A books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
[Remora] Add some less simple derived fixtypes.


Commit: 067ce4ac3e7bd87a7bfbd57b17b0b455192723f1
https://github.com/acl2/acl2/commit/067ce4ac3e7bd87a7bfbd57b17b0b455192723f1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
A books/kestrel/remora/abstract-syntax-structural-operations.lisp
M books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
[Remora] Add some structural AST ops.


Commit: 08b26812c6b69ece127f658c75997a1a35e16c18
https://github.com/acl2/acl2/commit/08b26812c6b69ece127f658c75997a1a35e16c18
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Import a symbol into the package.


Commit: 3362b3586bd9e07427070024457df71016c2f9e4
https://github.com/acl2/acl2/commit/3362b3586bd9e07427070024457df71016c2f9e4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
A books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
[Remora] Add some readable AST constructors.


Commit: 044eccee38392fe2bd2a4be9a706aa6c7b375305
https://github.com/acl2/acl2/commit/044eccee38392fe2bd2a4be9a706aa6c7b375305
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp

Log Message:
-----------
[Remora] Take theorem from library.


Commit: af95b1e63e89871c84044c383be94b65d789c468
https://github.com/acl2/acl2/commit/af95b1e63e89871c84044c383be94b65d789c468
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/fty/defresult.lisp

Log Message:
-----------
[FTY] Add a theorem.


Commit: 30891930d4dee2a4ee9a582b65cc6f2e77bc65fb
https://github.com/acl2/acl2/commit/30891930d4dee2a4ee9a582b65cc6f2e77bc65fb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
A books/kestrel/remora/static-semantics.lisp
M books/kestrel/remora/top.lisp

Log Message:
-----------
[Remora] Start a file and topic for static semantics.


Commit: 82dc7c98d7879d5a4e30d48ed0d84d07bb374ced
https://github.com/acl2/acl2/commit/82dc7c98d7879d5a4e30d48ed0d84d07bb374ced
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
A books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
[Remora] Start operations to match ASTs.


Commit: 25ce19987e7efb71ead65129ff41b1b36213ae0b
https://github.com/acl2/acl2/commit/25ce19987e7efb71ead65129ff41b1b36213ae0b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
[Remora] Reorder two files and topics.


Commit: c9e6760094dd36028e8eff6a55732e0859604ee7
https://github.com/acl2/acl2/commit/c9e6760094dd36028e8eff6a55732e0859604ee7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/static-semantics.lisp
A books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Initial, partial version of type checking.


Commit: 7f24c3c0796c4e081557c1097dacb197d3ade3cc
https://github.com/acl2/acl2/commit/7f24c3c0796c4e081557c1097dacb197d3ade3cc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Expand some doc.


Commit: 01a3b51e95b806e5c369591877062123ea098739
https://github.com/acl2/acl2/commit/01a3b51e95b806e5c369591877062123ea098739
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
A books/kestrel/remora/index-equivalence.lisp
M books/kestrel/remora/static-semantics.lisp

Log Message:
-----------
[Remora] Add initial code for index equivalence.


Commit: b8d4457358101fee9b022b14be54c8b1ab101503
https://github.com/acl2/acl2/commit/b8d4457358101fee9b022b14be54c8b1ab101503
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/index-equivalence.lisp

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


Commit: af6409db9adfa7e241b0f3d0db2f779098116328
https://github.com/acl2/acl2/commit/af6409db9adfa7e241b0f3d0db2f779098116328
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/static-semantics.lisp
M books/kestrel/remora/type-checking.lisp
A books/kestrel/remora/type-equivalence.lisp

Log Message:
-----------
[Remora] Move (placeholder) type equivalence to new file and topic.


Commit: 656132f2b83b3620ec2cf074fea12cbd0daa5ea9
https://github.com/acl2/acl2/commit/656132f2b83b3620ec2cf074fea12cbd0daa5ea9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp

Log Message:
-----------
[Remora] Remove two AST categories.

Terms and functions are not used anywhere else in the ASTs, and their purpose is
not entirely clear at this time. Terms are defined as atoms or term
abstractions, but term abstractions are already part of atoms. And functions are
defined as primitive operations or expressions, which excludes lambda
abstrations, which seems strange. We will revisit these.


Commit: cdf980d79d291f725caf71a26dbfd0b616f2807e
https://github.com/acl2/acl2/commit/cdf980d79d291f725caf71a26dbfd0b616f2807e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/index-equivalence.lisp
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Update some XDOC parents.


Commit: 7013939a5b3b912510299748ee0f583b3ab6ff19
https://github.com/acl2/acl2/commit/7013939a5b3b912510299748ee0f583b3ab6ff19
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/type-equivalence.lisp

Log Message:
-----------
[Remora] Refine type equivalence.

Now it relaxes index identity to index equivalence, so it is slightly less of a
placeholder. We still need to flesh out the rest of type equivalence.


Commit: 92c3f76ce7bf16742aeae32ea041d84866328b7c
https://github.com/acl2/acl2/commit/92c3f76ce7bf16742aeae32ea041d84866328b7c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp

Log Message:
-----------
[Remora] Add some error checking.


Commit: 0eb633e15a4bc593ff62690ce13dc1d4ce10466a
https://github.com/acl2/acl2/commit/0eb633e15a4bc593ff62690ce13dc1d4ce10466a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-structural-operations.lisp

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


Commit: a78b4dc528696cf1259fb5800bdbe25127a9cb8b
https://github.com/acl2/acl2/commit/a78b4dc528696cf1259fb5800bdbe25127a9cb8b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
[Remora] Extend some doc.


Commit: 39e7e86473806c095a7633964a24af178432bef7
https://github.com/acl2/acl2/commit/39e7e86473806c095a7633964a24af178432bef7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/index-equivalence.lisp

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


Commit: 62e1862f88d79f94c39feeffedd99a881797567c
https://github.com/acl2/acl2/commit/62e1862f88d79f94c39feeffedd99a881797567c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/index-equivalence.lisp

Log Message:
-----------
[Remora] Add missing `:returns`.


Commit: 248a325a1c72ff3d0bc650c24140adb3f485c189
https://github.com/acl2/acl2/commit/248a325a1c72ff3d0bc650c24140adb3f485c189
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/index-equivalence.lisp

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


Commit: 4074d59f97fdf34f243d847608528f893d13eca7
https://github.com/acl2/acl2/commit/4074d59f97fdf34f243d847608528f893d13eca7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/type-equivalence.lisp

Log Message:
-----------
[Remora] Add missing closing parenthesis.


Commit: dcc2a7320dbee41de8038e60467b632ba34292b4
https://github.com/acl2/acl2/commit/dcc2a7320dbee41de8038e60467b632ba34292b4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Fix an index check.


Commit: c090154970ad3b7b84ec3894d0c69027db7a97cb
https://github.com/acl2/acl2/commit/c090154970ad3b7b84ec3894d0c69027db7a97cb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

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


Commit: ba099746211754839eddc79d9650e8b31d9279cb
https://github.com/acl2/acl2/commit/ba099746211754839eddc79d9650e8b31d9279cb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Add missing spaces.


Commit: 6a33d1a7cac5ea37febf2cfdf703d0fcf72644ea
https://github.com/acl2/acl2/commit/6a33d1a7cac5ea37febf2cfdf703d0fcf72644ea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Remove unneeded binding.


Commit: 7bb80013b8d3134f34571df92c518a12c0b2f19e
https://github.com/acl2/acl2/commit/7bb80013b8d3134f34571df92c518a12c0b2f19e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-12 (Sun, 12 Apr 2026)

Changed paths:
M books/doc/relnotes.lisp
M books/kestrel/arrays-2d/arrays-2d.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/jvm/axe-syntax-functions-jvm.lisp
M books/kestrel/axe/jvm/tester.lisp
M books/kestrel/axe/prove-equal-with-axe-tests.lisp
M books/kestrel/axe/unroll-spec.lisp
M books/kestrel/axe/x86/tester-code-only.lisp
M books/kestrel/crypto/kdf/doc.lisp
M books/kestrel/executable-parsers/parse-mach-o-file.lisp
M books/kestrel/executable-parsers/parse-pe-file.lisp
M books/kestrel/fty/database.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/dependencies.lisp
M books/kestrel/fty/nat-natlist-result.lisp
A books/kestrel/jvm/bindings.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/execution-common.lisp
M books/kestrel/jvm/execution.lisp
M books/kestrel/jvm/execution2.lisp
M books/kestrel/jvm/frames.lisp
M books/kestrel/jvm/instructions.lisp
M books/kestrel/jvm/intern-table.lisp
M books/kestrel/jvm/java-types.lisp
M books/kestrel/jvm/jvm-facts.lisp
M books/kestrel/jvm/jvm-facts0.lisp
M books/kestrel/jvm/jvm.lisp
M books/kestrel/jvm/methods.lisp
M books/kestrel/jvm/package.lsp
M books/kestrel/jvm/pc-designators.lisp
M books/kestrel/jvm/read-and-parse-class-file.lisp
M books/kestrel/jvm/read-class-from-hierarchy.lisp
M books/kestrel/jvm/read-class.lisp
M books/kestrel/jvm/read-jar.lisp
A books/kestrel/jvm/states.lisp
A books/kestrel/jvm/string-encoding.lisp
M books/kestrel/jvm/strings.lisp
M books/kestrel/jvm/symbolic-execution.lisp
M books/kestrel/jvm/symbolic-execution2.lisp
A books/kestrel/jvm/th.lisp
M books/kestrel/jvm/top.lisp
M books/kestrel/typed-lists-light/map-code-char.lisp
M books/kestrel/unicode-light/code-point-to-utf-8-chars.lisp
M books/projects/x86isa/doc.lisp
M books/projects/x86isa/machine/catalogue-doc.lisp
M books/projects/x86isa/machine/inst-doc.lisp

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


Compare: https://github.com/acl2/acl2/compare/d8483fd63f36...7bb80013b8d3

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

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel