[acl2/acl2] 191545: [definductive] Add code to organize predicates in ...

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 191545959e3c0028f27d5c0bc70598ee4ef35ad2
https://github.com/acl2/acl2/commit/191545959e3c0028f27d5c0bc70598ee4ef35ad2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

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

Log Message:
-----------
[definductive] Add code to organize predicates in levels.


Commit: 2084c1ddf23ede096c4306328bb73c0eac898f7c
https://github.com/acl2/acl2/commit/2084c1ddf23ede096c4306328bb73c0eac898f7c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/initializer-validation.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/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/frame-flattening.lisp
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/static-environments.lisp
M books/kestrel/remora/type-value-equivalence.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

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


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

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

Log Message:
-----------
[definductive] Avoid some hints via a library.


Commit: 04ea48098610e95152c0f9430351175ffe0caaa7
https://github.com/acl2/acl2/commit/04ea48098610e95152c0f9430351175ffe0caaa7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

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

Log Message:
-----------
[definductive] Simplify some code.


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

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

Log Message:
-----------
[definductive] Generalize some code.


Commit: 4f9e120fe254bca283bfd24ec3f1f38549ebed0a
https://github.com/acl2/acl2/commit/4f9e120fe254bca283bfd24ec3f1f38549ebed0a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

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

Log Message:
-----------
[definductive] Generalize calculation of cliques.

Also create singleton cliques for non-mutually-recursive predicates.


Commit: 8ce3b3991c04b152091cb9788444e550ebe1311c
https://github.com/acl2/acl2/commit/8ce3b3991c04b152091cb9788444e550ebe1311c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)

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

Log Message:
-----------
[FTY] Generate more theorems.


Commit: dcb4f65d31a6a20caee4506990eb59a79b85f18b
https://github.com/acl2/acl2/commit/dcb4f65d31a6a20caee4506990eb59a79b85f18b
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] Add code to order cliques.


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

Changed paths:
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/grammar.abnf
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/type-values-and-environments.lisp

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


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

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

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


Commit: 9f08c745ff79e785eacf0353bc471fe9d0d65565
https://github.com/acl2/acl2/commit/9f08c745ff79e785eacf0353bc471fe9d0d65565
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] Rework some proofs slightly.


Commit: 0d0eff7aca6445615d8cb12d81aaec71f5999afb
https://github.com/acl2/acl2/commit/0d0eff7aca6445615d8cb12d81aaec71f5999afb
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] Generalize some code.


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

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

Log Message:
-----------
[FTY] Add a fixtype of lists of sets.


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

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

Log Message:
-----------
[FTY] Add some theorems.


Commit: ba71013680c782d5b806ace4f6490811ce2de962
https://github.com/acl2/acl2/commit/ba71013680c782d5b806ace4f6490811ce2de962
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] Use more general code.


Commit: 18fbc3e9580973784491f75eb7b62baa8f25db99
https://github.com/acl2/acl2/commit/18fbc3e9580973784491f75eb7b62baa8f25db99
Author: Matt Kaufmann <matthew.j...@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/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/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/system/doc/acl2-doc.lisp
M books/system/update-state.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Fixed the definition of the writeable-files field of state, which was causing (state-p1 *default-state*) to be false after yesterday's bug fix.

Quoting :DOC note-8-8, where only the "Moreover" part is new:

Fixed a soundness bug in the macro channel-to-string, which is used
in functions like [fms-to-string] (see [printing-to-strings]).
Thanks to Grant Jurgensen for reporting this bug and providing a
helpful analysis of it. The fix is to the constant
*default-state*. In particular, the following is no longer
provable by ACL2.

(equal (car (open-output-channel :string :character *default-state*))
nil)

Moreover, our fix required modifying several functions related to
I/O, often to add an output-p argument that is true when
considering output (which allows for a channel of type :character
with ``filename'' :string) but false when considering input.
Thanks to Aakash Koneru for pointing us in the direction of these
changes.

Passed "make proofs" and "make devel-check" in addition to the usual
"make regression-everything".


Commit: 5a8f2fef5dd89055d4ac25c4d9b5f78371e3279b
https://github.com/acl2/acl2/commit/5a8f2fef5dd89055d4ac25c4d9b5f78371e3279b
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] Add code for ordered leveled cliques.


Commit: 8702fc0f0fa4827f8c0fad990e4bd17f1eda1b14
https://github.com/acl2/acl2/commit/8702fc0f0fa4827f8c0fad990e4bd17f1eda1b14
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] Generalize more code.


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

Changed paths:
M axioms.lisp
M books/demos/brr-free-variables-log.txt
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/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/system/doc/acl2-doc.lisp
M books/system/update-state.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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


Compare: https://github.com/acl2/acl2/compare/ee340914c66f...dccf8aee3d73

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

[Alessandro Coglio]

Branch: refs/heads/master

Commit: d3d18802f2c5f837a70135a415c56db73a72b28f
https://github.com/acl2/acl2/commit/d3d18802f2c5f837a70135a415c56db73a72b28f

Author: Alessandro Coglio <em...@alessandrocoglio.info>
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
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt

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


Compare: https://github.com/acl2/acl2/compare/7d2ed67b4a94...d3d18802f2c5

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

Commit: 18fbc3e9580973784491f75eb7b62baa8f25db99
https://github.com/acl2/acl2/commit/18fbc3e9580973784491f75eb7b62baa8f25db99
Author: Matt Kaufmann <matthew.j...@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/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/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/system/doc/acl2-doc.lisp
M books/system/update-state.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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

Fixed the definition of the writeable-files field of state, which was causing (state-p1 *default-state*) to be false after yesterday's bug fix.

Quoting :DOC note-8-8, where only the "Moreover" part is new:

Fixed a soundness bug in the macro channel-to-string, which is used
in functions like [fms-to-string] (see [printing-to-strings]).
Thanks to Grant Jurgensen for reporting this bug and providing a
helpful analysis of it. The fix is to the constant
*default-state*. In particular, the following is no longer
provable by ACL2.

(equal (car (open-output-channel :string :character *default-state*))
nil)

Moreover, our fix required modifying several functions related to
I/O, often to add an output-p argument that is true when
considering output (which allows for a channel of type :character
with ``filename'' :string) but false when considering input.
Thanks to Aakash Koneru for pointing us in the direction of these
changes.

Passed "make proofs" and "make devel-check" in addition to the usual
"make regression-everything".

Commit: 1ec2dac601ef8b6ef0ca8852085d402bc8ad38bd
https://github.com/acl2/acl2/commit/1ec2dac601ef8b6ef0ca8852085d402bc8ad38bd
Author: Matt Kaufmann <kauf...@cs.utexas.edu>

Date: 2026-07-26 (Sun, 26 Jul 2026)

Changed paths:

M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt

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

Clarified in :DOC defttag that there is at most one active ttag at a time.

Thanks to Eric Smith for suggestion that such a clarification could be
useful.


Commit: 7d2ed67b4a94b6ab03cceff63171aae7dff75b96
https://github.com/acl2/acl2/commit/7d2ed67b4a94b6ab03cceff63171aae7dff75b96
Author: ACL2 Build Server <acl2bui...@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

Log Message:
-----------
Merge commit '6d7422df898c77731011eb5bb96c7476a539acf6' into HEAD

Commit: d3d18802f2c5f837a70135a415c56db73a72b28f
https://github.com/acl2/acl2/commit/d3d18802f2c5f837a70135a415c56db73a72b28f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
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
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt

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.


Compare: https://github.com/acl2/acl2/compare/6d7422df898c...bc5fb9635891