[acl2/acl2] 042c40: [bv] Reduce includes.

0 views
Skip to first unread message

Eric W. Smith

unread,
Jul 27, 2026, 3:22:21 PM (2 days ago) Jul 27
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 042c40eb326ce568e6623f77a86e5c2dccb0c97a
https://github.com/acl2/acl2/commit/042c40eb326ce568e6623f77a86e5c2dccb0c97a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-21 (Tue, 21 Jul 2026)

Changed paths:
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/logext.lisp

Log Message:
-----------
[bv] Reduce includes.


Commit: 17cbaa9c6ac6cf1d0b1e71d5d6125c8fe4f8c857
https://github.com/acl2/acl2/commit/17cbaa9c6ac6cf1d0b1e71d5d6125c8fe4f8c857
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-21 (Tue, 21 Jul 2026)

Changed paths:
M books/kestrel/arithmetic-light/divide.lisp
M books/kestrel/arithmetic-light/expt.lisp
M books/kestrel/arithmetic-light/numerator.lisp

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


Commit: 8b8d5c448b5458e2c5e6dd880f9e73958a3694c3
https://github.com/acl2/acl2/commit/8b8d5c448b5458e2c5e6dd880f9e73958a3694c3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-21 (Tue, 21 Jul 2026)

Changed paths:
M books/kestrel/arithmetic-light/minus.lisp

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


Commit: e74bbf5daea2de3b1c95c497bd4463af31a4b1c1
https://github.com/acl2/acl2/commit/e74bbf5daea2de3b1c95c497bd4463af31a4b1c1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-21 (Tue, 21 Jul 2026)

Changed paths:
M books/kestrel/arithmetic-light/mod.lisp

Log Message:
-----------
[arithmetic-light] Improve hint.


Commit: 9d00310eba797d7cb78dc328ebad1534b6b4ddcf
https://github.com/acl2/acl2/commit/9d00310eba797d7cb78dc328ebad1534b6b4ddcf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-22 (Wed, 22 Jul 2026)

Changed paths:
M Makefile
M axioms.lisp
M books/Makefile
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation-rules.lisp
M books/kestrel/remora/evaluation-tests.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking-tests.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names-validation.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp
M ld.lisp
M other-events.lisp

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


Commit: 6d9e94442ca7623a0425273231a0c371e6043d2e
https://github.com/acl2/acl2/commit/6d9e94442ca7623a0425273231a0c371e6043d2e
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-22 (Wed, 22 Jul 2026)

Changed paths:
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp

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


Commit: 21939fb21587da12b61411bf4ee474b9e68e5b5f
https://github.com/acl2/acl2/commit/21939fb21587da12b61411bf4ee474b9e68e5b5f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-23 (Thu, 23 Jul 2026)

Changed paths:
M axioms.lisp
M books/kestrel/arithmetic-light/minus.lisp
M books/kestrel/arithmetic-light/numerator.lisp
M books/kestrel/c/atc/support/top.lisp
M books/kestrel/c/syntax/printer.lisp
A books/kestrel/fty/symbol-set-set.lisp
M books/kestrel/fty/top.lisp
R books/kestrel/memory/acl2-customization.lsp
A books/kestrel/memory/make-memory-region-machinery.acl2
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/arithmetic.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/library-extensions.lisp
M books/kestrel/remora/monomorphize.lisp
A books/kestrel/remora/omaps.lisp
R books/kestrel/remora/oset-omaps.lisp
A books/kestrel/remora/osets.lisp
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/type-values-and-environments.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/projects/abnf/notation/semantics.lisp
M books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/abnf/tree-operations/top.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp

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


Commit: c1479130a8c7c42c811fc97987d93f02b5a1101b
https://github.com/acl2/acl2/commit/c1479130a8c7c42c811fc97987d93f02b5a1101b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/array-declarators.c
A books/kestrel/c/transformation/tests/struct-type-split/array-index-effectful.c
A books/kestrel/c/transformation/tests/struct-type-split/array-init-designated.c
A books/kestrel/c/transformation/tests/struct-type-split/array-init-inferred-designated.c
A books/kestrel/c/transformation/tests/struct-type-split/array-init-positional.c
A books/kestrel/c/transformation/tests/struct-type-split/array-initializers.c
A books/kestrel/c/transformation/tests/struct-type-split/array-member-flexible-after-anon.c
A books/kestrel/c/transformation/tests/struct-type-split/array-member-flexible-nested-anon.c
A books/kestrel/c/transformation/tests/struct-type-split/array-member-flexible.c
A books/kestrel/c/transformation/tests/struct-type-split/array-member-sized-typedef.c
A books/kestrel/c/transformation/tests/struct-type-split/array-member.c
A books/kestrel/c/transformation/tests/struct-type-split/array-vla-effectful.c
M books/kestrel/c/transformation/tests/struct-type-split/array.c
A books/kestrel/c/transformation/tests/struct-type-split/partial-init.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp

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


