[acl2/acl2] 9a8fab: [Remora] Define core subset.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 9a8fab0f80dbc90992b083ba1cd5af4732c38d5d
https://github.com/acl2/acl2/commit/9a8fab0f80dbc90992b083ba1cd5af4732c38d5d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-30 (Thu, 30 Apr 2026)

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

Log Message:
-----------
[Remora] Define core subset.


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

Changed paths:
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Improve some AST names.

Switch from base values to base literals.


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

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

Log Message:
-----------
[Remora] Slightly simplify core subset definition.


Commit: 563fab6bb7e481b5b21f7fa3f9d28ef097274324
https://github.com/acl2/acl2/commit/563fab6bb7e481b5b21f7fa3f9d28ef097274324
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp

Log Message:
-----------
[C$] Stylistic tweak.


Commit: 112d762093dbad86ee8f96241a686b9cdcbaeead
https://github.com/acl2/acl2/commit/112d762093dbad86ee8f96241a686b9cdcbaeead
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Improve structure of validator.

Introduce and use an explicit validator state.


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

Changed paths:
M books/kestrel/arithmetic-light/limit-expt.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/defthm-axe-basic-tests.lisp
M books/kestrel/axe/defthm-axe.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/prover-basic-tests.lisp
M books/kestrel/axe/prover-tests.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv/bvplus.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/syntax-abstraction.lisp

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


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

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

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


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

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

Log Message:
-----------
[Remora] Add some theorems about the core predicates.


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

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

Log Message:
-----------
[Remora] Start defining desugaring.


Commit: 17a98ac10e54a5f41a9fd484b21463d0d354d59d
https://github.com/acl2/acl2/commit/17a98ac10e54a5f41a9fd484b21463d0d354d59d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-30 (Thu, 30 Apr 2026)

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

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


Commit: 29dbe8bce76234fb5c602c22f7a18efc00ba042e
https://github.com/acl2/acl2/commit/29dbe8bce76234fb5c602c22f7a18efc00ba042e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/validator.lisp

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


Commit: 88dbbddd06569d2bbfd35f81423064a4f6c2a980
https://github.com/acl2/acl2/commit/88dbbddd06569d2bbfd35f81423064a4f6c2a980
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-30 (Thu, 30 Apr 2026)

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

Log Message:
-----------
[Remora] Make an AST fixtype consistent with the grammar.


Commit: 2e1550dcbb4598f226d782d0658ffea4ffb3cd47
https://github.com/acl2/acl2/commit/2e1550dcbb4598f226d782d0658ffea4ffb3cd47
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/character-literal-codes.lisp

Log Message:
-----------
[Remora] Define mapping from char literals to codes.


Commit: 32a10fa7117ab82a232d1b4dd733094772c7d940
https://github.com/acl2/acl2/commit/32a10fa7117ab82a232d1b4dd733094772c7d940
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/parser.lisp

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


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

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

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


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

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

Log Message:
-----------
[Remora] Rename a file and topic.


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

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

Log Message:
-----------
[Remora] Shorten definition of desugaring.


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

Changed paths:
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Fix XDOC.


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

Changed paths:
M books/kestrel/remora/character-literal-codes.lisp

Log Message:
-----------
[Remora] Update XDOC link.


Compare: https://github.com/acl2/acl2/compare/00f3cbf51c0d...cb334a6dc784

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

[Alessandro Coglio]

Branch: refs/heads/master

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-user-01

Commit: 00f3cbf51c0dc12ecb781e0388ac4a0bfcf956b9
https://github.com/acl2/acl2/commit/00f3cbf51c0dc12ecb781e0388ac4a0bfcf956b9
Author: Eric McCarthy <mcca...@kestrel.edu>

Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/parser.lisp

Log Message:
-----------

[remora] grammar and parser: define some component rules for common pieces to reduce the size of the larger rules

Commit: 3514880863d66287f588a76aa14d615a4d0c37e0
https://github.com/acl2/acl2/commit/3514880863d66287f588a76aa14d615a4d0c37e0
Author: Eric McCarthy <mcca...@kestrel.edu>

Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:

M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp

M books/kestrel/remora/syntax-abstraction.lisp

Log Message:
-----------

[remora] finish syntax abstraction and define parse-from-string and parse-from-file


Commit: fb8e08514bb844e9c6226579267e985a1321ea6d
https://github.com/acl2/acl2/commit/fb8e08514bb844e9c6226579267e985a1321ea6d
Author: Eric McCarthy <mcca...@kestrel.edu>

Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:

M books/kestrel/remora/parser-interface.lisp

Log Message:
-----------
[remora] remove reference to missing xdoc topic


Commit: fe1c68e16a002c029dd5ee4c61109d777c8af3f0
https://github.com/acl2/acl2/commit/fe1c68e16a002c029dd5ee4c61109d777c8af3f0
Author: Eric McCarthy <mcca...@kestrel.edu>

Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:

M books/kestrel/remora/parser-interface.lisp

M books/kestrel/remora/syntax-abstraction.lisp

Log Message:
-----------

[remora] adapt make-atom-base to change in ast :value -> :lit


Commit: e74888312bd13b87bd8594019961fa1a5e2993c4
https://github.com/acl2/acl2/commit/e74888312bd13b87bd8594019961fa1a5e2993c4
Author: Eric McCarthy <mcca...@kestrel.edu>

Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:

M books/kestrel/remora/parser-interface.lisp

Log Message:
-----------
[remora] adapt make-atom-base to change in ast :value -> :lit


Commit: 2151df4efcbe25d02d8baf5095dbb86698265fe0
https://github.com/acl2/acl2/commit/2151df4efcbe25d02d8baf5095dbb86698265fe0
Author: Eric McCarthy <mcca...@kestrel.edu>

Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:

A books/kestrel/remora/parse-directory-files.acl2
A books/kestrel/remora/parse-directory-files.lisp
A books/kestrel/remora/top.acl2
M books/kestrel/remora/top.lisp

Log Message:
-----------
[remora] add utility for parsing all the remora files in a directory, for testing purposes


Commit: 3c1e9306f84d788d83403e14f75b7a74c68a77e7
https://github.com/acl2/acl2/commit/3c1e9306f84d788d83403e14f75b7a74c68a77e7
Author: Eric McCarthy <mcca...@kestrel.edu>

Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:

M books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/top.lisp

Log Message:
-----------
[remora] separate two xdoc topics called "parse-directory-files" by renaming the parent one parse-directory-utilities


Commit: 210d0fb7be14c27698387fe754a6993eb814d229
https://github.com/acl2/acl2/commit/210d0fb7be14c27698387fe754a6993eb814d229
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/java/aij/assumptions.lisp
M books/kestrel/java/atj/code-generation.lisp
M books/kestrel/java/atj/common-code-generation.lisp
M books/kestrel/java/atj/java-abstract-syntax.lisp
M books/kestrel/java/atj/library-extensions.lisp
M books/kestrel/java/atj/shallow-quoted-constant-generation.lisp
M books/kestrel/java/atj/tests/acl2-times.lisp
M books/kestrel/java/language/binary-integer-literals.lisp
M books/kestrel/java/language/hexadecimal-integer-literals.lisp
M books/kestrel/java/language/primitive-operations.lisp
M books/kestrel/java/top.lisp

Log Message:
-----------
[java] Fix some doc/comment typos.


Commit: 3863ec070c6ceb8bf58127c9e5b6f6cae5169d7d
https://github.com/acl2/acl2/commit/3863ec070c6ceb8bf58127c9e5b6f6cae5169d7d
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validation-information.lisp

Log Message:
-----------
[C$] Remove enables for newly whitelisted functions

These functions are no longer disabled by
disable-most-builtin-logic-defuns, and so don't need to be enabled in
these proofs.


