[acl2/acl2] 8fd82b: [definductive] Improve some generated formulas.
0 views
Skip to first unread message
Alessandro Coglio
Jul 23, 2026, 2:40:18 AM (7 days ago) Jul 23
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 8fd82b37e22932ccd704c1ba249bf578aa10596c
https://github.com/acl2/acl2/commit/8fd82b37e22932ccd704c1ba249bf578aa10596c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-20 (Mon, 20 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve some generated formulas.
Avoid trivial `(implies (and) P)` in favor of just `P`.
Commit: 1921e6302b1eb888c37be9d093e1736d626e9c2b
https://github.com/acl2/acl2/commit/1921e6302b1eb888c37be9d093e1736d626e9c2b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize some code.
Add code that will be used when we lift the restriction to one predicate.
Commit: 03d26c0e40925a832710f4019e4999427cc10834
https://github.com/acl2/acl2/commit/03d26c0e40925a832710f4019e4999427cc10834
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M Makefile
M axioms.lisp
M books/Makefile
M books/kestrel/arithmetic-light/divide.lisp
M books/kestrel/arithmetic-light/expt.lisp
M books/kestrel/arithmetic-light/floor-mod-expt.lisp
M books/kestrel/arithmetic-light/minus.lisp
M books/kestrel/arithmetic-light/numerator.lisp
M books/kestrel/axe/make-axe-rules.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/bv/bvdiv.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/c/atc/support/def-array-support-tests.lisp
M books/kestrel/c/atc/support/def-array-support.lisp
M books/kestrel/c/atc/support/schar.lisp
M books/kestrel/c/atc/support/sint.lisp
M books/kestrel/c/atc/support/sllong.lisp
M books/kestrel/c/atc/support/slong.lisp
M books/kestrel/c/atc/support/sshort.lisp
M books/kestrel/c/atc/support/top.lisp
M books/kestrel/c/atc/support/uchar.lisp
M books/kestrel/c/atc/support/uint.lisp
M books/kestrel/c/atc/support/ullong.lisp
M books/kestrel/c/atc/support/ulong.lisp
M books/kestrel/c/atc/support/ushort.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/lists-light/all-equal-dollar.lisp
M books/kestrel/lists-light/all-same.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
R books/kestrel/remora/primitive-operation-values.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/kestrel/terms-light/count-ifs-in-term.lisp
M books/kestrel/terms-light/expand-lambdas-in-term-proofs.lisp
M books/kestrel/terms-light/expand-lambdas-in-term.lisp
R books/kestrel/terms-light/make-if-term-proof.lisp
A books/kestrel/terms-light/make-if-term-proofs.lisp
M books/kestrel/terms-light/sublis-var-simple-proofs.lisp
M books/kestrel/terms-light/top.lisp
A books/kestrel/terms-light/wrap-pattern-around-term-proofs.lisp
M books/kestrel/terms-light/wrap-pattern-around-term.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: b3d3264d377ec3732b8adc5b3f3921dea5f494d5
https://github.com/acl2/acl2/commit/b3d3264d377ec3732b8adc5b3f3921dea5f494d5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
A books/kestrel/fty/symbol-set-set.lisp
M books/kestrel/fty/top.lisp
Log Message:
-----------
[FTY] Add fixtype of sets of sets of symbols.
Commit: bd294f2f3b0f2a474934aebe87600f0e50fa8042
https://github.com/acl2/acl2/commit/bd294f2f3b0f2a474934aebe87600f0e50fa8042
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[Remora] Strengthen a return type.
Commit: ab089a83f8419c6c9f1e4cd25e21a67ad644d28c
https://github.com/acl2/acl2/commit/ab089a83f8419c6c9f1e4cd25e21a67ad644d28c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/bound-and-free-variable-operations.lisp
M books/kestrel/remora/evaluation.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/type-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
Log Message:
-----------
[Remora] Rename fixtype summand.
Commit: dfc60f80c88dadf52cc19fcbff68a96aef04e088
https://github.com/acl2/acl2/commit/dfc60f80c88dadf52cc19fcbff68a96aef04e088
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.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/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:
-----------
[Remora] Add unary `:sigma`.
For both types and type values.
Commit: 4e33542ac1702376b401bc7c4ff60e8434a8d916
https://github.com/acl2/acl2/commit/4e33542ac1702376b401bc7c4ff60e8434a8d916
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/syntax-abstraction.lisp
Log Message:
-----------
[Remora] Direct CST-to-AST to `:sigma`.
Commit: b3ef3203c53d154f7eed0da5fb5cb13f3b5070f0
https://github.com/acl2/acl2/commit/b3ef3203c53d154f7eed0da5fb5cb13f3b5070f0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add some inference rules.
Commit: c7fb62f2ea9c5f86da1254a0abcc97a93f0a05ce
https://github.com/acl2/acl2/commit/c7fb62f2ea9c5f86da1254a0abcc97a93f0a05ce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve some code.
Avoid artificial argument to ensure termination.
Commit: 19e30be80189c02f86310b77b927757dd4ae04f7
https://github.com/acl2/acl2/commit/19e30be80189c02f86310b77b927757dd4ae04f7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Simplify some lemmas.
Commit: 6e0bcfcfac2e79b94241ad2d641896b493ccf65a
https://github.com/acl2/acl2/commit/6e0bcfcfac2e79b94241ad2d641896b493ccf65a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
Log Message:
-----------
[Remora] Unarize box values.
Commit: c624f2c23dc46fe150839962de68f6d1406e6774
https://github.com/acl2/acl2/commit/c624f2c23dc46fe150839962de68f6d1406e6774
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Simplify some hints.
Commit: 06ba23db766b429c3d2951a7051ee5fd6f5f7f7e
https://github.com/acl2/acl2/commit/06ba23db766b429c3d2951a7051ee5fd6f5f7f7e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Simplify some hints.
Commit: 0c8dc0c942817c229735f763338297c132192131
https://github.com/acl2/acl2/commit/0c8dc0c942817c229735f763338297c132192131
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/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/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:
-----------
[Remora] Rename an AST summand.
Commit: 81088937bcf24d983a2b9d00d44ded429aba36ae
https://github.com/acl2/acl2/commit/81088937bcf24d983a2b9d00d44ded429aba36ae
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve some variable names.
Commit: 4d8c37b31f80ec1057ba34968018c302583b2b21
https://github.com/acl2/acl2/commit/4d8c37b31f80ec1057ba34968018c302583b2b21
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Simplify some names and nomenclature.
Commit: 867552704019f6829a9d3160d6ce6b65b72d6e40
https://github.com/acl2/acl2/commit/867552704019f6829a9d3160d6ce6b65b72d6e40
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Terminological tweaks.
Commit: 28035c72f574e73525948b3d32401eb55b5fef3b
https://github.com/acl2/acl2/commit/28035c72f574e73525948b3d32401eb55b5fef3b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/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
Log Message:
-----------
Merge.
Commit: 088bccf586f0e1e823e2b98f714f65ededc05a52
https://github.com/acl2/acl2/commit/088bccf586f0e1e823e2b98f714f65ededc05a52
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M axioms.lisp
M books/kestrel/c/atc/support/top.lisp
R books/kestrel/memory/acl2-customization.lsp
A books/kestrel/memory/make-memory-region-machinery.acl2
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
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/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: 071179a349d412e83d4a44b496956f8941f6eec5
https://github.com/acl2/acl2/commit/071179a349d412e83d4a44b496956f8941f6eec5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Merge.
Commit: 79c51f9a45dfc14b70a6b2b39a97b22615487d05
https://github.com/acl2/acl2/commit/79c51f9a45dfc14b70a6b2b39a97b22615487d05
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/94bdb5fdd751...79c51f9a45df
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 8fd82b37e22932ccd704c1ba249bf578aa10596c
https://github.com/acl2/acl2/commit/8fd82b37e22932ccd704c1ba249bf578aa10596c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-20 (Mon, 20 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve some generated formulas.
Avoid trivial `(implies (and) P)` in favor of just `P`.
Commit: 1921e6302b1eb888c37be9d093e1736d626e9c2b
https://github.com/acl2/acl2/commit/1921e6302b1eb888c37be9d093e1736d626e9c2b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize some code.
Add code that will be used when we lift the restriction to one predicate.
Commit: 03d26c0e40925a832710f4019e4999427cc10834
https://github.com/acl2/acl2/commit/03d26c0e40925a832710f4019e4999427cc10834
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M Makefile
M axioms.lisp
M books/Makefile
M books/kestrel/arithmetic-light/divide.lisp
M books/kestrel/arithmetic-light/expt.lisp
M books/kestrel/arithmetic-light/floor-mod-expt.lisp
M books/kestrel/arithmetic-light/minus.lisp
M books/kestrel/arithmetic-light/numerator.lisp
M books/kestrel/axe/make-axe-rules.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/bv/bvdiv.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/c/atc/support/def-array-support-tests.lisp
M books/kestrel/c/atc/support/def-array-support.lisp
M books/kestrel/c/atc/support/schar.lisp
M books/kestrel/c/atc/support/sint.lisp
M books/kestrel/c/atc/support/sllong.lisp
M books/kestrel/c/atc/support/slong.lisp
M books/kestrel/c/atc/support/sshort.lisp
M books/kestrel/c/atc/support/top.lisp
M books/kestrel/c/atc/support/uchar.lisp
M books/kestrel/c/atc/support/uint.lisp
M books/kestrel/c/atc/support/ullong.lisp
M books/kestrel/c/atc/support/ulong.lisp
M books/kestrel/c/atc/support/ushort.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/lists-light/all-equal-dollar.lisp
M books/kestrel/lists-light/all-same.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
R books/kestrel/remora/primitive-operation-values.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/kestrel/terms-light/count-ifs-in-term.lisp
M books/kestrel/terms-light/expand-lambdas-in-term-proofs.lisp
M books/kestrel/terms-light/expand-lambdas-in-term.lisp
R books/kestrel/terms-light/make-if-term-proof.lisp
A books/kestrel/terms-light/make-if-term-proofs.lisp
M books/kestrel/terms-light/sublis-var-simple-proofs.lisp
M books/kestrel/terms-light/top.lisp
A books/kestrel/terms-light/wrap-pattern-around-term-proofs.lisp
M books/kestrel/terms-light/wrap-pattern-around-term.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: b3d3264d377ec3732b8adc5b3f3921dea5f494d5
https://github.com/acl2/acl2/commit/b3d3264d377ec3732b8adc5b3f3921dea5f494d5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
A books/kestrel/fty/symbol-set-set.lisp
M books/kestrel/fty/top.lisp
Log Message:
-----------
[FTY] Add fixtype of sets of sets of symbols.
Commit: bd294f2f3b0f2a474934aebe87600f0e50fa8042
https://github.com/acl2/acl2/commit/bd294f2f3b0f2a474934aebe87600f0e50fa8042
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[Remora] Strengthen a return type.
Commit: ab089a83f8419c6c9f1e4cd25e21a67ad644d28c
https://github.com/acl2/acl2/commit/ab089a83f8419c6c9f1e4cd25e21a67ad644d28c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/bound-and-free-variable-operations.lisp
M books/kestrel/remora/evaluation.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/type-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
Log Message:
-----------
[Remora] Rename fixtype summand.
Commit: dfc60f80c88dadf52cc19fcbff68a96aef04e088
https://github.com/acl2/acl2/commit/dfc60f80c88dadf52cc19fcbff68a96aef04e088
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/renaming-evaluation.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/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:
-----------
[Remora] Add unary `:sigma`.
For both types and type values.
Commit: 4e33542ac1702376b401bc7c4ff60e8434a8d916
https://github.com/acl2/acl2/commit/4e33542ac1702376b401bc7c4ff60e8434a8d916
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/syntax-abstraction.lisp
Log Message:
-----------
[Remora] Direct CST-to-AST to `:sigma`.
Commit: b3ef3203c53d154f7eed0da5fb5cb13f3b5070f0
https://github.com/acl2/acl2/commit/b3ef3203c53d154f7eed0da5fb5cb13f3b5070f0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add some inference rules.
Commit: c7fb62f2ea9c5f86da1254a0abcc97a93f0a05ce
https://github.com/acl2/acl2/commit/c7fb62f2ea9c5f86da1254a0abcc97a93f0a05ce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve some code.
Avoid artificial argument to ensure termination.
Commit: 19e30be80189c02f86310b77b927757dd4ae04f7
https://github.com/acl2/acl2/commit/19e30be80189c02f86310b77b927757dd4ae04f7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Simplify some lemmas.
Commit: 6e0bcfcfac2e79b94241ad2d641896b493ccf65a
https://github.com/acl2/acl2/commit/6e0bcfcfac2e79b94241ad2d641896b493ccf65a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
Log Message:
-----------
[Remora] Unarize box values.
Commit: c624f2c23dc46fe150839962de68f6d1406e6774
https://github.com/acl2/acl2/commit/c624f2c23dc46fe150839962de68f6d1406e6774
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Simplify some hints.
Commit: 06ba23db766b429c3d2951a7051ee5fd6f5f7f7e
https://github.com/acl2/acl2/commit/06ba23db766b429c3d2951a7051ee5fd6f5f7f7e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Simplify some hints.
Commit: 0c8dc0c942817c229735f763338297c132192131
https://github.com/acl2/acl2/commit/0c8dc0c942817c229735f763338297c132192131
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/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/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:
-----------
[Remora] Rename an AST summand.
Commit: 81088937bcf24d983a2b9d00d44ded429aba36ae
https://github.com/acl2/acl2/commit/81088937bcf24d983a2b9d00d44ded429aba36ae
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve some variable names.
Commit: 4d8c37b31f80ec1057ba34968018c302583b2b21
https://github.com/acl2/acl2/commit/4d8c37b31f80ec1057ba34968018c302583b2b21
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Simplify some names and nomenclature.
Commit: 867552704019f6829a9d3160d6ce6b65b72d6e40
https://github.com/acl2/acl2/commit/867552704019f6829a9d3160d6ce6b65b72d6e40
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Terminological tweaks.
Commit: 28035c72f574e73525948b3d32401eb55b5fef3b
https://github.com/acl2/acl2/commit/28035c72f574e73525948b3d32401eb55b5fef3b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/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
Log Message:
-----------
Merge.
Commit: 088bccf586f0e1e823e2b98f714f65ededc05a52
https://github.com/acl2/acl2/commit/088bccf586f0e1e823e2b98f714f65ededc05a52
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M axioms.lisp
M books/kestrel/c/atc/support/top.lisp
R books/kestrel/memory/acl2-customization.lsp
A books/kestrel/memory/make-memory-region-machinery.acl2
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
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/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: 071179a349d412e83d4a44b496956f8941f6eec5
https://github.com/acl2/acl2/commit/071179a349d412e83d4a44b496956f8941f6eec5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Merge.
Commit: 79c51f9a45dfc14b70a6b2b39a97b22615487d05
https://github.com/acl2/acl2/commit/79c51f9a45dfc14b70a6b2b39a97b22615487d05
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/94bdb5fdd751...79c51f9a45df
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Jul 23, 2026, 2:40:40 AM (7 days ago) Jul 23
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Jul 25, 2026, 8:30:44 PM (4 days ago) Jul 25
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: efb8f939fd89113603f62d9e89652d18c35f39aa
https://github.com/acl2/acl2/commit/efb8f939fd89113603f62d9e89652d18c35f39aa
Author: Matt Kaufmann <matthew.j...@gmail.com>
Quoting :DOC note-8-8:
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)
Commit: 94bdb5fdd75190378e89a4d633569a109f93e1e7
https://github.com/acl2/acl2/commit/94bdb5fdd75190378e89a4d633569a109f93e1e7
Author: Matt Kaufmann <matthew.j...@gmail.com>
Commit: 79c51f9a45dfc14b70a6b2b39a97b22615487d05
https://github.com/acl2/acl2/commit/79c51f9a45dfc14b70a6b2b39a97b22615487d05
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
Log Message:
-----------
Merge.
Commit: 9287628bf308605b0949c3692284311cf56b6c90
https://github.com/acl2/acl2/commit/9287628bf308605b0949c3692284311cf56b6c90
Commit: 5ed458b8ec9b5c079f9bc7f4e0dfb96705d527b5
https://github.com/acl2/acl2/commit/5ed458b8ec9b5c079f9bc7f4e0dfb96705d527b5
Commit: 844e1723997865adba8eb5dbcc2587948d22f4fd
https://github.com/acl2/acl2/commit/844e1723997865adba8eb5dbcc2587948d22f4fd
Commit: 3dc91b941a0aa295bb1f494d8bccb5b4e1c9a3f8
https://github.com/acl2/acl2/commit/3dc91b941a0aa295bb1f494d8bccb5b4e1c9a3f8
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
Log Message:
-----------
[arithmetic-light] Tweaks to maybe help acl2(r).
Commit: c9adf569d8b0610212063fb851b07033529927cd
https://github.com/acl2/acl2/commit/c9adf569d8b0610212063fb851b07033529927cd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
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
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/dimension-equivalence-infrules.lisp
https://github.com/acl2/acl2/commit/b32552adabf923c8f3ae7d2323ecd54e5fea54f2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
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/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/parser-tests.lisp
https://github.com/acl2/acl2/commit/dad332a67e8a2c12aadd369f2f8196ffe6ef8bd5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
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/evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
Log Message:
-----------
[Remora] Add unary AST.
Commit: 8a0cc39fbed986521646ec822075130767dfb5a4
https://github.com/acl2/acl2/commit/8a0cc39fbed986521646ec822075130767dfb5a4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/parser-tests.lisp
Commit: 032736f467b4d411a480b842c816bc2877200753
https://github.com/acl2/acl2/commit/032736f467b4d411a480b842c816bc2877200753
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
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-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-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
Log Message:
-----------
Support arrays in struct-type-split
Split array objects and members while preserving bounds and initializer extents. Reject unsupported flexible members and effectful duplication, with regression tests and updated documentation.
Commit: 89ee3cb279003164c4de43c8ce7fee8f8179ae47
https://github.com/acl2/acl2/commit/89ee3cb279003164c4de43c8ce7fee8f8179ae47
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/type-checking.lisp
Commit: 9fddefde9c95c7a91296f460e7dc3c2000d4119a
https://github.com/acl2/acl2/commit/9fddefde9c95c7a91296f460e7dc3c2000d4119a
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/array-member.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
Log Message:
-----------
[C2C] Fix struct-type-split array member designators
Commit: 52897737de706ba2f4b3092c25074c2db1846ce0
https://github.com/acl2/acl2/commit/52897737de706ba2f4b3092c25074c2db1846ce0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/type-values-and-environments.lisp
Commit: 7197c0fad412255db3660d1fd094ffb13a56ee89
https://github.com/acl2/acl2/commit/7197c0fad412255db3660d1fd094ffb13a56ee89
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Speed up some proofs.
Commit: 0c35c0cc37044f552c8b01b623ce07b1f42e8688
https://github.com/acl2/acl2/commit/0c35c0cc37044f552c8b01b623ce07b1f42e8688
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
Commit: 02bd16760af9153aeaf9612ff09144f27249f77f
https://github.com/acl2/acl2/commit/02bd16760af9153aeaf9612ff09144f27249f77f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/arithmetic.lisp
Log Message:
-----------
[Remora] Add some doc.
Commit: 105a069ac6d37d008fa8fdf87bdb197d8c838596
https://github.com/acl2/acl2/commit/105a069ac6d37d008fa8fdf87bdb197d8c838596
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/library-extensions.lisp
Log Message:
-----------
[Remora] Swap some topic order.
Commit: c98a080cb0461d0235d5813a776cc89d0a3638f3
https://github.com/acl2/acl2/commit/c98a080cb0461d0235d5813a776cc89d0a3638f3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/library-extensions.lisp
A books/kestrel/remora/omaps.lisp
R books/kestrel/remora/oset-omaps.lisp
A books/kestrel/remora/osets.lisp
M books/kestrel/remora/renaming-evaluation.lisp
Log Message:
-----------
[Remora] Refactor oset and omap library extensions.
Commit: 6db99906de7e1a49aeca5bd4a2c3837b996ebdd8
https://github.com/acl2/acl2/commit/6db99906de7e1a49aeca5bd4a2c3837b996ebdd8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Fix bug in printer.
An opening square bracket was omitted in certain declarators.
Thanks to Grant Jurgensen for finding and reporting the issue.
Commit: baa3c2704341921534ea95c3343aadcc00ef60da
https://github.com/acl2/acl2/commit/baa3c2704341921534ea95c3343aadcc00ef60da
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
Merge.
Commit: 9a194a958eba137e88e0bb2cd8012f386ae114bb
https://github.com/acl2/acl2/commit/9a194a958eba137e88e0bb2cd8012f386ae114bb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
Log Message:
-----------
[Remora] Update and improve AST doc.
Commit: 0995b9f453977b810edb7629cc0b76b51066be7a
https://github.com/acl2/acl2/commit/0995b9f453977b810edb7629cc0b76b51066be7a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
Log Message:
-----------
[Remora] Improve some doc.
Commit: 778a395d7c878e5563b7fa169f7f2d87d9f7b374
https://github.com/acl2/acl2/commit/778a395d7c878e5563b7fa169f7f2d87d9f7b374
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
Log Message:
-----------
[Remora] Update some doc.
Commit: 2e897fcc92be0311e93835a03db58cc684015077
https://github.com/acl2/acl2/commit/2e897fcc92be0311e93835a03db58cc684015077
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-equivalence.lisp
Log Message:
-----------
[Remora] Tweak syntax abstraction for function types.
Commit: 5a90cd5b7b2346aea88f3102556f5f477425e257
https://github.com/acl2/acl2/commit/5a90cd5b7b2346aea88f3102556f5f477425e257
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
Log Message:
-----------
[Remora] Document a requirement.
Commit: 4251a3a7f4cdf92f559618bee653cb66d9aff2f6
https://github.com/acl2/acl2/commit/4251a3a7f4cdf92f559618bee653cb66d9aff2f6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
Log Message:
-----------
[Remora] Document another AST restriction.
Commit: 84ed3a38c0685a359b753ae46fe4596a855d2363
https://github.com/acl2/acl2/commit/84ed3a38c0685a359b753ae46fe4596a855d2363
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formed.lisp
Log Message:
-----------
[Remora] Tighten some code.
Commit: 92245bb7f223eee0a5d41a4db794c52757322860
https://github.com/acl2/acl2/commit/92245bb7f223eee0a5d41a4db794c52757322860
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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-initializers.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
Log Message:
-----------
[C2C] Extend struct-type-split array tests
Commit: a5cd31e9541d0b4d06f8ef389cd6c86d8ecc2564
https://github.com/acl2/acl2/commit/a5cd31e9541d0b4d06f8ef389cd6c86d8ecc2564
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp
Log Message:
-----------
[C2C] Correct struct-type-split documentation
Commit: 89d84f5401d80471a4cc8e83ba9ac6b86959c24e
https://github.com/acl2/acl2/commit/89d84f5401d80471a4cc8e83ba9ac6b86959c24e
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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
Log Message:
-----------
Merge branch 'gj-struct-type-split' into testing-kestrel
Commit: 4d16d0e8c707f747914403cd684911ca727cbd7c
https://github.com/acl2/acl2/commit/4d16d0e8c707f747914403cd684911ca727cbd7c
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp
Log Message:
-----------
[C2C] Update struct-type-split limitations documentation
Commit: 4e51300e429eda9341d7c0b7e12e30bceb9523a9
https://github.com/acl2/acl2/commit/4e51300e429eda9341d7c0b7e12e30bceb9523a9
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/lists.lisp
-----------
[REMORA] added reshape
Commit: c3c29fbf6a9de69d8567d323f21a699fe07634ec
https://github.com/acl2/acl2/commit/c3c29fbf6a9de69d8567d323f21a699fe07634ec
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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/primitives-evaluation.lisp
M books/kestrel/remora/type-value-equivalence.lisp
Because the latter are more "basic", and we may need to use them to define some
upcoming extensions of the core predicates.
Commit: 2eef47833fdb36d29a5e64f7e1387f3bd19ff60f
https://github.com/acl2/acl2/commit/2eef47833fdb36d29a5e64f7e1387f3bd19ff60f
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Allow a non-recursive single predicate.
When a single predicate is defined, drop the requirement that it be
recursive: it then yields a non-recursive proof validity function,
generated without a measure or induction hints, and its minimality
theorem is proved by a direct case analysis on the proof kind rather
than by induction. Multiple predicates must still be mutually
recursive (form a single clique).
Commit: 93e8670392ad6d7c9deef44e04f101609453c383
https://github.com/acl2/acl2/commit/93e8670392ad6d7c9deef44e04f101609453c383
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Incorporate AC's feedback
Added authorship to headers and move auxillary function short to main
documentation.
Commit: 8307006706449d473ced4e08d02461e5e4d8c418
https://github.com/acl2/acl2/commit/8307006706449d473ced4e08d02461e5e4d8c418
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Add some structural ops.
Commit: ef807a1e1d2e61b51404bf2641d8025cb4747745
https://github.com/acl2/acl2/commit/ef807a1e1d2e61b51404bf2641d8025cb4747745
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add a theorem.
Commit: b86fa357fdabf6dc7fc51cb6ffb4f9c1917f738f
https://github.com/acl2/acl2/commit/b86fa357fdabf6dc7fc51cb6ffb4f9c1917f738f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Redirect desugaring away from n-ary function types.
Commit: 44404497126a27b50da898846e0904927021fe76
https://github.com/acl2/acl2/commit/44404497126a27b50da898846e0904927021fe76
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
Log Message:
-----------
[C$] Annotate inferred array designators
Commit: c7d6700ea5d668158aadb33662f9a74a773c6626
https://github.com/acl2/acl2/commit/c7d6700ea5d668158aadb33662f9a74a773c6626
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Desugar n-ary function types.
Commit: df32bef251b0e613275db80098305cf1a8bba62f
https://github.com/acl2/acl2/commit/df32bef251b0e613275db80098305cf1a8bba62f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add a theorem.
Commit: 6baf67f679d2e71f2bf4ae25bf16b16aeaa91ce7
https://github.com/acl2/acl2/commit/6baf67f679d2e71f2bf4ae25bf16b16aeaa91ce7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Direct desugaring away from n-ary universal types.
Commit: 8bc75130006b5a9c43f45e60d411634e6e0f7773
https://github.com/acl2/acl2/commit/8bc75130006b5a9c43f45e60d411634e6e0f7773
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add two theorems.
Commit: 6c7ff33d7974601fda257dfce4da6974f07ed915
https://github.com/acl2/acl2/commit/6c7ff33d7974601fda257dfce4da6974f07ed915
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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:
-----------
projects/fields/ updates
Commit: 391a8916372f0dec9a96fa8c9be075144b06376c
https://github.com/acl2/acl2/commit/391a8916372f0dec9a96fa8c9be075144b06376c
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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
Log Message:
-----------
merge
Commit: 765089ccbd03ec84600fa00801ea0382e29a1d55
https://github.com/acl2/acl2/commit/765089ccbd03ec84600fa00801ea0382e29a1d55
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Merge commit '93e8670392ad6d7c9deef44e04f101609453c383' into HEAD
Commit: ebafd700f7360be021b637237334d0378239f65f
https://github.com/acl2/acl2/commit/ebafd700f7360be021b637237334d0378239f65f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Desugar n-ary universal, product, and sum types.
Commit: a3d4d4dbeb5c8bf885197a30fea29a6edd4582a5
https://github.com/acl2/acl2/commit/a3d4d4dbeb5c8bf885197a30fea29a6edd4582a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Add some structural ops.
Commit: c5903196d17e52edbd2aa61df06ea63a4e0ca4b2
https://github.com/acl2/acl2/commit/c5903196d17e52edbd2aa61df06ea63a4e0ca4b2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: 041ff6870c6029952f4dd58ee47063db8eae5422
https://github.com/acl2/acl2/commit/041ff6870c6029952f4dd58ee47063db8eae5422
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Avoid n-ary applications in desugaring.
Commit: bf0f11d45ced0c359cd9e9348ba8f38910edc709
https://github.com/acl2/acl2/commit/bf0f11d45ced0c359cd9e9348ba8f38910edc709
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Desugar n-ary applications.
Commit: e10fc1fcad8f9a546c50ffef628eb064e34f02e9
https://github.com/acl2/acl2/commit/e10fc1fcad8f9a546c50ffef628eb064e34f02e9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Add some structural ops.
Commit: f2667797915e038339e2bfa2699a711123aee5bd
https://github.com/acl2/acl2/commit/f2667797915e038339e2bfa2699a711123aee5bd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: d5d984fc1cb3e9acc9f4a5f06b97457b87523a2b
https://github.com/acl2/acl2/commit/d5d984fc1cb3e9acc9f4a5f06b97457b87523a2b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Desugar n-ary lambda abstractions.
Commit: 9411b5691c9a7d4a61ba740ba51216649e450477
https://github.com/acl2/acl2/commit/9411b5691c9a7d4a61ba740ba51216649e450477
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Add a structural op.
Commit: 75dc41d781ef62d1d86e3ddcdcffa2eef65e13e2
https://github.com/acl2/acl2/commit/75dc41d781ef62d1d86e3ddcdcffa2eef65e13e2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: 74346e2b766ad18b3cd931a9373a1688e7c32994
https://github.com/acl2/acl2/commit/74346e2b766ad18b3cd931a9373a1688e7c32994
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Desugar n-ary unboxing.
Commit: 0e5a20e60e608b2bb1a4430d50d4512d6d9ae5b9
https://github.com/acl2/acl2/commit/0e5a20e60e608b2bb1a4430d50d4512d6d9ae5b9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
A books/kestrel/fty/symbol-set-list-list.lisp
A books/kestrel/fty/symbol-set-list.lisp
Commit: d9c4568dcf0f6afc98e51b7cd00fe30f8b675c74
https://github.com/acl2/acl2/commit/d9c4568dcf0f6afc98e51b7cd00fe30f8b675c74
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: c3c3e77eaafa2619c63d41b686291bc3e0de2c4e
https://github.com/acl2/acl2/commit/c3c3e77eaafa2619c63d41b686291bc3e0de2c4e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Simplify some hints.
Commit: cd3d8ccb5b61d8b09cb5dc2e03f8457c92438156
https://github.com/acl2/acl2/commit/cd3d8ccb5b61d8b09cb5dc2e03f8457c92438156
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some predicates.
Commit: 64315dd94fa498152b9ee22c67e3e0c0f002cf95
https://github.com/acl2/acl2/commit/64315dd94fa498152b9ee22c67e3e0c0f002cf95
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Simplify some hints.
Commit: aa08e28029585b351d3320c52bb9d08823d66cb9
https://github.com/acl2/acl2/commit/aa08e28029585b351d3320c52bb9d08823d66cb9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/grammar.abnf
Log Message:
-----------
[Remora] Move a note to a more central position.
Commit: 174e3b504b2f61b12a00880b7ea8ac00a0f40ae2
https://github.com/acl2/acl2/commit/174e3b504b2f61b12a00880b7ea8ac00a0f40ae2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/grammar.abnf
Log Message:
-----------
[Remora] Remove stray blank line.
Commit: c5cc5cc0b0f1dfc042862f9360a31e4582ce73b9
https://github.com/acl2/acl2/commit/c5cc5cc0b0f1dfc042862f9360a31e4582ce73b9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Remove a subsumed theorem.
Commit: 626cc63ae67d16a7f8d168586cde9df56668f060
https://github.com/acl2/acl2/commit/626cc63ae67d16a7f8d168586cde9df56668f060
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some doc.
Commit: 6a464d57c695a911e59ccd6c748fcd04bda09065
https://github.com/acl2/acl2/commit/6a464d57c695a911e59ccd6c748fcd04bda09065
Author: Alessandro Coglio <2409151...@users.noreply.github.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/lists.lisp
-----------
Merge pull request #1988 from ltmquan/remora
[REMORA] added `reshape`
Commit: 4a09c83a8e661cb2d7efca549c1c3e713e29a942
https://github.com/acl2/acl2/commit/4a09c83a8e661cb2d7efca549c1c3e713e29a942
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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
Commit: 982d0b0ce236bdea389bc44f3473bd2321529e23
https://github.com/acl2/acl2/commit/982d0b0ce236bdea389bc44f3473bd2321529e23
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Add a function.
Commit: 7e454027835d45e850af9b409ce77a9bcd1c0a02
https://github.com/acl2/acl2/commit/7e454027835d45e850af9b409ce77a9bcd1c0a02
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Simplify desugaring.
Commit: 6c058e674b27559d9fe019ec67c89beac31a3c8b
https://github.com/acl2/acl2/commit/6c058e674b27559d9fe019ec67c89beac31a3c8b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/lists.lisp
-----------
Merge.
Commit: 4f344831107e8a7e1e10844b77c5a90c8c13bb34
https://github.com/acl2/acl2/commit/4f344831107e8a7e1e10844b77c5a90c8c13bb34
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
A books/kestrel/fty/symbol-set-list-list.lisp
A books/kestrel/fty/symbol-set-list.lisp
M books/kestrel/fty/top.lisp
Commit: 4b184ad520371bfc4c3bb02499898a53f4cc240c
https://github.com/acl2/acl2/commit/4b184ad520371bfc4c3bb02499898a53f4cc240c
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
merge
Commit: 127036a730484d24d097aa2f5b78fa8c4c01f265
https://github.com/acl2/acl2/commit/127036a730484d24d097aa2f5b78fa8c4c01f265
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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: c2b5f1278ac2ced5a7b5679b128807bd01f82ebe
https://github.com/acl2/acl2/commit/c2b5f1278ac2ced5a7b5679b128807bd01f82ebe
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/projects/fields/embeddings.lisp
M books/projects/fields/support/embeddings.lisp
Log Message:
-----------
Defined inverse embedding
Commit: 89d2cf4304c4002efa205c9ed51c453b7b2d4263
https://github.com/acl2/acl2/commit/89d2cf4304c4002efa205c9ed51c453b7b2d4263
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add more inference rules.
Commit: 4f41c9f07359f37071f263ab6dd9d628b3eee524
https://github.com/acl2/acl2/commit/4f41c9f07359f37071f263ab6dd9d628b3eee524
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/lists.lisp
-----------
Merge commit '6a464d57c695a911e59ccd6c748fcd04bda09065' into HEAD
Commit: a20ec9a94780982cc48fc875c447fa3b9b8101d1
https://github.com/acl2/acl2/commit/a20ec9a94780982cc48fc875c447fa3b9b8101d1
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
Log Message:
-----------
“merge”
Commit: 9230f610e8176bef5e8b7519df0a335310b335f9
https://github.com/acl2/acl2/commit/9230f610e8176bef5e8b7519df0a335310b335f9
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/lists.lisp
-----------
“merge”
Commit: 98383ead4d64968fa0e2645c4223257c39d5eff3
https://github.com/acl2/acl2/commit/98383ead4d64968fa0e2645c4223257c39d5eff3
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
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/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/type-value-equivalence.lisp
Log Message:
-----------
Merge commit '127036a730484d24d097aa2f5b78fa8c4c01f265' into HEAD
Commit: b6c31cb88ebf2e41e9d0e7e0bd79b87a8066d16c
https://github.com/acl2/acl2/commit/b6c31cb88ebf2e41e9d0e7e0bd79b87a8066d16c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.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/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/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
Commit: c0b81f47bf75544e141e04b5802cb7e9882ed5c4
https://github.com/acl2/acl2/commit/c0b81f47bf75544e141e04b5802cb7e9882ed5c4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Improve some doc.
Commit: 01c535f961022c5a01f27331aedf1fb589f498b3
https://github.com/acl2/acl2/commit/01c535f961022c5a01f27331aedf1fb589f498b3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Simplify two inference rules.
Commit: 2cc59f19f45bf2ee2c5f56a9d01fd353bbcb9831
https://github.com/acl2/acl2/commit/2cc59f19f45bf2ee2c5f56a9d01fd353bbcb9831
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add and improve some inference rules.
Commit: 25e80ce781d1704b4cd30cd8a361bdc9f8013fb6
https://github.com/acl2/acl2/commit/25e80ce781d1704b4cd30cd8a361bdc9f8013fb6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add a rule for dimension subtractions.
Commit: c9ca7237aafd1842a6d4e9e00e321a09eea76230
https://github.com/acl2/acl2/commit/c9ca7237aafd1842a6d4e9e00e321a09eea76230
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Fix layout.
Commit: bb08f3c7e07c2641f26ece0c1ce3272cfe124854
https://github.com/acl2/acl2/commit/bb08f3c7e07c2641f26ece0c1ce3272cfe124854
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Fix some code and doc.
Commit: 4584af836f19a05f51c3e6a4d1f46c3160f21f02
https://github.com/acl2/acl2/commit/4584af836f19a05f51c3e6a4d1f46c3160f21f02
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Fix typo in doc.
Commit: 2c0ae2cbae0b3342e1f0a57a76a091d2ec796b72
https://github.com/acl2/acl2/commit/2c0ae2cbae0b3342e1f0a57a76a091d2ec796b72
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add an inference rule.
Commit: e819cef97511be7c96577a12704b1817600df5d8
https://github.com/acl2/acl2/commit/e819cef97511be7c96577a12704b1817600df5d8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add inference rule.
Commit: 19a79469dbf277ff1e9eaef7f7977d977353faf6
https://github.com/acl2/acl2/commit/19a79469dbf277ff1e9eaef7f7977d977353faf6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remore] Remove some redundant inf. rules.
Commit: cf8a4ae1465ed49634b77b72f8eaa54179849c57
https://github.com/acl2/acl2/commit/cf8a4ae1465ed49634b77b72f8eaa54179849c57
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Improve the inf. rules.
Commit: 6df62bcb2c6839f8904b2ce72d58cb12ebc24a1b
https://github.com/acl2/acl2/commit/6df62bcb2c6839f8904b2ce72d58cb12ebc24a1b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Improve dimeq inf rules and their doc.
Compare: https://github.com/acl2/acl2/compare/17eeec0b6f05...6df62bcb2c68
https://github.com/acl2/acl2/commit/efb8f939fd89113603f62d9e89652d18c35f39aa
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M axioms.lisp
Changed paths:
M axioms.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:
-----------
Fixed a soundness bug in the macro channel-to-string.
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
Log Message:
-----------
Quoting :DOC note-8-8:
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)
https://github.com/acl2/acl2/commit/94bdb5fdd75190378e89a4d633569a109f93e1e7
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
Log Message:
-----------
Fixed a typo in :DOC safe-mode.
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
Log Message:
-----------
Commit: 79c51f9a45dfc14b70a6b2b39a97b22615487d05
https://github.com/acl2/acl2/commit/79c51f9a45dfc14b70a6b2b39a97b22615487d05
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/9287628bf308605b0949c3692284311cf56b6c90
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/evaluation.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
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/evaluation.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names.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:
-----------
[Remora] Add unary `:unbox`.
M books/kestrel/remora/unique-names.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:
-----------
Commit: 5ed458b8ec9b5c079f9bc7f4e0dfb96705d527b5
https://github.com/acl2/acl2/commit/5ed458b8ec9b5c079f9bc7f4e0dfb96705d527b5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/syntax-abstraction.lisp
Log Message:
-----------
[Remora] Direct CST-to-AST to unary `:unbox`.
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/syntax-abstraction.lisp
Log Message:
-----------
Commit: 844e1723997865adba8eb5dbcc2587948d22f4fd
https://github.com/acl2/acl2/commit/844e1723997865adba8eb5dbcc2587948d22f4fd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-22 (Wed, 22 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
Date: 2026-07-22 (Wed, 22 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/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] Add unary `:box` AST.
Log Message:
-----------
Commit: 3dc91b941a0aa295bb1f494d8bccb5b4e1c9a3f8
https://github.com/acl2/acl2/commit/3dc91b941a0aa295bb1f494d8bccb5b4e1c9a3f8
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
Log Message:
-----------
[arithmetic-light] Tweaks to maybe help acl2(r).
Commit: c9adf569d8b0610212063fb851b07033529927cd
https://github.com/acl2/acl2/commit/c9adf569d8b0610212063fb851b07033529927cd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
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
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/dimension-equivalence-infrules.lisp
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
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/kestrel/remora/primitives-evaluation-polymorphic-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.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/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: b32552adabf923c8f3ae7d2323ecd54e5fea54f2
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/b32552adabf923c8f3ae7d2323ecd54e5fea54f2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
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/evaluation.lisp
M books/kestrel/remora/parser-tests.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/type-equivalence.lisp
M books/kestrel/remora/values-to-abstract-syntax.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/values-to-abstract-syntax.lisp
Log Message:
-----------
[Remora] Rename an AST summand.
Commit: dad332a67e8a2c12aadd369f2f8196ffe6ef8bd5
-----------
[Remora] Rename an AST summand.
https://github.com/acl2/acl2/commit/dad332a67e8a2c12aadd369f2f8196ffe6ef8bd5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
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/printer.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
Log Message:
-----------
[Remora] Add unary AST.
Commit: 8a0cc39fbed986521646ec822075130767dfb5a4
https://github.com/acl2/acl2/commit/8a0cc39fbed986521646ec822075130767dfb5a4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/syntax-abstraction.lisp
Log Message:
-----------
[Remora] Internally produce unary function types.
Log Message:
-----------
Commit: 032736f467b4d411a480b842c816bc2877200753
https://github.com/acl2/acl2/commit/032736f467b4d411a480b842c816bc2877200753
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
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-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-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
Log Message:
-----------
Support arrays in struct-type-split
Split array objects and members while preserving bounds and initializer extents. Reject unsupported flexible members and effectful duplication, with regression tests and updated documentation.
Commit: 89ee3cb279003164c4de43c8ce7fee8f8179ae47
https://github.com/acl2/acl2/commit/89ee3cb279003164c4de43c8ce7fee8f8179ae47
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
Log Message:
-----------
[Remora] Product more unary function types internally.
Log Message:
-----------
Commit: 9fddefde9c95c7a91296f460e7dc3c2000d4119a
https://github.com/acl2/acl2/commit/9fddefde9c95c7a91296f460e7dc3c2000d4119a
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/array-member.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
Log Message:
-----------
[C2C] Fix struct-type-split array member designators
Commit: 52897737de706ba2f4b3092c25074c2db1846ce0
https://github.com/acl2/acl2/commit/52897737de706ba2f4b3092c25074c2db1846ce0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/renaming-evaluation.lisp
M books/kestrel/remora/type-values-and-environments.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
Log Message:
-----------
[Remora] Make function type values unary.
Log Message:
-----------
Commit: 7197c0fad412255db3660d1fd094ffb13a56ee89
https://github.com/acl2/acl2/commit/7197c0fad412255db3660d1fd094ffb13a56ee89
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
Commit: 0c35c0cc37044f552c8b01b623ce07b1f42e8688
https://github.com/acl2/acl2/commit/0c35c0cc37044f552c8b01b623ce07b1f42e8688
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
Commit: 02bd16760af9153aeaf9612ff09144f27249f77f
https://github.com/acl2/acl2/commit/02bd16760af9153aeaf9612ff09144f27249f77f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/arithmetic.lisp
Log Message:
-----------
[Remora] Add some doc.
Commit: 105a069ac6d37d008fa8fdf87bdb197d8c838596
https://github.com/acl2/acl2/commit/105a069ac6d37d008fa8fdf87bdb197d8c838596
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/library-extensions.lisp
Log Message:
-----------
[Remora] Swap some topic order.
Commit: c98a080cb0461d0235d5813a776cc89d0a3638f3
https://github.com/acl2/acl2/commit/c98a080cb0461d0235d5813a776cc89d0a3638f3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/library-extensions.lisp
A books/kestrel/remora/omaps.lisp
R books/kestrel/remora/oset-omaps.lisp
A books/kestrel/remora/osets.lisp
M books/kestrel/remora/renaming-evaluation.lisp
Log Message:
-----------
[Remora] Refactor oset and omap library extensions.
Commit: 6db99906de7e1a49aeca5bd4a2c3837b996ebdd8
https://github.com/acl2/acl2/commit/6db99906de7e1a49aeca5bd4a2c3837b996ebdd8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Fix bug in printer.
An opening square bracket was omitted in certain declarators.
Thanks to Grant Jurgensen for finding and reporting the issue.
Commit: baa3c2704341921534ea95c3343aadcc00ef60da
https://github.com/acl2/acl2/commit/baa3c2704341921534ea95c3343aadcc00ef60da
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
Merge.
Commit: 9a194a958eba137e88e0bb2cd8012f386ae114bb
https://github.com/acl2/acl2/commit/9a194a958eba137e88e0bb2cd8012f386ae114bb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
Log Message:
-----------
[Remora] Update and improve AST doc.
Commit: 0995b9f453977b810edb7629cc0b76b51066be7a
https://github.com/acl2/acl2/commit/0995b9f453977b810edb7629cc0b76b51066be7a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
Log Message:
-----------
[Remora] Improve some doc.
Commit: 778a395d7c878e5563b7fa169f7f2d87d9f7b374
https://github.com/acl2/acl2/commit/778a395d7c878e5563b7fa169f7f2d87d9f7b374
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
Log Message:
-----------
[Remora] Update some doc.
Commit: 2e897fcc92be0311e93835a03db58cc684015077
https://github.com/acl2/acl2/commit/2e897fcc92be0311e93835a03db58cc684015077
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-equivalence.lisp
Log Message:
-----------
[Remora] Tweak syntax abstraction for function types.
Commit: 5a90cd5b7b2346aea88f3102556f5f477425e257
https://github.com/acl2/acl2/commit/5a90cd5b7b2346aea88f3102556f5f477425e257
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
Log Message:
-----------
[Remora] Document a requirement.
Commit: 4251a3a7f4cdf92f559618bee653cb66d9aff2f6
https://github.com/acl2/acl2/commit/4251a3a7f4cdf92f559618bee653cb66d9aff2f6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
Log Message:
-----------
[Remora] Document another AST restriction.
Commit: 84ed3a38c0685a359b753ae46fe4596a855d2363
https://github.com/acl2/acl2/commit/84ed3a38c0685a359b753ae46fe4596a855d2363
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-23 (Thu, 23 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formed.lisp
Log Message:
-----------
[Remora] Tighten some code.
Commit: 92245bb7f223eee0a5d41a4db794c52757322860
https://github.com/acl2/acl2/commit/92245bb7f223eee0a5d41a4db794c52757322860
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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-initializers.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
Log Message:
-----------
[C2C] Extend struct-type-split array tests
Commit: a5cd31e9541d0b4d06f8ef389cd6c86d8ecc2564
https://github.com/acl2/acl2/commit/a5cd31e9541d0b4d06f8ef389cd6c86d8ecc2564
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp
Log Message:
-----------
[C2C] Correct struct-type-split documentation
Commit: 89d84f5401d80471a4cc8e83ba9ac6b86959c24e
https://github.com/acl2/acl2/commit/89d84f5401d80471a4cc8e83ba9ac6b86959c24e
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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
Log Message:
-----------
Merge branch 'gj-struct-type-split' into testing-kestrel
Commit: 4d16d0e8c707f747914403cd684911ca727cbd7c
https://github.com/acl2/acl2/commit/4d16d0e8c707f747914403cd684911ca727cbd7c
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp
Log Message:
-----------
[C2C] Update struct-type-split limitations documentation
Commit: 4e51300e429eda9341d7c0b7e12e30bceb9523a9
https://github.com/acl2/acl2/commit/4e51300e429eda9341d7c0b7e12e30bceb9523a9
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/expression-values-and-environments.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
Log Message:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
-----------
[REMORA] added reshape
Commit: c3c29fbf6a9de69d8567d323f21a699fe07634ec
https://github.com/acl2/acl2/commit/c3c29fbf6a9de69d8567d323f21a699fe07634ec
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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/primitives-evaluation.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
Log Message:
-----------
[Remora] Refactor core predicates after structurals.
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:
-----------
Because the latter are more "basic", and we may need to use them to define some
upcoming extensions of the core predicates.
Commit: 2eef47833fdb36d29a5e64f7e1387f3bd19ff60f
https://github.com/acl2/acl2/commit/2eef47833fdb36d29a5e64f7e1387f3bd19ff60f
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
When a single predicate is defined, drop the requirement that it be
recursive: it then yields a non-recursive proof validity function,
generated without a measure or induction hints, and its minimality
theorem is proved by a direct case analysis on the proof kind rather
than by induction. Multiple predicates must still be mutually
recursive (form a single clique).
Commit: 93e8670392ad6d7c9deef44e04f101609453c383
https://github.com/acl2/acl2/commit/93e8670392ad6d7c9deef44e04f101609453c383
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Added authorship to headers and move auxillary function short to main
documentation.
Commit: 8307006706449d473ced4e08d02461e5e4d8c418
https://github.com/acl2/acl2/commit/8307006706449d473ced4e08d02461e5e4d8c418
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Add some structural ops.
Commit: ef807a1e1d2e61b51404bf2641d8025cb4747745
https://github.com/acl2/acl2/commit/ef807a1e1d2e61b51404bf2641d8025cb4747745
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add a theorem.
Commit: b86fa357fdabf6dc7fc51cb6ffb4f9c1917f738f
https://github.com/acl2/acl2/commit/b86fa357fdabf6dc7fc51cb6ffb4f9c1917f738f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Redirect desugaring away from n-ary function types.
Commit: 44404497126a27b50da898846e0904927021fe76
https://github.com/acl2/acl2/commit/44404497126a27b50da898846e0904927021fe76
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
Log Message:
-----------
[C$] Annotate inferred array designators
Commit: c7d6700ea5d668158aadb33662f9a74a773c6626
https://github.com/acl2/acl2/commit/c7d6700ea5d668158aadb33662f9a74a773c6626
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Desugar n-ary function types.
Commit: df32bef251b0e613275db80098305cf1a8bba62f
https://github.com/acl2/acl2/commit/df32bef251b0e613275db80098305cf1a8bba62f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add a theorem.
Commit: 6baf67f679d2e71f2bf4ae25bf16b16aeaa91ce7
https://github.com/acl2/acl2/commit/6baf67f679d2e71f2bf4ae25bf16b16aeaa91ce7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Direct desugaring away from n-ary universal types.
Commit: 8bc75130006b5a9c43f45e60d411634e6e0f7773
https://github.com/acl2/acl2/commit/8bc75130006b5a9c43f45e60d411634e6e0f7773
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add two theorems.
Commit: 6c7ff33d7974601fda257dfce4da6974f07ed915
https://github.com/acl2/acl2/commit/6c7ff33d7974601fda257dfce4da6974f07ed915
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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:
-----------
projects/fields/ updates
Commit: 391a8916372f0dec9a96fa8c9be075144b06376c
https://github.com/acl2/acl2/commit/391a8916372f0dec9a96fa8c9be075144b06376c
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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
Log Message:
-----------
merge
Commit: 765089ccbd03ec84600fa00801ea0382e29a1d55
https://github.com/acl2/acl2/commit/765089ccbd03ec84600fa00801ea0382e29a1d55
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Commit: ebafd700f7360be021b637237334d0378239f65f
https://github.com/acl2/acl2/commit/ebafd700f7360be021b637237334d0378239f65f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Desugar n-ary universal, product, and sum types.
Commit: a3d4d4dbeb5c8bf885197a30fea29a6edd4582a5
https://github.com/acl2/acl2/commit/a3d4d4dbeb5c8bf885197a30fea29a6edd4582a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Add some structural ops.
Commit: c5903196d17e52edbd2aa61df06ea63a4e0ca4b2
https://github.com/acl2/acl2/commit/c5903196d17e52edbd2aa61df06ea63a4e0ca4b2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: 041ff6870c6029952f4dd58ee47063db8eae5422
https://github.com/acl2/acl2/commit/041ff6870c6029952f4dd58ee47063db8eae5422
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Avoid n-ary applications in desugaring.
Commit: bf0f11d45ced0c359cd9e9348ba8f38910edc709
https://github.com/acl2/acl2/commit/bf0f11d45ced0c359cd9e9348ba8f38910edc709
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Desugar n-ary applications.
Commit: e10fc1fcad8f9a546c50ffef628eb064e34f02e9
https://github.com/acl2/acl2/commit/e10fc1fcad8f9a546c50ffef628eb064e34f02e9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Add some structural ops.
Commit: f2667797915e038339e2bfa2699a711123aee5bd
https://github.com/acl2/acl2/commit/f2667797915e038339e2bfa2699a711123aee5bd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: d5d984fc1cb3e9acc9f4a5f06b97457b87523a2b
https://github.com/acl2/acl2/commit/d5d984fc1cb3e9acc9f4a5f06b97457b87523a2b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Desugar n-ary lambda abstractions.
Commit: 9411b5691c9a7d4a61ba740ba51216649e450477
https://github.com/acl2/acl2/commit/9411b5691c9a7d4a61ba740ba51216649e450477
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
Log Message:
-----------
[Remora] Add a structural op.
Commit: 75dc41d781ef62d1d86e3ddcdcffa2eef65e13e2
https://github.com/acl2/acl2/commit/75dc41d781ef62d1d86e3ddcdcffa2eef65e13e2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: 74346e2b766ad18b3cd931a9373a1688e7c32994
https://github.com/acl2/acl2/commit/74346e2b766ad18b3cd931a9373a1688e7c32994
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Desugar n-ary unboxing.
Commit: 0e5a20e60e608b2bb1a4430d50d4512d6d9ae5b9
https://github.com/acl2/acl2/commit/0e5a20e60e608b2bb1a4430d50d4512d6d9ae5b9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
A books/kestrel/fty/symbol-set-list-list.lisp
A books/kestrel/fty/symbol-set-list.lisp
M books/kestrel/fty/top.lisp
Log Message:
-----------
[FTY] Add two general fixtypes.
Log Message:
-----------
Commit: d9c4568dcf0f6afc98e51b7cd00fe30f8b675c74
https://github.com/acl2/acl2/commit/d9c4568dcf0f6afc98e51b7cd00fe30f8b675c74
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some theorems.
Commit: c3c3e77eaafa2619c63d41b686291bc3e0de2c4e
https://github.com/acl2/acl2/commit/c3c3e77eaafa2619c63d41b686291bc3e0de2c4e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Simplify some hints.
Commit: cd3d8ccb5b61d8b09cb5dc2e03f8457c92438156
https://github.com/acl2/acl2/commit/cd3d8ccb5b61d8b09cb5dc2e03f8457c92438156
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some predicates.
Commit: 64315dd94fa498152b9ee22c67e3e0c0f002cf95
https://github.com/acl2/acl2/commit/64315dd94fa498152b9ee22c67e3e0c0f002cf95
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Simplify some hints.
Commit: aa08e28029585b351d3320c52bb9d08823d66cb9
https://github.com/acl2/acl2/commit/aa08e28029585b351d3320c52bb9d08823d66cb9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/grammar.abnf
Log Message:
-----------
[Remora] Move a note to a more central position.
Commit: 174e3b504b2f61b12a00880b7ea8ac00a0f40ae2
https://github.com/acl2/acl2/commit/174e3b504b2f61b12a00880b7ea8ac00a0f40ae2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/grammar.abnf
Log Message:
-----------
[Remora] Remove stray blank line.
Commit: c5cc5cc0b0f1dfc042862f9360a31e4582ce73b9
https://github.com/acl2/acl2/commit/c5cc5cc0b0f1dfc042862f9360a31e4582ce73b9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Remove a subsumed theorem.
Commit: 626cc63ae67d16a7f8d168586cde9df56668f060
https://github.com/acl2/acl2/commit/626cc63ae67d16a7f8d168586cde9df56668f060
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Log Message:
-----------
[Remora] Add some doc.
Commit: 6a464d57c695a911e59ccd6c748fcd04bda09065
https://github.com/acl2/acl2/commit/6a464d57c695a911e59ccd6c748fcd04bda09065
Author: Alessandro Coglio <2409151...@users.noreply.github.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/expression-values-and-environments.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
Log Message:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
-----------
Merge pull request #1988 from ltmquan/remora
[REMORA] added `reshape`
Commit: 4a09c83a8e661cb2d7efca549c1c3e713e29a942
https://github.com/acl2/acl2/commit/4a09c83a8e661cb2d7efca549c1c3e713e29a942
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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.
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Commit: 982d0b0ce236bdea389bc44f3473bd2321529e23
https://github.com/acl2/acl2/commit/982d0b0ce236bdea389bc44f3473bd2321529e23
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
Commit: 7e454027835d45e850af9b409ce77a9bcd1c0a02
https://github.com/acl2/acl2/commit/7e454027835d45e850af9b409ce77a9bcd1c0a02
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/desugaring.lisp
Log Message:
-----------
[Remora] Simplify desugaring.
Commit: 6c058e674b27559d9fe019ec67c89beac31a3c8b
https://github.com/acl2/acl2/commit/6c058e674b27559d9fe019ec67c89beac31a3c8b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/remora/expression-values-and-environments.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
Log Message:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
-----------
Merge.
Commit: 4f344831107e8a7e1e10844b77c5a90c8c13bb34
https://github.com/acl2/acl2/commit/4f344831107e8a7e1e10844b77c5a90c8c13bb34
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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/std/util/definductive.lisp
Log Message:
-----------
Merge.
Log Message:
-----------
Commit: 4b184ad520371bfc4c3bb02499898a53f4cc240c
https://github.com/acl2/acl2/commit/4b184ad520371bfc4c3bb02499898a53f4cc240c
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Commit: 127036a730484d24d097aa2f5b78fa8c4c01f265
https://github.com/acl2/acl2/commit/127036a730484d24d097aa2f5b78fa8c4c01f265
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
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: c2b5f1278ac2ced5a7b5679b128807bd01f82ebe
https://github.com/acl2/acl2/commit/c2b5f1278ac2ced5a7b5679b128807bd01f82ebe
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/projects/fields/embeddings.lisp
M books/projects/fields/support/embeddings.lisp
Log Message:
-----------
Defined inverse embedding
Commit: 89d2cf4304c4002efa205c9ed51c453b7b2d4263
https://github.com/acl2/acl2/commit/89d2cf4304c4002efa205c9ed51c453b7b2d4263
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: 4f41c9f07359f37071f263ab6dd9d628b3eee524
https://github.com/acl2/acl2/commit/4f41c9f07359f37071f263ab6dd9d628b3eee524
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/remora/expression-values-and-environments.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
Log Message:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
-----------
Merge commit '6a464d57c695a911e59ccd6c748fcd04bda09065' into HEAD
Commit: a20ec9a94780982cc48fc875c447fa3b9b8101d1
https://github.com/acl2/acl2/commit/a20ec9a94780982cc48fc875c447fa3b9b8101d1
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
Log Message:
-----------
“merge”
Commit: 9230f610e8176bef5e8b7519df0a335310b335f9
https://github.com/acl2/acl2/commit/9230f610e8176bef5e8b7519df0a335310b335f9
Author: David Russinoff <da...@russinoff.com>
Date: 2026-07-24 (Fri, 24 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/remora/expression-values-and-environments.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
Log Message:
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
-----------
“merge”
Commit: 98383ead4d64968fa0e2645c4223257c39d5eff3
https://github.com/acl2/acl2/commit/98383ead4d64968fa0e2645c4223257c39d5eff3
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
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/evaluation.lisp
M books/kestrel/remora/expression-values-and-environments.lisp
M books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/primitives-evaluation.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/std/util/definductive.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 '127036a730484d24d097aa2f5b78fa8c4c01f265' into HEAD
Commit: b6c31cb88ebf2e41e9d0e7e0bd79b87a8066d16c
https://github.com/acl2/acl2/commit/b6c31cb88ebf2e41e9d0e7e0bd79b87a8066d16c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.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/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/primitives-evaluation.lisp
M books/kestrel/remora/static-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/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/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.
Log Message:
-----------
Commit: c0b81f47bf75544e141e04b5802cb7e9882ed5c4
https://github.com/acl2/acl2/commit/c0b81f47bf75544e141e04b5802cb7e9882ed5c4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: 01c535f961022c5a01f27331aedf1fb589f498b3
https://github.com/acl2/acl2/commit/01c535f961022c5a01f27331aedf1fb589f498b3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: 2cc59f19f45bf2ee2c5f56a9d01fd353bbcb9831
https://github.com/acl2/acl2/commit/2cc59f19f45bf2ee2c5f56a9d01fd353bbcb9831
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: 25e80ce781d1704b4cd30cd8a361bdc9f8013fb6
https://github.com/acl2/acl2/commit/25e80ce781d1704b4cd30cd8a361bdc9f8013fb6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: c9ca7237aafd1842a6d4e9e00e321a09eea76230
https://github.com/acl2/acl2/commit/c9ca7237aafd1842a6d4e9e00e321a09eea76230
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: bb08f3c7e07c2641f26ece0c1ce3272cfe124854
https://github.com/acl2/acl2/commit/bb08f3c7e07c2641f26ece0c1ce3272cfe124854
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: 4584af836f19a05f51c3e6a4d1f46c3160f21f02
https://github.com/acl2/acl2/commit/4584af836f19a05f51c3e6a4d1f46c3160f21f02
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: 2c0ae2cbae0b3342e1f0a57a76a091d2ec796b72
https://github.com/acl2/acl2/commit/2c0ae2cbae0b3342e1f0a57a76a091d2ec796b72
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: e819cef97511be7c96577a12704b1817600df5d8
https://github.com/acl2/acl2/commit/e819cef97511be7c96577a12704b1817600df5d8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: 19a79469dbf277ff1e9eaef7f7977d977353faf6
https://github.com/acl2/acl2/commit/19a79469dbf277ff1e9eaef7f7977d977353faf6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: cf8a4ae1465ed49634b77b72f8eaa54179849c57
https://github.com/acl2/acl2/commit/cf8a4ae1465ed49634b77b72f8eaa54179849c57
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Commit: 6df62bcb2c6839f8904b2ce72d58cb12ebc24a1b
https://github.com/acl2/acl2/commit/6df62bcb2c6839f8904b2ce72d58cb12ebc24a1b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-25 (Sat, 25 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Log Message:
-----------
Compare: https://github.com/acl2/acl2/compare/17eeec0b6f05...6df62bcb2c68
Reply all
Reply to author
Forward
0 new messages