Commit: 936fde5c60298b0e687fd5f4c996db01a36ece08
https://github.com/acl2/acl2/commit/936fde5c60298b0e687fd5f4c996db01a36ece08
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M axioms.lisp
M books/demos/brr-free-variables-log.txt
M books/doc/relnotes.lisp
M books/kestrel/data/treemap/doc.lisp
M books/kestrel/data/treemap/keys.lisp
M books/kestrel/data/treemap/package.lsp
M books/kestrel/data/treemap/values.lisp
M books/kestrel/data/treeset/defs.lisp
A books/kestrel/data/treeset/generic-count.lisp
M books/kestrel/data/treeset/generic-typed.lisp
M books/kestrel/data/treeset/internal/iter.lisp
M books/kestrel/data/treeset/internal/tree.lisp
M books/kestrel/data/treeset/iter.lisp
M books/kestrel/data/treeset/package.lsp
M books/kestrel/data/treeset/top.lisp
M books/kestrel/file-io-light/channels.lisp
M books/kestrel/file-io-light/close-output-channel.lisp
M books/kestrel/file-io-light/open-channels-p.lisp
M books/kestrel/file-io-light/read-byte-dollar.lisp
M books/kestrel/file-io-light/read-char-dollar.lisp
M books/kestrel/file-io-light/read-object.lisp
A books/kestrel/fty/set-list.lisp
A books/kestrel/fty/symbol-set-list-list.lisp
A books/kestrel/fty/symbol-set-list.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/lists.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/type-values-and-environments.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
A books/kestrel/utilities/bind-to-bool.lisp
M books/kestrel/utilities/ld-history.lisp
M books/kestrel/utilities/state.lisp
M books/kestrel/utilities/top.lisp
M books/projects/fields/README
M books/projects/fields/embeddings.lisp
M books/projects/fields/extensions.lisp
M books/projects/fields/galois.lisp
A books/projects/fields/polynomials.lisp
M books/projects/fields/support/embeddings.lisp
M books/projects/fields/support/galois.lisp
A books/projects/fields/vectors.lisp
M books/projects/linear/field.lisp
M books/projects/linear/ring.lisp
M books/projects/linear/support/field.lisp
M books/projects/linear/support/ring.lisp
M books/projects/linear/support/vectors.lisp
M books/projects/linear/vectors.lisp
M books/std/io/base.lisp
M books/std/util/definductive.lisp
M books/system/doc/acl2-doc.lisp
M books/system/update-state.lisp
M books/tools/with-supporters.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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


Commit: 0160eab834466ca15482741553adc66f5325ccf4
https://github.com/acl2/acl2/commit/0160eab834466ca15482741553adc66f5325ccf4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/memory/make-memory-region-machinery.lisp

Log Message:
-----------
[memory] Speed up book.

Without any local events, nothing needs to be rolled back for the local incompatibility check.


Commit: 6dc75040be50008759ce75d1e7c266d335a61d18
https://github.com/acl2/acl2/commit/6dc75040be50008759ce75d1e7c266d335a61d18
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/axe/unify-term-and-dag-fast-correct.lisp
M books/kestrel/axe/unify-term-and-dag.lisp
M books/kestrel/clause-processors/push-unary-fns-into-lambdas.lisp
M books/kestrel/clause-processors/push-unary-fns.lisp
M books/kestrel/evaluators/defevaluator-theorems.lisp
M books/kestrel/helpers/linter.lisp
M books/kestrel/helpers/model-induct.lisp
M books/kestrel/lists-light/intersection-equal.lisp
M books/kestrel/lists-light/no-duplicatesp-equal.lisp
M books/kestrel/lists-light/remove1-equal.lisp
M books/kestrel/terms-light/arglistp1.lisp
M books/kestrel/terms-light/bound-vars-in-term.lisp
M books/kestrel/terms-light/combine-ifs-in-then-and-else-branches.lisp
M books/kestrel/terms-light/copy-term-proofs.lisp
M books/kestrel/terms-light/drop-trivial-lambdas-proofs.lisp
M books/kestrel/terms-light/drop-trivial-lambdas.lisp
M books/kestrel/terms-light/drop-unused-lambda-bindings-proofs.lisp
M books/kestrel/terms-light/drop-unused-lambda-bindings.lisp
M books/kestrel/terms-light/empty-eval-helpers.lisp
M books/kestrel/terms-light/expand-lambdas-in-term-proofs.lisp
M books/kestrel/terms-light/expand-lambdas-in-term.lisp
M books/kestrel/terms-light/free-vars-in-term.lisp
M books/kestrel/terms-light/function-call-subterms.lisp
M books/kestrel/terms-light/get-conjuncts.lisp
M books/kestrel/terms-light/lambdas-closed-in-termp.lisp
M books/kestrel/terms-light/let-bind-formals-in-calls.lisp
M books/kestrel/terms-light/let-vars-in-term.lisp
M books/kestrel/terms-light/logic-fnsp.lisp
M books/kestrel/terms-light/no-duplicate-lambda-formals-in-termp.lisp
M books/kestrel/terms-light/no-nils-in-termp.lisp
M books/kestrel/terms-light/non-trivial-formals.lisp
M books/kestrel/terms-light/reconstruct-lets-in-term-proofs.lisp
M books/kestrel/terms-light/reconstruct-lets-in-term.lisp
M books/kestrel/terms-light/rename-vars-in-term.lisp
M books/kestrel/terms-light/replace-term-with-term.lisp
M books/kestrel/terms-light/serialize-lambdas-in-term-proofs.lisp
M books/kestrel/terms-light/serialize-lambdas-in-term.lisp
M books/kestrel/terms-light/simple-untranslate-in-term-proofs.lisp
M books/kestrel/terms-light/simplify-ors-proofs.lisp
M books/kestrel/terms-light/simplify-ors.lisp
M books/kestrel/terms-light/sublis-var-and-magic-eval.lisp
M books/kestrel/terms-light/sublis-var-simple-proofs.lisp
M books/kestrel/terms-light/subst-var-alt-proofs.lisp
M books/kestrel/terms-light/subst-var-alt.lisp
M books/kestrel/terms-light/subst-var-deep.lisp
M books/kestrel/terms-light/substitute-constants-in-lambdas-proofs.lisp
M books/kestrel/terms-light/substitute-constants-in-lambdas.lisp
M books/kestrel/terms-light/substitute-lambda-formals.lisp
M books/kestrel/terms-light/substitute-unnecessary-lambda-vars.lisp
M books/kestrel/terms-light/substitute-unnecessary-lambda-vars2-proofs.lisp
M books/kestrel/terms-light/substitute-unnecessary-lambda-vars2.lisp
M books/kestrel/terms-light/termp-simple.lisp
M books/kestrel/utilities/all-vars-in-term-bound-in-alistp.lisp
M books/kestrel/utilities/defopeners.lisp
M books/kestrel/utilities/terms.lisp

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


