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: 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
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