[acl2/acl2] de1b1a: [jvm] Organize some code.

0 views
Skip to first unread message

Eric W. Smith

unread,
Apr 11, 2026, 6:19:18 PM (6 days ago) Apr 11
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: de1b1a5f4a886ccd77ddc082e7f34525ef003d16
https://github.com/acl2/acl2/commit/de1b1a5f4a886ccd77ddc082e7f34525ef003d16
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-09 (Thu, 09 Apr 2026)

Changed paths:
A books/kestrel/jvm/bindings.lisp
M books/kestrel/jvm/intern-table.lisp
M books/kestrel/jvm/jvm-facts.lisp
M books/kestrel/jvm/jvm-facts0.lisp
M books/kestrel/jvm/jvm.lisp

Log Message:
-----------
[jvm] Organize some code.


Commit: 337eba6a654e0589adc1b6516407a5b0752390ac
https://github.com/acl2/acl2/commit/337eba6a654e0589adc1b6516407a5b0752390ac
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-09 (Thu, 09 Apr 2026)

Changed paths:
M books/kestrel/jvm/execution-common.lisp
M books/kestrel/jvm/frames.lisp
M books/kestrel/jvm/intern-table.lisp
M books/kestrel/jvm/jvm.lisp
M books/kestrel/jvm/pc-designators.lisp
A books/kestrel/jvm/th.lisp
M books/kestrel/jvm/top.lisp

Log Message:
-----------
[jvm] Continue refactoring.

Also improve a rule or 2.


Commit: 2488685ee2ba199d558cba14409b495b5bcb07c7
https://github.com/acl2/acl2/commit/2488685ee2ba199d558cba14409b495b5bcb07c7
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-09 (Thu, 09 Apr 2026)

Changed paths:
M books/kestrel/jvm/jvm.lisp
M books/kestrel/jvm/methods.lisp

Log Message:
-----------
[jvm] Continue organizing.


Commit: f89a85ac4bafe1e3aafb5307050a9d5016014e97
https://github.com/acl2/acl2/commit/f89a85ac4bafe1e3aafb5307050a9d5016014e97
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-09 (Thu, 09 Apr 2026)

Changed paths:
M books/kestrel/axe/jvm/axe-syntax-functions-jvm.lisp

Log Message:
-----------
[axe/jvm] Reduce includes and speed up proofs.


Commit: c3dc777354d1545a716df423da5bbc346a98f0d3
https://github.com/acl2/acl2/commit/c3dc777354d1545a716df423da5bbc346a98f0d3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-09 (Thu, 09 Apr 2026)

Changed paths:
M books/kestrel/jvm/jvm.lisp

Log Message:
-----------
[jvm] Strengthen jvm-statep.


Commit: d6ca011f4a1e5b2b44734a40c91e2903f10f2b1b
https://github.com/acl2/acl2/commit/d6ca011f4a1e5b2b44734a40c91e2903f10f2b1b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-09 (Thu, 09 Apr 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/external-preprocessing.lisp
M books/kestrel/c/syntax/files.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/output-files.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp

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


Commit: 936ea1a846a1cc72fb9f8f6e3e09ae6ae594b38c
https://github.com/acl2/acl2/commit/936ea1a846a1cc72fb9f8f6e3e09ae6ae594b38c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-09 (Thu, 09 Apr 2026)

Changed paths:
M books/kestrel/jvm/execution-common.lisp
M books/kestrel/jvm/execution.lisp
M books/kestrel/jvm/execution2.lisp
M books/kestrel/jvm/instructions.lisp
M books/kestrel/jvm/jvm.lisp
M books/kestrel/jvm/pc-designators.lisp
A books/kestrel/jvm/states.lisp
M books/kestrel/jvm/symbolic-execution.lisp
M books/kestrel/jvm/symbolic-execution2.lisp
M books/kestrel/jvm/top.lisp

Log Message:
-----------
[jvm] Factor material into new book states.lisp.


Commit: d60a0c1da05fbb593efab2bf87a93a6a8415d1a2
https://github.com/acl2/acl2/commit/d60a0c1da05fbb593efab2bf87a93a6a8415d1a2
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-10 (Fri, 10 Apr 2026)

Changed paths:
M books/kestrel/arrays-2d/arrays-2d.lisp
M books/kestrel/axe/equivalence-checker.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

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


Commit: d9a40c248802a8fc5d3100a48d749f2cbb35b2e7
https://github.com/acl2/acl2/commit/d9a40c248802a8fc5d3100a48d749f2cbb35b2e7
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-10 (Fri, 10 Apr 2026)

Changed paths:
M books/kestrel/typed-lists-light/map-code-char.lisp

Log Message:
-----------
[typed-lists-light] Add 2 rules about map-code-char.


Commit: 5ae54bf755b2dec8f8b3cd6bb6654d73031831e1
https://github.com/acl2/acl2/commit/5ae54bf755b2dec8f8b3cd6bb6654d73031831e1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-10 (Fri, 10 Apr 2026)

Changed paths:
M books/kestrel/jvm/intern-table.lisp

Log Message:
-----------
[jvm] Improve a rule.


Commit: b24ec5c402c0bd3bb8e74f81a704ec1893fb3e24
https://github.com/acl2/acl2/commit/b24ec5c402c0bd3bb8e74f81a704ec1893fb3e24
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-10 (Fri, 10 Apr 2026)

Changed paths:
M books/kestrel/jvm/strings.lisp

Log Message:
-----------
[jvm] Improve function and rename to java-char-listp.