Commit: 0ac898a0a60a3d0c33fc52283494f517f034d77b
https://github.com/acl2/acl2/commit/0ac898a0a60a3d0c33fc52283494f517f034d77b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/file-io-light/close-input-channel.lisp
M books/kestrel/file-io-light/prin1-dollar.lisp
M books/kestrel/file-io-light/prin1-with-slashes.lisp
M books/kestrel/file-io-light/prin1-with-slashes1.lisp
M books/kestrel/file-io-light/read-objects-from-channel.lisp
M books/kestrel/file-io-light/read-objects-from-file.lisp
M books/kestrel/file-io-light/write-bytes-to-file.lisp
M books/kestrel/file-io-light/write-objects-to-channel.lisp
M books/kestrel/file-io-light/write-strings-to-file-bang.lisp
M books/kestrel/file-io-light/write-strings-to-file.lisp
M books/kestrel/lists-light/subseq-list.lisp
M books/kestrel/number-theory/mod.lisp
M books/kestrel/strings-light/add-prefix-to-strings.lisp
M books/kestrel/strings-light/decimal-digits.lisp
M books/kestrel/strings-light/downcase.lisp
M books/kestrel/strings-light/reverse.lisp
M books/kestrel/strings-light/split-chars.lisp
M books/kestrel/strings-light/split-string-last.lisp
M books/kestrel/strings-light/strcdr.lisp
M books/kestrel/strings-light/strip-prefix-from-string.lisp
M books/kestrel/strings-light/strnthcdr.lisp
M books/kestrel/strings-light/subseq.lisp
M books/kestrel/strings-light/upcase.lisp

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


Compare: https://github.com/acl2/acl2/compare/353bc6572a32...0ac898a0a60a

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

Alessandro Coglio

unread,
Jul 27, 2026, 5:16:48 PM (2 days ago) Jul 27
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: eccd1f774325f10e687e50afadc0cdd85315a7e9
https://github.com/acl2/acl2/commit/eccd1f774325f10e687e50afadc0cdd85315a7e9
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-21 (Tue, 21 Jul 2026)

Changed paths:
M books/kestrel/lists-light/intersection-equal.lisp
M books/kestrel/lists-light/no-duplicatesp-equal.lisp
M books/kestrel/lists-light/remove1-equal.lisp

Log Message:
-----------
[lists-light] Add some rules.

Also make sure a rule about intersection-equal is in that book.


Commit: a9c1e05f1498827c69d83f498a7e6e434a1131dd
https://github.com/acl2/acl2/commit/a9c1e05f1498827c69d83f498a7e6e434a1131dd
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-21 (Tue, 21 Jul 2026)

Changed paths:
M books/kestrel/terms-light/arglistp1.lisp
M books/kestrel/terms-light/get-conjuncts.lisp
M books/kestrel/terms-light/logic-fnsp.lisp
M books/kestrel/terms-light/non-trivial-formals.lisp
M books/kestrel/terms-light/serialize-lambdas-in-term-proofs.lisp

