[acl2/acl2] f95653: [axe] More improvements prompted by AI review.

[Eric W. Smith]

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

Changed paths:
M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/defthm-axe.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/rewriter-common.lisp
M books/kestrel/axe/tactic-prover-tests.lisp

Log Message:
-----------
[axe] More improvements prompted by AI review.

Notably, the :counter-example option to defthm-axe has been renamed to :counterexample.


Commit: 4aea1d6ceedc046758a6d98cddec710af6167a40
https://github.com/acl2/acl2/commit/4aea1d6ceedc046758a6d98cddec710af6167a40
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-07 (Tue, 07 Apr 2026)

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

Log Message:
-----------
[jvm] Address issue found in AI review.


Commit: 9e2703c53b5d08a212fc7f953ce3cb8684789dae
https://github.com/acl2/acl2/commit/9e2703c53b5d08a212fc7f953ce3cb8684789dae
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-08 (Wed, 08 Apr 2026)

Changed paths:
M books/kestrel/c/language/implementation-environments/bool-formats.lisp
M books/kestrel/c/language/implementation-environments/dialects.lisp
M books/kestrel/c/language/implementation-environments/integer-format-templates.lisp
M books/kestrel/c/language/implementation-environments/integer-formats.lisp
M books/kestrel/c/language/implementation-environments/schar-formats.lisp
M books/kestrel/c/language/implementation-environments/top.lisp
M books/kestrel/c/language/implementation-environments/uchar-formats.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstraction-mapping.lisp
M books/kestrel/c/syntax/concrete-syntax.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/file-paths.lisp
M books/kestrel/c/syntax/files.lisp
A books/kestrel/c/syntax/grammar-operations.lisp
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/output-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/positions.lisp
M books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/tests/call-graph/call-graph.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/wrap-fn.lisp

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


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

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

Log Message:
-----------
[jvm] Improve checking on individual instructions and sequences.


Commit: 86f6c3ebdddc0e29d9f2a8aa26941c20d2c1909a
https://github.com/acl2/acl2/commit/86f6c3ebdddc0e29d9f2a8aa26941c20d2c1909a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-08 (Wed, 08 Apr 2026)

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

Log Message:
-----------
[jvm] Rename jvm-instructionp to instructionp.


Commit: 8bcf2c46ffd617fecaf905fe72a291cb522ae236
https://github.com/acl2/acl2/commit/8bcf2c46ffd617fecaf905fe72a291cb522ae236
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-08 (Wed, 08 Apr 2026)

Changed paths:
M books/kestrel/axe/jvm/lifter-utilities.lisp
M books/kestrel/axe/jvm/lifter-utilities2.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/jvm/symbolic-execution-rules.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/execution.lisp
M books/kestrel/jvm/instructions.lisp
M books/kestrel/jvm/jvm-facts0.lisp
M books/kestrel/jvm/jvm.lisp

Log Message:
-----------
[jvm] Remove op-code.

Use instruction-opcode instead.


Commit: 514a4d364759c643cd95237cb5b865f32d4ae525
https://github.com/acl2/acl2/commit/514a4d364759c643cd95237cb5b865f32d4ae525
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-08 (Wed, 08 Apr 2026)

Changed paths:
M books/centaur/fgl/clauseproc.lisp
M books/centaur/fgl/config.lisp
M books/centaur/fgl/helper-utils.lisp
M books/centaur/fgl/interp-st.lisp
M books/centaur/fgl/interp.lisp
M books/centaur/fgl/logicman.lisp
M books/centaur/fgl/pathcond-aignet.lisp
M books/centaur/fgl/pathcond.lisp
M books/centaur/fgl/primitives-stub.lisp
A books/centaur/fgl/reference-ctrex.lisp
M books/centaur/fgl/svex-primitives.lisp
M books/centaur/fgl/syntax-bind.lisp
M books/centaur/fgl/top.lisp
M books/centaur/fgl/trace.lisp
M books/kestrel/c/language/portable-ascii-identifiers.lisp
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-options.lisp
M books/kestrel/c/syntax/spans.lisp
A books/kestrel/c/syntax/tests/disamb-example1/included.c
A books/kestrel/c/syntax/tests/disamb-example1/including.c
A books/kestrel/c/syntax/tests/disambiguator-trans-ensembles.lisp
A books/kestrel/c/syntax/tests/disambiguator-trans-units.lisp
R books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/top.lisp
A books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/acl2-customization.lsp
A books/kestrel/remora/package.lsp
A books/kestrel/remora/portcullis.acl2
A books/kestrel/remora/portcullis.lisp
A books/kestrel/remora/top.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp
M books/projects/x86isa/machine/inst-listing.lisp
A books/projects/x86isa/machine/instructions/bcd.lisp
M books/projects/x86isa/machine/instructions/top.lisp

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


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

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

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


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