Commit: 578f94b615e6c39c75e6f77f54da832a80a43d2b
https://github.com/acl2/acl2/commit/578f94b615e6c39c75e6f77f54da832a80a43d2b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/executable-parsers/parse-mach-o-file.lisp
M books/kestrel/executable-parsers/parse-pe-file.lisp

Log Message:
-----------
[executable-parsers] Adjust includes.


Commit: 3111c14c6d53cc5775f7ebd274a45fb0c66c6bf0
https://github.com/acl2/acl2/commit/3111c14c6d53cc5775f7ebd274a45fb0c66c6bf0
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/unicode-light/code-point-to-utf-8-chars.lisp

Log Message:
-----------
[unicode-light] Adjust includes.


Commit: de9c0700166eddba4738c84997586ceb570a7554
https://github.com/acl2/acl2/commit/de9c0700166eddba4738c84997586ceb570a7554
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

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

Log Message:
-----------
[jvm] Add symbol to package.


Commit: 75a480526c169c61e0ecf1cf8da5b99a8d830071
https://github.com/acl2/acl2/commit/75a480526c169c61e0ecf1cf8da5b99a8d830071
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/jvm/java-types.lisp

Log Message:
-----------
[jvm] Add rule.


Commit: 2cb7f31c20ceb591c8e3e8677f85fb8a52d6bd36
https://github.com/acl2/acl2/commit/2cb7f31c20ceb591c8e3e8677f85fb8a52d6bd36
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/jvm/strings.lisp

Log Message:
-----------
[jvm] Add rules.

Also disable a function and reduce exports.


Commit: 30d0aec65f0f1f5f528e80855f26fc1f1c882885
https://github.com/acl2/acl2/commit/30d0aec65f0f1f5f528e80855f26fc1f1c882885
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/jvm/jvm.lisp

Log Message:
-----------
[jvm] Adjust includes.


Commit: 1c3fc6880558586eee1b55a99b4c27beb19423ce
https://github.com/acl2/acl2/commit/1c3fc6880558586eee1b55a99b4c27beb19423ce
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
A books/kestrel/jvm/string-encoding.lisp
M books/kestrel/jvm/top.lisp

Log Message:
-----------
[jvm] Add intial version of encoding of char lists as readable strings.


Commit: 825cd56fc625f5c91f687223fbeb977a513e68e3
https://github.com/acl2/acl2/commit/825cd56fc625f5c91f687223fbeb977a513e68e3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/jvm/jvm.lisp

Log Message:
-----------
[jvm] Actually adjust includes.


Commit: fe7b920b290a011ddeea71655dd107b27c6f439c
https://github.com/acl2/acl2/commit/fe7b920b290a011ddeea71655dd107b27c6f439c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/jvm/class-file-parser.lisp

Log Message:
-----------
[jvm] Improve class file parser.

Check the bytes in CONSTANT_Utf8 entries and strengthen constant-pool-entryp.


Commit: 5f7f69320dcff29b95b51ce6de18955a02f36b26
https://github.com/acl2/acl2/commit/5f7f69320dcff29b95b51ce6de18955a02f36b26
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/jvm/class-file-parser.lisp

Log Message:
-----------
[jvm] Improve handling of the constant pool.

Also make various rules local.


Commit: 15e0b996658fe02819469ea563538d65d9207e3e
https://github.com/acl2/acl2/commit/15e0b996658fe02819469ea563538d65d9207e3e
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/read-and-parse-class-file.lisp
M books/kestrel/jvm/read-jar.lisp

Log Message:
-----------
[jvm] Continue improving class file parser.


Commit: d8e3025332653b0433f3927605df1a8993e6edb3
https://github.com/acl2/acl2/commit/d8e3025332653b0433f3927605df1a8993e6edb3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/axe/jvm/tester.lisp
M books/kestrel/jvm/class-file-parser.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

Log Message:
-----------
[jvm] Improve class file parser.

Use with-local-stobj for the constant-pool.


Commit: af19ffd6396af3710fae9fbf5bbfdc6ab784ef10
https://github.com/acl2/acl2/commit/af19ffd6396af3710fae9fbf5bbfdc6ab784ef10
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/doc/relnotes.lisp
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/let-designations.lisp
M books/kestrel/c/language/character-sets.lisp
M books/kestrel/c/language/pointer-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/grammar-operations.lisp
M books/kestrel/c/syntax/grammar.lisp
A books/kestrel/c/syntax/hash-conditional-evaluation.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/preservable-inclusions.lisp
M books/kestrel/c/syntax/tests/disambiguator-trans-units.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/token-concatenation.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp
M books/projects/abnf/grammar-definer/deftreeops.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/ed614520a769...af19ffd6396a

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

acl2buildserver

unread,
Apr 11, 2026, 9:34:51 PM (6 days ago) Apr 11
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: d8483fd63f36f985791559c64ce71edf93c486ae
https://github.com/acl2/acl2/commit/d8483fd63f36f985791559c64ce71edf93c486ae
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-04-11 (Sat, 11 Apr 2026)

Changed paths:
M books/kestrel/axe/jvm/axe-syntax-functions-jvm.lisp
M books/kestrel/axe/jvm/tester.lisp
M books/kestrel/executable-parsers/parse-mach-o-file.lisp
M books/kestrel/executable-parsers/parse-pe-file.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

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


Compare: https://github.com/acl2/acl2/compare/f5c3486b7c63...d8483fd63f36

acl2buildserver

unread,
Apr 11, 2026, 9:35:35 PM (6 days ago) Apr 11
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Apr 12, 2026, 11:37:10 PM (4 days ago) Apr 12
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
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
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/f5c3486b7c63...7bb80013b8d3
Reply all
Reply to author
Forward
0 new messages