[acl2/acl2] 0b9816: [jvm] Tweaks.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 0b98169d00441737568856f7f6cd6687df910b52
https://github.com/acl2/acl2/commit/0b98169d00441737568856f7f6cd6687df910b52
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:
M books/kestrel/jvm/call-stacks.lisp
M books/kestrel/jvm/frames.lisp

Log Message:
-----------
[jvm] Tweaks.


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

Changed paths:
M books/kestrel/axe/.sys/get-di...@useless-runes.lsp
M books/kestrel/axe/get-disjuncts.lisp

Log Message:
-----------
[axe] Clarify code and speed up proofs.


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

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/validator.lisp
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
A books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/character-literal-codes.lisp
A books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/grammar.abnf
A books/kestrel/remora/parse-directory-files.acl2
A books/kestrel/remora/parse-directory-files.lisp
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
A books/kestrel/remora/top.acl2
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-checking.lisp

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


Commit: af109f9d3302dac59e0cec3f7c8430a847adae7a
https://github.com/acl2/acl2/commit/af109f9d3302dac59e0cec3f7c8430a847adae7a
Author: Eric Smith <ews...@gmail.com>
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.


Commit: 059fd35d94541df709dd5a46d647524e92363f8a
https://github.com/acl2/acl2/commit/059fd35d94541df709dd5a46d647524e92363f8a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/compress1.lisp

Log Message:
-----------
[acl2-arrays] Improve comments.


Commit: 4516aec8640ab0ec37dbbd1f623dd3ba18cfe82f
https://github.com/acl2/acl2/commit/4516aec8640ab0ec37dbbd1f623dd3ba18cfe82f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
A books/kestrel/axe/pre-stp-rules.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/top.lisp

Log Message:
-----------
[axe] Create a book that brings in the pre-stp rules.


Commit: 5b5fc52bbd2c608d7318b697028bda17354f9d4a
https://github.com/acl2/acl2/commit/5b5fc52bbd2c608d7318b697028bda17354f9d4a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
A books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp

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


Commit: bcafe9e154b0bb5c778bfe3fb4641f4b1b2db0e8
https://github.com/acl2/acl2/commit/bcafe9e154b0bb5c778bfe3fb4641f4b1b2db0e8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/aref1.lisp
M books/kestrel/acl2-arrays/make-empty-array.lisp

Log Message:
-----------
[acl2-arrays] Clarify.


Commit: b52f0256de7eb63f76d0bbaae95ced60dfaf2ae2
https://github.com/acl2/acl2/commit/b52f0256de7eb63f76d0bbaae95ced60dfaf2ae2
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/.sys/make-into-ar...@useless-runes.lsp
M books/kestrel/acl2-arrays/make-into-array-with-len.lisp

Log Message:
-----------
[acl2-arrays] Generalize rules.


Commit: 0915da35d963143b5e5e2c5f09f11d0c0cae634c
https://github.com/acl2/acl2/commit/0915da35d963143b5e5e2c5f09f11d0c0cae634c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/make-empty-array.lisp
M books/kestrel/acl2-arrays/make-into-array-with-len.lisp
M books/kestrel/acl2-arrays/make-into-array.lisp

Log Message:
-----------
[acl2-arrays] Clarify.


Commit: 919cadc91e950a44aa7023a1ddd5d3f098274b91
https://github.com/acl2/acl2/commit/919cadc91e950a44aa7023a1ddd5d3f098274b91
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/make-into-array-with-len.lisp
M books/kestrel/acl2-arrays/make-into-array.lisp

Log Message:
-----------
[acl2-arrays] Reduce includes.


Commit: 64ddcc477870f06830a64400287d381110fed7d4
https://github.com/acl2/acl2/commit/64ddcc477870f06830a64400287d381110fed7d4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/array-to-alist.lisp
M books/kestrel/acl2-arrays/make-empty-array.lisp
M books/kestrel/acl2-arrays/make-into-array-with-len.lisp
M books/kestrel/acl2-arrays/make-into-array.lisp

Log Message:
-----------
[acl2-arrays] Clarify.

Also simplify hints.


Commit: b53ce9052e8a76b4225d9383def08ce9c852a4bf
https://github.com/acl2/acl2/commit/b53ce9052e8a76b4225d9383def08ce9c852a4bf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/make-empty-array.lisp
M books/kestrel/acl2-arrays/make-into-array.lisp

Log Message:
-----------
[acl2-arrays] Generalize more rules.


Commit: b26ed19dfac0d701709ccbfb16b0bf9d1a946104
https://github.com/acl2/acl2/commit/b26ed19dfac0d701709ccbfb16b0bf9d1a946104
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
R books/kestrel/acl2-arrays/.sys/make-emp...@useless-runes.lsp
A books/kestrel/acl2-arrays/.sys/new-a...@useless-runes.lsp
M books/kestrel/acl2-arrays/acl2-arrays.lisp
R books/kestrel/acl2-arrays/make-empty-array.lisp
M books/kestrel/acl2-arrays/make-into-array.lisp
A books/kestrel/acl2-arrays/new-array1.lisp
M books/kestrel/acl2-arrays/top.lisp
M books/kestrel/acl2-arrays/typed-acl2-arrays-tests.lisp
M books/kestrel/acl2-arrays/typed-acl2-arrays.lisp
M books/kestrel/axe/bounded-dag-parent-arrayp.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/contexts2.lisp
M books/kestrel/axe/crunch-dag.lisp
M books/kestrel/axe/crunch-dag2.lisp
M books/kestrel/axe/dag-array-builders.lisp
M books/kestrel/axe/dag-array-builders2.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-arrayp.lisp
M books/kestrel/axe/dag-size-fast.lisp
M books/kestrel/axe/dag-size-sparse.lisp
M books/kestrel/axe/dag-size.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dagify.lisp
M books/kestrel/axe/dagify0.lisp
M books/kestrel/axe/depth-array.lisp
M books/kestrel/axe/elim.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/evaluate-test-case.lisp
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/extract-dag-array.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/make-assumption-array.lisp
M books/kestrel/axe/make-dag-indices.lisp
M books/kestrel/axe/make-evaluator-tests.lisp
M books/kestrel/axe/make-evaluator.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/make-term-into-dag-array-basic.lisp
M books/kestrel/axe/make-term-into-dag-array-simple.lisp
M books/kestrel/axe/memoization.lisp
M books/kestrel/axe/merge-dag-into-dag-quick.lisp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/prove-with-stp2.lisp
M books/kestrel/axe/prover-common.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/rebuild-literals.lisp
M books/kestrel/axe/rebuild-nodes.lisp
M books/kestrel/axe/rebuild-nodes2.lisp
M books/kestrel/axe/remove-gaps.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/rewriter-alt.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/splitting.lisp
M books/kestrel/axe/substitute-vars2.lisp
M books/kestrel/axe/supporting-nodes.lisp
M books/kestrel/axe/supporting-vars.lisp
M books/kestrel/axe/translation-array.lisp
M books/kestrel/axe/wf-dagp.lisp

Log Message:
-----------
[acl2-arrays] Rename make-empty-array to new-array1.

And similarly for make-empty-array-with-default.


Commit: 92c92c2a336ce7f2d4705934bc9bd0fdf37ee9d4
https://github.com/acl2/acl2/commit/92c92c2a336ce7f2d4705934bc9bd0fdf37ee9d4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/axe/concretize-with-contexts.lisp
M books/kestrel/axe/dag-size.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/find-probable-facts-simple.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/rewriter-alt.lisp

Log Message:
-----------
[axe] Optimize.


Commit: e19f8b42a9d12e23ee2a87acd0a3d619b83109b9
https://github.com/acl2/acl2/commit/e19f8b42a9d12e23ee2a87acd0a3d619b83109b9
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/make-into-array-with-len.lisp
M books/kestrel/acl2-arrays/make-into-array.lisp

Log Message:
-----------
[acl2-arrays] Update todos.


Commit: 1316b8420c4c9c762d4a25fa911bc49d767a3951
https://github.com/acl2/acl2/commit/1316b8420c4c9c762d4a25fa911bc49d767a3951
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
A books/kestrel/acl2-arrays/alist-to-array1-with-len.lisp
A books/kestrel/acl2-arrays/alist-to-array1.lisp
R books/kestrel/acl2-arrays/make-into-array-with-len.lisp
R books/kestrel/acl2-arrays/make-into-array.lisp
M books/kestrel/acl2-arrays/top.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-size-sparse-tests.lisp
M books/kestrel/axe/dagify0.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/find-probable-facts.lisp
M books/kestrel/axe/get-disjuncts.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/make-evaluator-tests.lisp
M books/kestrel/axe/make-evaluator.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-dag-into-dag-quick.lisp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prover-common.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/wf-dagp.lisp

Log Message:
-----------
[acl2-arrays] Rename make-into-array to alist-to-array1.

Add similarly for make-into-array-with-len.


Commit: 8dc8c776cc18c29dfd66127ce87bc74f7a6e74dc
https://github.com/acl2/acl2/commit/8dc8c776cc18c29dfd66127ce87bc74f7a6e74dc
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-gso.lisp
A books/kestrel/c/transformation/tests/split-gso/implicit-initer.c
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
A books/kestrel/c/transformation/tests/split-gso/unnamed-members.c
M books/kestrel/c/transformation/utilities/subst-free.lisp
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/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-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/name-translation.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-code-generation.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/acl2-times.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/tutorial.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-placeholders.lisp
M books/kestrel/java/language/floating-point-value-set-parameters.lisp
M books/kestrel/java/language/grammar.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/keywords-validation.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/pointers.lisp
M books/kestrel/java/language/primitive-conversions.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/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-characters.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
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax.lisp
M books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parse-directory-files.lisp
A books/kestrel/remora/printer.lisp
M books/kestrel/remora/top.lisp

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


Compare: https://github.com/acl2/acl2/compare/ec50a736224e...8dc8c776cc18

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

[Eric W. Smith]

Branch: refs/heads/master

[Eric W. Smith]

Branch: refs/heads/testing