Log Message:
-----------
[terms-light] Add some rules.

And remove one now in lists-light.


Commit: e74bbf5daea2de3b1c95c497bd4463af31a4b1c1
https://github.com/acl2/acl2/commit/e74bbf5daea2de3b1c95c497bd4463af31a4b1c1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-21 (Tue, 21 Jul 2026)

Changed paths:
M books/kestrel/arithmetic-light/mod.lisp

Log Message:
-----------
[arithmetic-light] Improve hint.


Commit: b17917a040b3055372c1006b234aed32bd6ce757
https://github.com/acl2/acl2/commit/b17917a040b3055372c1006b234aed32bd6ce757
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-22 (Wed, 22 Jul 2026)

Changed paths:
M Makefile
M axioms.lisp
M books/Makefile
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation-rules.lisp
M books/kestrel/remora/evaluation-tests.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking-tests.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names-validation.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
Commit: 1d7d68e9aa7345169b1b8db053a04ac9224c58a3
https://github.com/acl2/acl2/commit/1d7d68e9aa7345169b1b8db053a04ac9224c58a3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-22 (Wed, 22 Jul 2026)

Changed paths:
M books/kestrel/c/atc/support/top.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names-validation.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp

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


Commit: 20a96249ae9d64e06a7e62dc4f3055a72aa1c717
https://github.com/acl2/acl2/commit/20a96249ae9d64e06a7e62dc4f3055a72aa1c717
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-22 (Wed, 22 Jul 2026)

Changed paths:
M books/kestrel/utilities/ld-history.lisp

Log Message:
-----------
[utilities] Update comment.


Commit: 38516e629135c93a326c032d3ff9a523847f1adb
https://github.com/acl2/acl2/commit/38516e629135c93a326c032d3ff9a523847f1adb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-23 (Thu, 23 Jul 2026)

Changed paths:
M axioms.lisp
A books/kestrel/fty/symbol-set-set.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/remora/type-values-and-environments.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/projects/abnf/notation/semantics.lisp
M books/projects/abnf/tree-operations/subtree-operations.lisp
M books/projects/abnf/tree-operations/top.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp

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


Commit: cef8b33069e4e02631e406163a76af8fe82adfda
https://github.com/acl2/acl2/commit/cef8b33069e4e02631e406163a76af8fe82adfda
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-23 (Thu, 23 Jul 2026)

Changed paths:
M axioms.lisp
M books/kestrel/arithmetic-light/minus.lisp
M books/kestrel/arithmetic-light/numerator.lisp
A books/kestrel/fty/symbol-set-set.lisp
M books/kestrel/fty/top.lisp
R books/kestrel/memory/acl2-customization.lsp
A books/kestrel/memory/make-memory-region-machinery.acl2
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
Commit: fb218277b2d80285a7147abc9e4a4c2a91df908d
https://github.com/acl2/acl2/commit/fb218277b2d80285a7147abc9e4a4c2a91df908d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-23 (Thu, 23 Jul 2026)

Changed paths:
M books/kestrel/arithmetic-light/minus.lisp
M books/kestrel/arithmetic-light/numerator.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/arithmetic.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/library-extensions.lisp
M books/kestrel/remora/monomorphize.lisp
A books/kestrel/remora/omaps.lisp
R books/kestrel/remora/oset-omaps.lisp
A books/kestrel/remora/osets.lisp
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/type-values-and-environments.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/std/util/definductive.lisp

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


Commit: 6d80b3911a5943eea4461fdcbe1cc49399dfa85b
https://github.com/acl2/acl2/commit/6d80b3911a5943eea4461fdcbe1cc49399dfa85b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-23 (Thu, 23 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/arithmetic.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/library-extensions.lisp
M books/kestrel/remora/monomorphize.lisp
A books/kestrel/remora/omaps.lisp
R books/kestrel/remora/oset-omaps.lisp
A books/kestrel/remora/osets.lisp
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/type-values-and-environments.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/std/util/definductive.lisp

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


Commit: 45c9bb6bdcc5aad2048b75c83b2d3ae13eabc187
https://github.com/acl2/acl2/commit/45c9bb6bdcc5aad2048b75c83b2d3ae13eabc187
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
Commit: b65ddef17c1aeec3c3fc39d32934ec220e975eae
https://github.com/acl2/acl2/commit/b65ddef17c1aeec3c3fc39d32934ec220e975eae
Commit: ce6074a2423bac5cce070099ef4aa95777646cc4
https://github.com/acl2/acl2/commit/ce6074a2423bac5cce070099ef4aa95777646cc4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp

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