Commit: bdf9382a60e00301186f383c04f19583fcf3d7c1
https://github.com/acl2/acl2/commit/bdf9382a60e00301186f383c04f19583fcf3d7c1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/java/atj/code-generation.lisp
M books/kestrel/java/atj/common-code-generation.lisp
M books/kestrel/java/atj/deep-code-generation.lisp
M books/kestrel/java/atj/doc.lisp
M books/kestrel/java/atj/input-processing.lisp
M books/kestrel/java/atj/java-abstract-syntax.lisp
M books/kestrel/java/atj/java-primitive-array-model.lisp
M books/kestrel/java/atj/java-primitive-arrays.lisp
M books/kestrel/java/atj/java-syntax-operations.lisp
M books/kestrel/java/atj/name-translation.lisp
M books/kestrel/java/atj/post-translation/cache-const-methods.lisp
M books/kestrel/java/atj/post-translation/lift-loop-tests.lisp
M books/kestrel/java/atj/post-translation/remove-array-write-calls.lisp
M books/kestrel/java/atj/post-translation/remove-continue.lisp
M books/kestrel/java/atj/post-translation/tailrec-elimination.lisp
M books/kestrel/java/atj/pre-translation/array-analysis.lisp
M books/kestrel/java/atj/pre-translation/conjunctions.lisp
M books/kestrel/java/atj/pre-translation/disjunctions.lisp
M books/kestrel/java/atj/pre-translation/multiple-values.lisp
M books/kestrel/java/atj/pre-translation/type-annotation.lisp
M books/kestrel/java/atj/pre-translation/var-renaming.lisp
M books/kestrel/java/atj/pre-translation/var-reuse.lisp
M books/kestrel/java/atj/shallow-code-generation.lisp
M books/kestrel/java/atj/shallow-quoted-constant-generation.lisp
M books/kestrel/java/atj/tests/acl2-times.lisp
M books/kestrel/java/atj/tutorial.lisp
M books/kestrel/java/atj/type-macros.lisp
M books/kestrel/java/atj/types.lisp
M books/kestrel/java/language/binary-integer-literals.lisp
M books/kestrel/java/language/decimal-integer-literals.lisp
M books/kestrel/java/language/escape-sequences.lisp
M books/kestrel/java/language/floating-point-placeholders.lisp
M books/kestrel/java/language/grammar.lisp
M books/kestrel/java/language/hexadecimal-integer-literals.lisp
M books/kestrel/java/language/keywords-validation.lisp
M books/kestrel/java/language/pointers.lisp
M books/kestrel/java/language/primitive-function-macros.lisp
M books/kestrel/java/language/primitive-operations.lisp
M books/kestrel/java/language/primitive-types.lisp
M books/kestrel/java/language/reference-types.lisp
M books/kestrel/java/language/unicode-characters.lisp
M books/kestrel/java/language/unicode-escapes.lisp
M books/kestrel/java/language/unicode-input-characters.lisp

Log Message:
-----------
[Java] Fix doc typos.


Commit: cb24c45c8714629d67de92783f4d9728a98bdc23
https://github.com/acl2/acl2/commit/cb24c45c8714629d67de92783f4d9728a98bdc23
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/java/atj/code-generation.lisp
M books/kestrel/java/atj/common-code-generation.lisp
M books/kestrel/java/atj/deep-code-generation.lisp
M books/kestrel/java/atj/doc.lisp
M books/kestrel/java/atj/input-processing.lisp
M books/kestrel/java/atj/java-abstract-syntax.lisp
M books/kestrel/java/atj/java-primitive-array-model.lisp
M books/kestrel/java/atj/java-primitive-arrays.lisp
M books/kestrel/java/atj/java-syntax-operations.lisp
M books/kestrel/java/atj/name-translation.lisp
M books/kestrel/java/atj/post-translation/cache-const-methods.lisp
M books/kestrel/java/atj/post-translation/lift-loop-tests.lisp
M books/kestrel/java/atj/post-translation/remove-array-write-calls.lisp
M books/kestrel/java/atj/post-translation/remove-continue.lisp
M books/kestrel/java/atj/post-translation/tailrec-elimination.lisp
M books/kestrel/java/atj/pre-translation/array-analysis.lisp
M books/kestrel/java/atj/pre-translation/conjunctions.lisp
M books/kestrel/java/atj/pre-translation/disjunctions.lisp
M books/kestrel/java/atj/pre-translation/multiple-values.lisp
M books/kestrel/java/atj/pre-translation/type-annotation.lisp
M books/kestrel/java/atj/pre-translation/var-renaming.lisp
M books/kestrel/java/atj/pre-translation/var-reuse.lisp
M books/kestrel/java/atj/shallow-code-generation.lisp
M books/kestrel/java/atj/shallow-quoted-constant-generation.lisp
M books/kestrel/java/atj/tests/acl2-times.lisp
M books/kestrel/java/atj/tutorial.lisp
M books/kestrel/java/atj/type-macros.lisp
M books/kestrel/java/atj/types.lisp
M books/kestrel/java/language/binary-integer-literals.lisp
M books/kestrel/java/language/decimal-integer-literals.lisp
M books/kestrel/java/language/escape-sequences.lisp
M books/kestrel/java/language/floating-point-placeholders.lisp
M books/kestrel/java/language/grammar.lisp
M books/kestrel/java/language/hexadecimal-integer-literals.lisp
M books/kestrel/java/language/keywords-validation.lisp
M books/kestrel/java/language/pointers.lisp
M books/kestrel/java/language/primitive-function-macros.lisp
M books/kestrel/java/language/primitive-types.lisp
M books/kestrel/java/language/reference-types.lisp
M books/kestrel/java/language/unicode-characters.lisp
M books/kestrel/java/language/unicode-escapes.lisp
M books/kestrel/java/language/unicode-input-characters.lisp

Log Message:
-----------
[Java] Update file header for files edited in previous commit.


Commit: 231391345b9381aada8115488024c1d138ca3de8
https://github.com/acl2/acl2/commit/231391345b9381aada8115488024c1d138ca3de8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/java/aij/top.lisp
M books/kestrel/java/atj/aij-notions.lisp
M books/kestrel/java/atj/array-write-method-names.lisp
M books/kestrel/java/atj/atj.lisp
M books/kestrel/java/atj/code-generation.lisp
M books/kestrel/java/atj/deep-code-generation.lisp
M books/kestrel/java/atj/doc.lisp
M books/kestrel/java/atj/java-input-types.lisp
M books/kestrel/java/atj/java-pretty-printer.lisp
M books/kestrel/java/atj/java-primitive-array-model.lisp
M books/kestrel/java/atj/java-primitive-arrays.lisp
M books/kestrel/java/atj/java-primitives.lisp
M books/kestrel/java/atj/java-syntax-operations.lisp
M books/kestrel/java/atj/post-translation/cache-const-methods.lisp
M books/kestrel/java/atj/post-translation/fold-returns.lisp
M books/kestrel/java/atj/post-translation/lift-loop-tests.lisp
M books/kestrel/java/atj/post-translation/remove-array-write-calls.lisp
M books/kestrel/java/atj/post-translation/remove-continue.lisp
M books/kestrel/java/atj/post-translation/simplify-conds.lisp
M books/kestrel/java/atj/post-translation/tailrec-elimination.lisp
M books/kestrel/java/atj/post-translation/top.lisp
M books/kestrel/java/atj/pre-translation/array-analysis.lisp
M books/kestrel/java/atj/pre-translation/conjunctions.lisp
M books/kestrel/java/atj/pre-translation/disjunctions.lisp
M books/kestrel/java/atj/pre-translation/multiple-values.lisp
M books/kestrel/java/atj/pre-translation/no-aij-types-analysis.lisp
M books/kestrel/java/atj/pre-translation/remove-dead-if-branches.lisp
M books/kestrel/java/atj/pre-translation/remove-return-last.lisp
M books/kestrel/java/atj/pre-translation/top.lisp
M books/kestrel/java/atj/pre-translation/trivial-vars.lisp
M books/kestrel/java/atj/pre-translation/type-annotation.lisp
M books/kestrel/java/atj/pre-translation/unused-vars.lisp
M books/kestrel/java/atj/pre-translation/var-renaming.lisp
M books/kestrel/java/atj/pre-translation/var-reuse.lisp
M books/kestrel/java/atj/shallow-quoted-constant-generation.lisp
M books/kestrel/java/atj/test-structures.lisp
M books/kestrel/java/atj/tests/abnf.lisp
M books/kestrel/java/atj/tests/booleans.lisp
M books/kestrel/java/atj/tests/cache-const-methods.lisp
M books/kestrel/java/atj/tests/factorial.lisp
M books/kestrel/java/atj/tests/fibonacci.lisp
M books/kestrel/java/atj/tests/hard-error.lisp
M books/kestrel/java/atj/tests/multivalue.lisp
M books/kestrel/java/atj/tests/natives.lisp
M books/kestrel/java/atj/tests/no-aij-types.lisp
M books/kestrel/java/atj/tests/packages.lisp
M books/kestrel/java/atj/tests/primarrays.lisp
M books/kestrel/java/atj/tests/primitives.lisp
M books/kestrel/java/atj/top.lisp
M books/kestrel/java/atj/type-macros.lisp
M books/kestrel/java/atj/types-for-built-ins.lisp
M books/kestrel/java/atj/types-for-bv-fns.lisp
M books/kestrel/java/atj/types-for-ihs-fns.lisp
M books/kestrel/java/atj/types-for-list-fns.lisp
M books/kestrel/java/atj/types-for-natives.lisp
M books/kestrel/java/atj/types-for-std-fns.lisp
M books/kestrel/java/atj/types.lisp
M books/kestrel/java/language/binary-digits-validation.lisp
M books/kestrel/java/language/binary-integer-literals.lisp
M books/kestrel/java/language/boolean-literals-validation.lisp
M books/kestrel/java/language/boolean-literals.lisp
M books/kestrel/java/language/decimal-digits-validation.lisp
M books/kestrel/java/language/decimal-integer-literals.lisp
M books/kestrel/java/language/escape-sequences.lisp
M books/kestrel/java/language/floating-point-value-set-parameters.lisp
M books/kestrel/java/language/hexadecimal-digits-validation.lisp
M books/kestrel/java/language/hexadecimal-integer-literals.lisp
M books/kestrel/java/language/integer-literals.lisp
M books/kestrel/java/language/literals.lisp
M books/kestrel/java/language/null-literal-validation.lisp
M books/kestrel/java/language/null-literal.lisp
M books/kestrel/java/language/octal-digits-validation.lisp
M books/kestrel/java/language/octal-integer-literals.lisp
M books/kestrel/java/language/optional-integer-type-suffix.lisp
M books/kestrel/java/language/package-names.lisp
M books/kestrel/java/language/primitive-conversions.lisp
M books/kestrel/java/language/primitive-types.lisp
M books/kestrel/java/language/primitive-values.lisp
M books/kestrel/java/language/reference-types.lisp
M books/kestrel/java/language/reference-values.lisp
M books/kestrel/java/language/semantics.lisp
M books/kestrel/java/language/syntax.lisp
M books/kestrel/java/language/top.lisp
M books/kestrel/java/language/types.lisp
M books/kestrel/java/language/unicode-escapes.lisp
M books/kestrel/java/language/unicode-input-characters.lisp
M books/kestrel/java/language/values.lisp
M books/kestrel/java/portcullis.lisp

Log Message:
-----------
[Java] Modernize file headers.


Commit: 3912f2c2afb80dc702feb51a0f6fca1364b5eafa
https://github.com/acl2/acl2/commit/3912f2c2afb80dc702feb51a0f6fca1364b5eafa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validation-information.lisp

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


Compare: https://github.com/acl2/acl2/compare/8cd5022fddcd...3912f2c2afb8