Changed paths:
M books/kestrel/remora/abstract-syntax.lisp
M books/kestrel/remora/top.lisp
A books/kestrel/strings-light/downcase-tests.lisp

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


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

Changed paths:
M books/kestrel/axe/jvm/lifter-utilities.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/instructions.lisp
M books/kestrel/jvm/jvm.lisp
M books/kestrel/jvm/methods.lisp
M books/kestrel/jvm/strings.lisp

Log Message:
-----------
[jvm] Put some things in the JVM package.


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

Changed paths:
M books/kestrel/jvm/call-stacks.lisp
M books/kestrel/jvm/class-tables.lisp
M books/kestrel/jvm/fields.lisp
M books/kestrel/jvm/intern-table.lisp
M books/kestrel/jvm/methods.lisp

Log Message:
-----------
[jvm] Drop unneeded package prefixes.


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

Changed paths:
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/classes.lisp
M books/kestrel/jvm/events-for-class.lisp
M books/kestrel/jvm/fields.lisp
M books/kestrel/jvm/floats.lisp
M books/kestrel/jvm/floats2.lisp
M books/kestrel/jvm/get-method-info.lisp
M books/kestrel/jvm/int-subtypes.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
M books/kestrel/jvm/method-indicators.lisp
M books/kestrel/jvm/methods.lisp
M books/kestrel/jvm/package.lsp
M books/kestrel/jvm/strings.lisp
M books/kestrel/jvm/values.lisp

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


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

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

Log Message:
-----------
[jvm] Clean up package definition.


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

Changed paths:
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/jvm/arrays.lisp
M books/kestrel/jvm/arrays0.lisp
M books/kestrel/jvm/jvm-facts0.lisp
M books/kestrel/jvm/jvm-rules.lisp

Log Message:
-----------
[jvm] Make array-length a defun.


Compare: https://github.com/acl2/acl2/compare/43d0cb10c1e9...a9e3a3eb7e88

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

[acl2buildserver]

Branch: refs/heads/master

Commit: 532931e28e36f3c8301d9eee567815e6dbacf7cd
https://github.com/acl2/acl2/commit/532931e28e36f3c8301d9eee567815e6dbacf7cd
Author: ACL2 Build Server <acl2bui...@gmail.com>

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

Changed paths:

M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/defthm-axe.lisp
M books/kestrel/axe/jvm/lifter-utilities.lisp
M books/kestrel/axe/jvm/lifter-utilities2.lisp
M books/kestrel/axe/jvm/lifter.lisp

M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/jvm/symbolic-execution-rules.lisp
M books/kestrel/axe/jvm/unroller2.lisp

M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/rewriter-common.lisp
M books/kestrel/axe/tactic-prover-tests.lisp

M books/kestrel/jvm/arrays.lisp
M books/kestrel/jvm/arrays0.lisp
M books/kestrel/jvm/call-stacks.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/class-tables.lisp
M books/kestrel/jvm/classes.lisp
M books/kestrel/jvm/events-for-class.lisp
M books/kestrel/jvm/execution.lisp

M books/kestrel/jvm/fields.lisp
M books/kestrel/jvm/floats.lisp
M books/kestrel/jvm/floats2.lisp
M books/kestrel/jvm/get-method-info.lisp

M books/kestrel/jvm/instructions.lisp

M books/kestrel/jvm/int-subtypes.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-rules.lisp

M books/kestrel/jvm/jvm.lisp
M books/kestrel/jvm/method-indicators.lisp
M books/kestrel/jvm/methods.lisp
M books/kestrel/jvm/package.lsp
M books/kestrel/jvm/strings.lisp

M books/kestrel/jvm/types.lisp

M books/kestrel/jvm/values.lisp

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

Merge commit 'a9e3a3eb7e88785e38a48e82092df0a7384cfeaf' into HEAD


Compare: https://github.com/acl2/acl2/compare/7ce5c03f9d58...532931e28e36

[acl2buildserver]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-user-01

Commit: cba8788ec3472a4513ade557747e5fbd6ee629cf
https://github.com/acl2/acl2/commit/cba8788ec3472a4513ade557747e5fbd6ee629cf
Author: Alessandro Coglio <em...@alessandrocoglio.info>

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

Changed paths:

M books/projects/abnf/grammar-definer/deftreeops.lisp

Log Message:
-----------
[ABNF] Fix some output text.


Commit: 1d93c5c8b41ddd552508a2d029fb18360e251889
https://github.com/acl2/acl2/commit/1d93c5c8b41ddd552508a2d029fb18360e251889
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Merge.


Compare: https://github.com/acl2/acl2/compare/7ce5c03f9d58...1d93c5c8b41d