Commit: 578abc70d30e9776d898cb2b458b5bb579dd918f
https://github.com/acl2/acl2/commit/578abc70d30e9776d898cb2b458b5bb579dd918f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/data/treemap/doc.lisp
M books/kestrel/data/treemap/keys.lisp
M books/kestrel/data/treemap/package.lsp
M books/kestrel/data/treemap/values.lisp
M books/kestrel/data/treeset/defs.lisp
A books/kestrel/data/treeset/generic-count.lisp
M books/kestrel/data/treeset/generic-typed.lisp
M books/kestrel/data/treeset/internal/iter.lisp
M books/kestrel/data/treeset/internal/tree.lisp
M books/kestrel/data/treeset/iter.lisp
M books/kestrel/data/treeset/package.lsp
M books/kestrel/data/treeset/top.lisp
A books/kestrel/fty/symbol-set-list-list.lisp
A books/kestrel/fty/symbol-set-list.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/lists.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/type-values-and-environments.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/projects/fields/README
M books/projects/fields/embeddings.lisp
M books/projects/fields/extensions.lisp
M books/projects/fields/galois.lisp
A books/projects/fields/polynomials.lisp
M books/projects/fields/support/embeddings.lisp
M books/projects/fields/support/galois.lisp
A books/projects/fields/vectors.lisp
M books/projects/linear/field.lisp
M books/projects/linear/ring.lisp
M books/projects/linear/support/field.lisp
M books/projects/linear/support/ring.lisp
M books/projects/linear/support/vectors.lisp
M books/projects/linear/vectors.lisp
M books/std/util/definductive.lisp

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


Commit: 7b09d5b8663845b21395d5d1a496541c6aec12cd
https://github.com/acl2/acl2/commit/7b09d5b8663845b21395d5d1a496541c6aec12cd
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/data/treemap/doc.lisp
M books/kestrel/data/treemap/keys.lisp
M books/kestrel/data/treemap/package.lsp
M books/kestrel/data/treemap/values.lisp
M books/kestrel/data/treeset/defs.lisp
A books/kestrel/data/treeset/generic-count.lisp
M books/kestrel/data/treeset/generic-typed.lisp
M books/kestrel/data/treeset/internal/iter.lisp
M books/kestrel/data/treeset/internal/tree.lisp
M books/kestrel/data/treeset/iter.lisp
M books/kestrel/data/treeset/package.lsp
M books/kestrel/data/treeset/top.lisp
A books/kestrel/fty/symbol-set-list-list.lisp
A books/kestrel/fty/symbol-set-list.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/dimension-equivalence-infrules.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/lists.lisp
M books/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/type-values-and-environments.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/projects/fields/README
M books/projects/fields/embeddings.lisp
M books/projects/fields/extensions.lisp
M books/projects/fields/galois.lisp
A books/projects/fields/polynomials.lisp
M books/projects/fields/support/embeddings.lisp
M books/projects/fields/support/galois.lisp
A books/projects/fields/vectors.lisp
M books/projects/linear/field.lisp
M books/projects/linear/ring.lisp
M books/projects/linear/support/field.lisp
M books/projects/linear/support/ring.lisp
M books/projects/linear/support/vectors.lisp
M books/projects/linear/vectors.lisp
M books/std/util/definductive.lisp

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


Commit: f0fa077e9fc1a046e73edae592a39aad79d15394
https://github.com/acl2/acl2/commit/f0fa077e9fc1a046e73edae592a39aad79d15394
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/fty/symbol-set-list-list.lisp

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


Commit: 3f7e2f73e90f91dfea2653a327394b025980f70c
https://github.com/acl2/acl2/commit/3f7e2f73e90f91dfea2653a327394b025980f70c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/std/util/definductive.lisp

Log Message:
-----------
[definductive] Streamline some proofs.


Commit: 4e3269495b949e92a750cba00f4cbb2d7a7b7126
https://github.com/acl2/acl2/commit/4e3269495b949e92a750cba00f4cbb2d7a7b7126
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/doc/relnotes.lisp
M books/tools/with-supporters.lisp

Log Message:
-----------
Fixed theory bug in with-supporters.

Quoting :DOC note-8-8-books:

Fixed a bug in [with-supporters] that was preventing [disable]s for
names of theorems (as opposed to functions.

Thanks to Eric Smith for pointing out this bug with an example.


Commit: 50b7500ce63150e1ca71c2f59d1867b36fe5922a
https://github.com/acl2/acl2/commit/50b7500ce63150e1ca71c2f59d1867b36fe5922a
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/doc/relnotes.lisp

Log Message:
-----------
Add missing right parenthesis in recently-updated :DOC note-8-8-books.


Commit: bc5fb9635891154093a402eb6097499ca5eaf35b
https://github.com/acl2/acl2/commit/bc5fb9635891154093a402eb6097499ca5eaf35b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/doc/relnotes.lisp
M books/tools/with-supporters.lisp

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


Commit: 6709dd015c3064d844987ae50655d0187643b2cf
https://github.com/acl2/acl2/commit/6709dd015c3064d844987ae50655d0187643b2cf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M axioms.lisp
M books/demos/brr-free-variables-log.txt
M books/doc/relnotes.lisp
M books/kestrel/file-io-light/channels.lisp
M books/kestrel/file-io-light/close-output-channel.lisp
M books/kestrel/file-io-light/open-channels-p.lisp
M books/kestrel/file-io-light/read-byte-dollar.lisp
M books/kestrel/file-io-light/read-char-dollar.lisp
M books/kestrel/file-io-light/read-object.lisp
A books/kestrel/fty/set-list.lisp
M books/kestrel/fty/symbol-set-list-list.lisp
M books/kestrel/fty/symbol-set-list.lisp
M books/kestrel/fty/top.lisp
A books/kestrel/utilities/bind-to-bool.lisp
M books/kestrel/utilities/state.lisp
M books/kestrel/utilities/top.lisp
M books/std/io/base.lisp
M books/std/util/definductive.lisp
M books/system/doc/acl2-doc.lisp
M books/system/update-state.lisp
M books/tools/with-supporters.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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


Commit: b4fdaa8143c8db650b7772834a092bb1102773ba
https://github.com/acl2/acl2/commit/b4fdaa8143c8db650b7772834a092bb1102773ba
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/utilities/all-vars-in-term-bound-in-alistp.lisp
M books/kestrel/utilities/defopeners.lisp
M books/kestrel/utilities/terms.lisp

Log Message:
-----------
[utilities] Improve use of make-flag.


Commit: fcce54eef86a99f3335fe145012e59f5b636a6af
https://github.com/acl2/acl2/commit/fcce54eef86a99f3335fe145012e59f5b636a6af
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/axe/unify-term-and-dag-fast-correct.lisp
M books/kestrel/axe/unify-term-and-dag.lisp

Log Message:
-----------
[axe] Improve use of make-flag.


Commit: 49d8988bfaea4617c88df7fa488dfd72cf6509db
https://github.com/acl2/acl2/commit/49d8988bfaea4617c88df7fa488dfd72cf6509db
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/clause-processors/push-unary-fns-into-lambdas.lisp
M books/kestrel/clause-processors/push-unary-fns.lisp

Log Message:
-----------
[clause-processors] Improve use of make-flag.


Commit: fef9f8b828115862449e02a85888c119839c5ac8
https://github.com/acl2/acl2/commit/fef9f8b828115862449e02a85888c119839c5ac8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/evaluators/defevaluator-theorems.lisp

Log Message:
-----------
[evaluators] Improve use of make-flag.


Commit: 70d74aef89f710f55619b56f31b8addf393b701e
https://github.com/acl2/acl2/commit/70d74aef89f710f55619b56f31b8addf393b701e
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/helpers/linter.lisp
M books/kestrel/helpers/model-induct.lisp

Log Message:
-----------
[helpers] Improve use of make-flag.


Commit: 0719f0d587f4178ba0671a07dd8ac7d5f61a7c7d
https://github.com/acl2/acl2/commit/0719f0d587f4178ba0671a07dd8ac7d5f61a7c7d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/terms-light/bound-vars-in-term.lisp
M books/kestrel/terms-light/combine-ifs-in-then-and-else-branches.lisp
M books/kestrel/terms-light/copy-term-proofs.lisp
M books/kestrel/terms-light/drop-trivial-lambdas-proofs.lisp
M books/kestrel/terms-light/drop-trivial-lambdas.lisp
M books/kestrel/terms-light/drop-unused-lambda-bindings-proofs.lisp
M books/kestrel/terms-light/drop-unused-lambda-bindings.lisp
M books/kestrel/terms-light/empty-eval-helpers.lisp
M books/kestrel/terms-light/expand-lambdas-in-term-proofs.lisp
M books/kestrel/terms-light/expand-lambdas-in-term.lisp
M books/kestrel/terms-light/free-vars-in-term.lisp
M books/kestrel/terms-light/function-call-subterms.lisp
M books/kestrel/terms-light/lambdas-closed-in-termp.lisp
M books/kestrel/terms-light/let-bind-formals-in-calls.lisp
M books/kestrel/terms-light/let-vars-in-term.lisp
M books/kestrel/terms-light/no-duplicate-lambda-formals-in-termp.lisp
M books/kestrel/terms-light/no-nils-in-termp.lisp
M books/kestrel/terms-light/reconstruct-lets-in-term-proofs.lisp
M books/kestrel/terms-light/reconstruct-lets-in-term.lisp
M books/kestrel/terms-light/rename-vars-in-term.lisp
M books/kestrel/terms-light/replace-term-with-term.lisp
M books/kestrel/terms-light/serialize-lambdas-in-term-proofs.lisp
M books/kestrel/terms-light/serialize-lambdas-in-term.lisp
M books/kestrel/terms-light/simple-untranslate-in-term-proofs.lisp
M books/kestrel/terms-light/simplify-ors-proofs.lisp
M books/kestrel/terms-light/simplify-ors.lisp
M books/kestrel/terms-light/sublis-var-and-magic-eval.lisp
M books/kestrel/terms-light/sublis-var-simple-proofs.lisp
M books/kestrel/terms-light/subst-var-alt-proofs.lisp
M books/kestrel/terms-light/subst-var-alt.lisp
M books/kestrel/terms-light/subst-var-deep.lisp
M books/kestrel/terms-light/substitute-constants-in-lambdas-proofs.lisp
M books/kestrel/terms-light/substitute-constants-in-lambdas.lisp
M books/kestrel/terms-light/substitute-lambda-formals.lisp
M books/kestrel/terms-light/substitute-unnecessary-lambda-vars.lisp
M books/kestrel/terms-light/substitute-unnecessary-lambda-vars2-proofs.lisp
M books/kestrel/terms-light/substitute-unnecessary-lambda-vars2.lisp
M books/kestrel/terms-light/termp-simple.lisp

Log Message:
-----------
[terms-light] Improve use of make-flag.


Commit: 54521946294d8b52a92fba0ef9a219c4a4c9f1b9
https://github.com/acl2/acl2/commit/54521946294d8b52a92fba0ef9a219c4a4c9f1b9
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M axioms.lisp
M books/demos/brr-free-variables-log.txt
M books/doc/relnotes.lisp
M books/kestrel/file-io-light/channels.lisp
M books/kestrel/file-io-light/close-output-channel.lisp
M books/kestrel/file-io-light/open-channels-p.lisp
M books/kestrel/file-io-light/read-byte-dollar.lisp
M books/kestrel/file-io-light/read-char-dollar.lisp
M books/kestrel/file-io-light/read-object.lisp
A books/kestrel/fty/set-list.lisp
M books/kestrel/fty/symbol-set-list-list.lisp
M books/kestrel/fty/symbol-set-list.lisp
M books/kestrel/fty/top.lisp
A books/kestrel/utilities/bind-to-bool.lisp
M books/kestrel/utilities/state.lisp
M books/kestrel/utilities/top.lisp
M books/std/io/base.lisp
M books/std/util/definductive.lisp
M books/system/doc/acl2-doc.lisp
M books/system/update-state.lisp
M books/tools/with-supporters.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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


Commit: 535a7a256dbde98db1678736fb7430c4b9d96326
https://github.com/acl2/acl2/commit/535a7a256dbde98db1678736fb7430c4b9d96326
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/lists-light/subseq-list.lisp

Log Message:
-----------
[lists-light] Add rule.


Commit: 590c846d1df6f3d74e60f5f6a47f1322adb5f253
https://github.com/acl2/acl2/commit/590c846d1df6f3d74e60f5f6a47f1322adb5f253
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:
M books/kestrel/strings-light/add-prefix-to-strings.lisp
M books/kestrel/strings-light/decimal-digits.lisp
M books/kestrel/strings-light/downcase.lisp
M books/kestrel/strings-light/reverse.lisp
M books/kestrel/strings-light/split-chars.lisp
M books/kestrel/strings-light/split-string-last.lisp
M books/kestrel/strings-light/strcdr.lisp
M books/kestrel/strings-light/strip-prefix-from-string.lisp
M books/kestrel/strings-light/strnthcdr.lisp
M books/kestrel/strings-light/subseq.lisp
M books/kestrel/strings-light/upcase.lisp

Log Message:
-----------
[strings-light] Add various rules.
Commit: 033bd3d6ad759cf5d6d9cd2a5720aea36416ae5d
https://github.com/acl2/acl2/commit/033bd3d6ad759cf5d6d9cd2a5720aea36416ae5d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/lists-light/subseq-list.lisp

Log Message:
-----------
[lights-light] Tweak rule to avoid clash with STD.


Commit: e09e22f2de682e2bec66f17ecb62f8e2847368d9
https://github.com/acl2/acl2/commit/e09e22f2de682e2bec66f17ecb62f8e2847368d9
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/number-theory/mod.lisp

Log Message:
-----------
[number-theory] Add a rule.


Commit: 8c8fb675e97e006cba6edb6f686b4f15205853c6
https://github.com/acl2/acl2/commit/8c8fb675e97e006cba6edb6f686b4f15205853c6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/file-io-light/close-input-channel.lisp
M books/kestrel/file-io-light/prin1-dollar.lisp
M books/kestrel/file-io-light/prin1-with-slashes.lisp
M books/kestrel/file-io-light/prin1-with-slashes1.lisp
M books/kestrel/file-io-light/read-objects-from-channel.lisp
M books/kestrel/file-io-light/read-objects-from-file.lisp
M books/kestrel/file-io-light/write-bytes-to-file.lisp
M books/kestrel/file-io-light/write-objects-to-channel.lisp
M books/kestrel/file-io-light/write-strings-to-file-bang.lisp
M books/kestrel/file-io-light/write-strings-to-file.lisp

Log Message:
-----------
[file-io-light] Add various missing rules.


Commit: 78dcb9f9b968d613bf080549ea2fc65a39cf1a84
https://github.com/acl2/acl2/commit/78dcb9f9b968d613bf080549ea2fc65a39cf1a84
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/utilities/ld-history.lisp

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


Commit: 0160eab834466ca15482741553adc66f5325ccf4
https://github.com/acl2/acl2/commit/0160eab834466ca15482741553adc66f5325ccf4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/memory/make-memory-region-machinery.lisp

Log Message:
-----------
[memory] Speed up book.

Without any local events, nothing needs to be rolled back for the local incompatibility check.


Commit: 353bc6572a32029ff14d53835d84c86708e5155a
https://github.com/acl2/acl2/commit/353bc6572a32029ff14d53835d84c86708e5155a
Commit: b4a99ee7df1b06c10d25b9b19b430773ab1fdd7e
https://github.com/acl2/acl2/commit/b4a99ee7df1b06c10d25b9b19b430773ab1fdd7e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp

Log Message:
-----------
[Remora] Make unary box types optionals in ASTs.

This mirrors a recent change to the Haskell implementation, related to the
proper handling of the desugaring of n-ary boxes to unary ones.


Commit: 9826583245b7bad3933b5d39933daf92924bd0e2
https://github.com/acl2/acl2/commit/9826583245b7bad3933b5d39933daf92924bd0e2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

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

Log Message:
-----------
[Remora] Add desugaring of n-ary boxes.


Commit: e48d78f4620c2906f760a01d9004c0ead6022bcc
https://github.com/acl2/acl2/commit/e48d78f4620c2906f760a01d9004c0ead6022bcc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

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

Log Message:
-----------
[C$] Export more symbols.


Commit: 477cfa18323b7f562aa95be8310eb85a824b71a7
https://github.com/acl2/acl2/commit/477cfa18323b7f562aa95be8310eb85a824b71a7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp

Log Message:
-----------
[STS safety] Pass additional information.

The additional information are the type completions, so that (in an upcoming
commit) we can use that to deepen certain checks.


Commit: f9968a2f079c36296de9486581a8e88033ee58f2
https://github.com/acl2/acl2/commit/f9968a2f079c36296de9486581a8e88033ee58f2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp

Log Message:
-----------
[STS safety] Add a recursion limit to a clique.

In preparation for an extension.


Commit: 0bda1a3a53d111a9af061149359ef83837b06cea
https://github.com/acl2/acl2/commit/0bda1a3a53d111a9af061149359ef83837b06cea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Adapt type checking to desugared boxes.


Commit: 5fa695ad1ea92fc691392889af51165a6cb0f3a8
https://github.com/acl2/acl2/commit/5fa695ad1ea92fc691392889af51165a6cb0f3a8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

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

Log Message:
-----------
[Remora] Slightly simplify some code.


Commit: 12160a9624bf90cd057bce1488c4d5dc5fc0d6ff
https://github.com/acl2/acl2/commit/12160a9624bf90cd057bce1488c4d5dc5fc0d6ff
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/arithmetic-light/mod.lisp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/logext.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp

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


Commit: 68f84dfed2194d03f7cc69263291923bf42f05b6
https://github.com/acl2/acl2/commit/68f84dfed2194d03f7cc69263291923bf42f05b6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp

Log Message:
-----------
[STS safety] Pass validation table.

This is also needed, to look up tagged struct members.


Commit: d9ff6a5c46c3b14fc6cc6c1bad3143cfb508a65e
https://github.com/acl2/acl2/commit/d9ff6a5c46c3b14fc6cc6c1bad3143cfb508a65e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp

Log Message:
-----------
[STS safe] Improve a check.

For cast expressions, improve the 'may refer' check to also look up members
of tagged struct and union types.


Commit: 3d8b5eaa1d6b665c9fec2caa16cfa3701b20a2f8
https://github.com/acl2/acl2/commit/3d8b5eaa1d6b665c9fec2caa16cfa3701b20a2f8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/arithmetic-light/mod.lisp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/logext.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp

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


Compare: https://github.com/acl2/acl2/compare/d3d18802f2c5...3d8b5eaa1d6b

Eric W. Smith

unread,
Jul 27, 2026, 5:23:08 PM (2 days ago) Jul 27
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: e74bbf5daea2de3b1c95c497bd4463af31a4b1c1
https://github.com/acl2/acl2/commit/e74bbf5daea2de3b1c95c497bd4463af31a4b1c1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-21 (Tue, 21 Jul 2026)

Changed paths:
M books/kestrel/arithmetic-light/mod.lisp

Log Message:
-----------
[arithmetic-light] Improve hint.


Commit: 0160eab834466ca15482741553adc66f5325ccf4
https://github.com/acl2/acl2/commit/0160eab834466ca15482741553adc66f5325ccf4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-07-27 (Mon, 27 Jul 2026)

Changed paths:
M books/kestrel/memory/make-memory-region-machinery.lisp

Log Message:
-----------
[memory] Speed up book.

Without any local events, nothing needs to be rolled back for the local incompatibility check.


Compare: https://github.com/acl2/acl2/compare/353bc6572a32...0ac898a0a60a

Eric W. Smith

unread,
Jul 27, 2026, 5:23:35 PM (2 days ago) Jul 27
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages