[acl2/acl2] 30155a: [definductive] Extend towards multiple predicates.
0 views
Skip to first unread message
Alessandro Coglio
Jul 27, 2026, 9:27:36 PM (2 days ago) Jul 27
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 30155a9d5075f897a0611d01d45ac9da140a6ecb
https://github.com/acl2/acl2/commit/30155a9d5075f897a0611d01d45ac9da140a6ecb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Extend towards multiple predicates.
Commit: baf5dea6860b01b838771413976b5b424bace3d7
https://github.com/acl2/acl2/commit/baf5dea6860b01b838771413976b5b424bace3d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/fty/symbol-set-list-list.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize some generation code.
Commit: 83920ef0755c6825703b5041658d99d6eb81bf74
https://github.com/acl2/acl2/commit/83920ef0755c6825703b5041658d99d6eb81bf74
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
R books/kestrel/c/syntax/abstract-syntax-symbols.lisp
A books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
Log Message:
-----------
[C$] Rename file.
Commit: a97917c3f4a341625b4fcda2956806810648b79e
https://github.com/acl2/acl2/commit/a97917c3f4a341625b4fcda2956806810648b79e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize generation of proof fixtypes.
Generalize the code to generate multiple fixtypes, organized in cliques,
according to the organization of the predicates.
Commit: d8b790f88fdaeb08d135ec443fde62b2ad0ce628
https://github.com/acl2/acl2/commit/d8b790f88fdaeb08d135ec443fde62b2ad0ce628
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
Log Message:
-----------
[C$] Rename a constant.
Commit: a7fa757a3bf19f79e7bb51ebab07eedab2e773dd
https://github.com/acl2/acl2/commit/a7fa757a3bf19f79e7bb51ebab07eedab2e773dd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve some generated doc.
Commit: 40cbb52e5c77afa00eb4bbe96068a3df4fd15537
https://github.com/acl2/acl2/commit/40cbb52e5c77afa00eb4bbe96068a3df4fd15537
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve function names.
Commit: 31eb2d3e322e6cacef551f2fecf3a9e5d4b21565
https://github.com/acl2/acl2/commit/31eb2d3e322e6cacef551f2fecf3a9e5d4b21565
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/arithmetic-light/mod.lisp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/logext.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
Log Message:
-----------
Merge.
Commit: 4c3411a8164be965eb8c7428f2cb61002d8ba997
https://github.com/acl2/acl2/commit/4c3411a8164be965eb8c7428f2cb61002d8ba997
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
R books/kestrel/c/syntax/abstract-syntax-symbols.lisp
A books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/027ef5e77d5f...4c3411a8164b
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 30155a9d5075f897a0611d01d45ac9da140a6ecb
https://github.com/acl2/acl2/commit/30155a9d5075f897a0611d01d45ac9da140a6ecb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Extend towards multiple predicates.
Commit: baf5dea6860b01b838771413976b5b424bace3d7
https://github.com/acl2/acl2/commit/baf5dea6860b01b838771413976b5b424bace3d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/fty/symbol-set-list-list.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize some generation code.
Commit: 83920ef0755c6825703b5041658d99d6eb81bf74
https://github.com/acl2/acl2/commit/83920ef0755c6825703b5041658d99d6eb81bf74
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
R books/kestrel/c/syntax/abstract-syntax-symbols.lisp
A books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
Log Message:
-----------
[C$] Rename file.
Commit: a97917c3f4a341625b4fcda2956806810648b79e
https://github.com/acl2/acl2/commit/a97917c3f4a341625b4fcda2956806810648b79e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize generation of proof fixtypes.
Generalize the code to generate multiple fixtypes, organized in cliques,
according to the organization of the predicates.
Commit: d8b790f88fdaeb08d135ec443fde62b2ad0ce628
https://github.com/acl2/acl2/commit/d8b790f88fdaeb08d135ec443fde62b2ad0ce628
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
Log Message:
-----------
[C$] Rename a constant.
Commit: a7fa757a3bf19f79e7bb51ebab07eedab2e773dd
https://github.com/acl2/acl2/commit/a7fa757a3bf19f79e7bb51ebab07eedab2e773dd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve some generated doc.
Commit: 40cbb52e5c77afa00eb4bbe96068a3df4fd15537
https://github.com/acl2/acl2/commit/40cbb52e5c77afa00eb4bbe96068a3df4fd15537
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Improve function names.
Commit: 31eb2d3e322e6cacef551f2fecf3a9e5d4b21565
https://github.com/acl2/acl2/commit/31eb2d3e322e6cacef551f2fecf3a9e5d4b21565
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/arithmetic-light/mod.lisp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/logext.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
Log Message:
-----------
Merge.
Commit: 4c3411a8164be965eb8c7428f2cb61002d8ba997
https://github.com/acl2/acl2/commit/4c3411a8164be965eb8c7428f2cb61002d8ba997
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
R books/kestrel/c/syntax/abstract-syntax-symbols.lisp
A books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/027ef5e77d5f...4c3411a8164b
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Jul 27, 2026, 10:43:33 PM (2 days ago) Jul 27
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
https://github.com/acl2/acl2/commit/e48d78f4620c2906f760a01d9004c0ead6022bcc
Log Message:
-----------
[C$] Export more symbols.
Commit: 477cfa18323b7f562aa95be8310eb85a824b71a7
https://github.com/acl2/acl2/commit/477cfa18323b7f562aa95be8310eb85a824b71a7
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[STS safety] Pass additional information.
The additional information are the type completions, so that (in an upcoming
commit) we can use that to deepen certain checks.
Commit: f9968a2f079c36296de9486581a8e88033ee58f2
https://github.com/acl2/acl2/commit/f9968a2f079c36296de9486581a8e88033ee58f2
Log Message:
-----------
[STS safety] Add a recursion limit to a clique.
In preparation for an extension.
Commit: 68f84dfed2194d03f7cc69263291923bf42f05b6
https://github.com/acl2/acl2/commit/68f84dfed2194d03f7cc69263291923bf42f05b6
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[STS safety] Pass validation table.
This is also needed, to look up tagged struct members.
Commit: d9ff6a5c46c3b14fc6cc6c1bad3143cfb508a65e
https://github.com/acl2/acl2/commit/d9ff6a5c46c3b14fc6cc6c1bad3143cfb508a65e
Log Message:
-----------
[STS safe] Improve a check.
For cast expressions, improve the 'may refer' check to also look up members
of tagged struct and union types.
Commit: 3d8b5eaa1d6b665c9fec2caa16cfa3701b20a2f8
https://github.com/acl2/acl2/commit/3d8b5eaa1d6b665c9fec2caa16cfa3701b20a2f8
https://github.com/acl2/acl2/commit/c4b20182389ec6af95aef76e07182d931595e445
Log Message:
-----------
[STS safety] Relax checks on initializers with designators.
Commit: 2e4ebd41dd0577425be283c923fccd8d42587d30
https://github.com/acl2/acl2/commit/2e4ebd41dd0577425be283c923fccd8d42587d30
Log Message:
-----------
[STS safety] Add safety checks to several tests.
Commit: 027ef5e77d5fc46824fa12920195cd8a63a56a31
https://github.com/acl2/acl2/commit/027ef5e77d5fc46824fa12920195cd8a63a56a31
Log Message:
-----------
[STS] Lift a safety check restriction.
Commit: 1d751d9dfa145e90ce9eeb0077c87fb2a7fba3f0
https://github.com/acl2/acl2/commit/1d751d9dfa145e90ce9eeb0077c87fb2a7fba3f0
A books/kestrel/remora/abstract-syntax-well-formedness.lisp
M books/kestrel/remora/abstract-syntax.lisp
M books/kestrel/remora/printer.lisp
Log Message:
-----------
[Remorea] Rename a file.
Commit: e811bc2b10f1cac113b3a10167c1f87efde02ecb
https://github.com/acl2/acl2/commit/e811bc2b10f1cac113b3a10167c1f87efde02ecb
Log Message:
-----------
[ABNF] Add/tweak some tree ops.
Commit: e9552d12728666f999294a2926b2e60fd5eb9714
https://github.com/acl2/acl2/commit/e9552d12728666f999294a2926b2e60fd5eb9714
M books/kestrel/remora/abstract-syntax.lisp
Log Message:
-----------
[Remora] Reorder some topics.
Commit: 442a8809986ae04af64ac5887e5ff403a522672c
https://github.com/acl2/acl2/commit/442a8809986ae04af64ac5887e5ff403a522672c
M books/kestrel/remora/identifier-syntax.lisp
Log Message:
-----------
[Remora] Shorten some function names.
Commit: 85e8efd17c51605bbd578b3533814cd90b3aa64a
https://github.com/acl2/acl2/commit/85e8efd17c51605bbd578b3533814cd90b3aa64a
Log Message:
-----------
[Remora] Update some doc.
Commit: cd621457b7f1c3ea5b6863982e071ffa4bc6e9a2
https://github.com/acl2/acl2/commit/cd621457b7f1c3ea5b6863982e071ffa4bc6e9a2
Log Message:
-----------
[Remora] Update AST well-formedness predicates.
Commit: a920db560320c22211f99d70a64d7d850c1010ce
https://github.com/acl2/acl2/commit/a920db560320c22211f99d70a64d7d850c1010ce
Log Message:
-----------
[Remora] Extend the AST wf predicates.
Commit: b759d3869c4afb5d26550096ce2121e9bbf58d2a
https://github.com/acl2/acl2/commit/b759d3869c4afb5d26550096ce2121e9bbf58d2a
Log Message:
-----------
[Remora] Fix some wf AST predicates.
Commit: 074940a440ca47154cbb89eaef8ce499422287aa
https://github.com/acl2/acl2/commit/074940a440ca47154cbb89eaef8ce499422287aa
Log Message:
-----------
[Remora] Update some doc.
Commit: 8164c8a48182ecab7c26978064d503d4ab9d3495
https://github.com/acl2/acl2/commit/8164c8a48182ecab7c26978064d503d4ab9d3495
Log Message:
-----------
Update reference.
Commit: 6940dc566408f796434cd29ab29089c8595f3699
https://github.com/acl2/acl2/commit/6940dc566408f796434cd29ab29089c8595f3699
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
Log Message:
-----------
[Remora] Relax a wf AST constraint.
Commit: 603b9780c8457208e32223bea9fd1c94c0f4d359
https://github.com/acl2/acl2/commit/603b9780c8457208e32223bea9fd1c94c0f4d359
Log Message:
-----------
[Remora] Fix some doc.
Commit: 4a97cfec16660cdbceb344eaa1f296d747decb00
https://github.com/acl2/acl2/commit/4a97cfec16660cdbceb344eaa1f296d747decb00
Log Message:
-----------
[ABNF] Add a tree operation.
Commit: fefdaaa899744ce213fbc75b646ac765aaae4921
https://github.com/acl2/acl2/commit/fefdaaa899744ce213fbc75b646ac765aaae4921
Log Message:
-----------
[ABNF] Update some parents.
Commit: 342d0dbc952343594a51d72d73dbbece9c116f6b
https://github.com/acl2/acl2/commit/342d0dbc952343594a51d72d73dbbece9c116f6b
Log Message:
-----------
[Remora] Localize a book inclusion.
Commit: fe8910bb876abbc3fc83ad76d6b4afe119acfd78
https://github.com/acl2/acl2/commit/fe8910bb876abbc3fc83ad76d6b4afe119acfd78
Log Message:
-----------
[ABNF] Fix doc typos.
Commit: b51aa1138f8d6f267f3e3098f777b026fa5222ce
https://github.com/acl2/acl2/commit/b51aa1138f8d6f267f3e3098f777b026fa5222ce
-----------
Merge.
Commit: 0b00a045e17109f26ba645907d7ee9ed01e3abe4
https://github.com/acl2/acl2/commit/0b00a045e17109f26ba645907d7ee9ed01e3abe4
M books/projects/filesystems/utilities/cpp-syntax/package.lsp
Commit: ccc84b54b651a2bf45ff092654c2d4ad509b84f9
https://github.com/acl2/acl2/commit/ccc84b54b651a2bf45ff092654c2d4ad509b84f9
Log Message:
-----------
[Remora] Improve some doc.
Commit: 76311569bccb8aa68ab8a7dbfe56d951782d5a5c
https://github.com/acl2/acl2/commit/76311569bccb8aa68ab8a7dbfe56d951782d5a5c
Log Message:
-----------
Merge.
Commit: e15e7589a80f5ceaa5931ddbbca30858563c9958
https://github.com/acl2/acl2/commit/e15e7589a80f5ceaa5931ddbbca30858563c9958
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/12160a9624bf...e15e7589a80f
Home: https://github.com/acl2/acl2
Commit: 30155a9d5075f897a0611d01d45ac9da140a6ecb
https://github.com/acl2/acl2/commit/30155a9d5075f897a0611d01d45ac9da140a6ecb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Extend towards multiple predicates.
Commit: baf5dea6860b01b838771413976b5b424bace3d7
https://github.com/acl2/acl2/commit/baf5dea6860b01b838771413976b5b424bace3d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/fty/symbol-set-list-list.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize some generation code.
Commit: e48d78f4620c2906f760a01d9004c0ead6022bcc
Commit: 30155a9d5075f897a0611d01d45ac9da140a6ecb
https://github.com/acl2/acl2/commit/30155a9d5075f897a0611d01d45ac9da140a6ecb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Extend towards multiple predicates.
Commit: baf5dea6860b01b838771413976b5b424bace3d7
https://github.com/acl2/acl2/commit/baf5dea6860b01b838771413976b5b424bace3d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/fty/symbol-set-list-list.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize some generation code.
https://github.com/acl2/acl2/commit/e48d78f4620c2906f760a01d9004c0ead6022bcc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[C$] Export more symbols.
Commit: 477cfa18323b7f562aa95be8310eb85a824b71a7
https://github.com/acl2/acl2/commit/477cfa18323b7f562aa95be8310eb85a824b71a7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[STS safety] Pass additional information.
The additional information are the type completions, so that (in an upcoming
commit) we can use that to deepen certain checks.
Commit: f9968a2f079c36296de9486581a8e88033ee58f2
https://github.com/acl2/acl2/commit/f9968a2f079c36296de9486581a8e88033ee58f2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[STS safety] Add a recursion limit to a clique.
In preparation for an extension.
Commit: 68f84dfed2194d03f7cc69263291923bf42f05b6
https://github.com/acl2/acl2/commit/68f84dfed2194d03f7cc69263291923bf42f05b6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
[STS safety] Pass validation table.
This is also needed, to look up tagged struct members.
Commit: d9ff6a5c46c3b14fc6cc6c1bad3143cfb508a65e
https://github.com/acl2/acl2/commit/d9ff6a5c46c3b14fc6cc6c1bad3143cfb508a65e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[STS safe] Improve a check.
For cast expressions, improve the 'may refer' check to also look up members
of tagged struct and union types.
Commit: 3d8b5eaa1d6b665c9fec2caa16cfa3701b20a2f8
https://github.com/acl2/acl2/commit/3d8b5eaa1d6b665c9fec2caa16cfa3701b20a2f8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/arithmetic-light/mod.lisp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/logext.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/arithmetic-light/mod.lisp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/logext.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
Log Message:
-----------
Merge.
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/monomorphize.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/values-to-abstract-syntax.lisp
Log Message:
-----------
Merge.
Commit: 83920ef0755c6825703b5041658d99d6eb81bf74
https://github.com/acl2/acl2/commit/83920ef0755c6825703b5041658d99d6eb81bf74
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
R books/kestrel/c/syntax/abstract-syntax-symbols.lisp
A books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
Log Message:
-----------
[C$] Rename file.
Commit: a97917c3f4a341625b4fcda2956806810648b79e
https://github.com/acl2/acl2/commit/a97917c3f4a341625b4fcda2956806810648b79e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize generation of proof fixtypes.
Generalize the code to generate multiple fixtypes, organized in cliques,
according to the organization of the predicates.
Commit: c4b20182389ec6af95aef76e07182d931595e445
https://github.com/acl2/acl2/commit/83920ef0755c6825703b5041658d99d6eb81bf74
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
R books/kestrel/c/syntax/abstract-syntax-symbols.lisp
A books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
Log Message:
-----------
[C$] Rename file.
Commit: a97917c3f4a341625b4fcda2956806810648b79e
https://github.com/acl2/acl2/commit/a97917c3f4a341625b4fcda2956806810648b79e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize generation of proof fixtypes.
Generalize the code to generate multiple fixtypes, organized in cliques,
according to the organization of the predicates.
https://github.com/acl2/acl2/commit/c4b20182389ec6af95aef76e07182d931595e445
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[STS safety] Relax checks on initializers with designators.
Commit: 2e4ebd41dd0577425be283c923fccd8d42587d30
https://github.com/acl2/acl2/commit/2e4ebd41dd0577425be283c923fccd8d42587d30
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[STS safety] Add safety checks to several tests.
Commit: 027ef5e77d5fc46824fa12920195cd8a63a56a31
https://github.com/acl2/acl2/commit/027ef5e77d5fc46824fa12920195cd8a63a56a31
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[STS] Lift a safety check restriction.
https://github.com/acl2/acl2/commit/1d751d9dfa145e90ce9eeb0077c87fb2a7fba3f0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
R books/kestrel/remora/abstract-syntax-well-formed.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
A books/kestrel/remora/abstract-syntax-well-formedness.lisp
M books/kestrel/remora/abstract-syntax.lisp
M books/kestrel/remora/printer.lisp
Log Message:
-----------
[Remorea] Rename a file.
Commit: e811bc2b10f1cac113b3a10167c1f87efde02ecb
https://github.com/acl2/acl2/commit/e811bc2b10f1cac113b3a10167c1f87efde02ecb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/projects/abnf/tree-operations/subtree-operations.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[ABNF] Add/tweak some tree ops.
Commit: e9552d12728666f999294a2926b2e60fd5eb9714
https://github.com/acl2/acl2/commit/e9552d12728666f999294a2926b2e60fd5eb9714
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax.lisp
Log Message:
-----------
[Remora] Reorder some topics.
Commit: 442a8809986ae04af64ac5887e5ff403a522672c
https://github.com/acl2/acl2/commit/442a8809986ae04af64ac5887e5ff403a522672c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/identifier-syntax.lisp
Log Message:
-----------
[Remora] Shorten some function names.
Commit: 85e8efd17c51605bbd578b3533814cd90b3aa64a
https://github.com/acl2/acl2/commit/85e8efd17c51605bbd578b3533814cd90b3aa64a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[Remora] Update some doc.
Commit: cd621457b7f1c3ea5b6863982e071ffa4bc6e9a2
https://github.com/acl2/acl2/commit/cd621457b7f1c3ea5b6863982e071ffa4bc6e9a2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[Remora] Update AST well-formedness predicates.
Commit: a920db560320c22211f99d70a64d7d850c1010ce
https://github.com/acl2/acl2/commit/a920db560320c22211f99d70a64d7d850c1010ce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[Remora] Extend the AST wf predicates.
Commit: b759d3869c4afb5d26550096ce2121e9bbf58d2a
https://github.com/acl2/acl2/commit/b759d3869c4afb5d26550096ce2121e9bbf58d2a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[Remora] Fix some wf AST predicates.
Commit: 074940a440ca47154cbb89eaef8ce499422287aa
https://github.com/acl2/acl2/commit/074940a440ca47154cbb89eaef8ce499422287aa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/check-keywords.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[Remora] Update some doc.
https://github.com/acl2/acl2/commit/8164c8a48182ecab7c26978064d503d4ab9d3495
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/package.lsp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
Update reference.
Commit: 6940dc566408f796434cd29ab29089c8595f3699
https://github.com/acl2/acl2/commit/6940dc566408f796434cd29ab29089c8595f3699
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
Log Message:
-----------
[Remora] Relax a wf AST constraint.
Commit: 603b9780c8457208e32223bea9fd1c94c0f4d359
https://github.com/acl2/acl2/commit/603b9780c8457208e32223bea9fd1c94c0f4d359
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[Remora] Fix some doc.
Commit: 4a97cfec16660cdbceb344eaa1f296d747decb00
https://github.com/acl2/acl2/commit/4a97cfec16660cdbceb344eaa1f296d747decb00
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/projects/abnf/tree-operations/subtree-operations.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[ABNF] Add a tree operation.
Commit: fefdaaa899744ce213fbc75b646ac765aaae4921
https://github.com/acl2/acl2/commit/fefdaaa899744ce213fbc75b646ac765aaae4921
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/projects/abnf/tree-operations/subtree-operations.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[ABNF] Update some parents.
Commit: 342d0dbc952343594a51d72d73dbbece9c116f6b
https://github.com/acl2/acl2/commit/342d0dbc952343594a51d72d73dbbece9c116f6b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formedness.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[Remora] Localize a book inclusion.
Commit: fe8910bb876abbc3fc83ad76d6b4afe119acfd78
https://github.com/acl2/acl2/commit/fe8910bb876abbc3fc83ad76d6b4afe119acfd78
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/projects/abnf/tree-operations/subtree-operations.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[ABNF] Fix doc typos.
Commit: b51aa1138f8d6f267f3e3098f777b026fa5222ce
https://github.com/acl2/acl2/commit/b51aa1138f8d6f267f3e3098f777b026fa5222ce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
Log Message:
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
-----------
Merge.
Commit: 0b00a045e17109f26ba645907d7ee9ed01e3abe4
https://github.com/acl2/acl2/commit/0b00a045e17109f26ba645907d7ee9ed01e3abe4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
R books/kestrel/c/syntax/abstract-syntax-symbols.lisp
A books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
M books/kestrel/fty/symbol-set-list-list.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
R books/kestrel/c/syntax/abstract-syntax-symbols.lisp
A books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
M books/projects/filesystems/utilities/cpp-syntax/package.lsp
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
Log Message:
-----------
Commit: ccc84b54b651a2bf45ff092654c2d4ad509b84f9
https://github.com/acl2/acl2/commit/ccc84b54b651a2bf45ff092654c2d4ad509b84f9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
[Remora] Improve some doc.
Commit: 76311569bccb8aa68ab8a7dbfe56d951782d5a5c
https://github.com/acl2/acl2/commit/76311569bccb8aa68ab8a7dbfe56d951782d5a5c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/projects/abnf/tree-operations/subtree-operations.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
Merge.
Commit: e15e7589a80f5ceaa5931ddbbca30858563c9958
https://github.com/acl2/acl2/commit/e15e7589a80f5ceaa5931ddbbca30858563c9958
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/remora/dimension-equivalence-infrules.lisp
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/12160a9624bf...e15e7589a80f
Alessandro Coglio
Jul 28, 2026, 12:08:01 AM (yesterday) Jul 28
to acl2-...@googlegroups.com
Branch: refs/heads/master
Compare: https://github.com/acl2/acl2/compare/027ef5e77d5f...8164c8a48182
Home: https://github.com/acl2/acl2
Commit: 30155a9d5075f897a0611d01d45ac9da140a6ecb
https://github.com/acl2/acl2/commit/30155a9d5075f897a0611d01d45ac9da140a6ecb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Extend towards multiple predicates.
Commit: baf5dea6860b01b838771413976b5b424bace3d7
https://github.com/acl2/acl2/commit/baf5dea6860b01b838771413976b5b424bace3d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/fty/symbol-set-list-list.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize some generation code.
Commit: 30155a9d5075f897a0611d01d45ac9da140a6ecb
https://github.com/acl2/acl2/commit/30155a9d5075f897a0611d01d45ac9da140a6ecb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Extend towards multiple predicates.
Commit: baf5dea6860b01b838771413976b5b424bace3d7
https://github.com/acl2/acl2/commit/baf5dea6860b01b838771413976b5b424bace3d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/kestrel/fty/symbol-set-list-list.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize some generation code.
Commit: 83920ef0755c6825703b5041658d99d6eb81bf74
https://github.com/acl2/acl2/commit/83920ef0755c6825703b5041658d99d6eb81bf74
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
R books/kestrel/c/syntax/abstract-syntax-symbols.lisp
A books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
Log Message:
-----------
[C$] Rename file.
Commit: a97917c3f4a341625b4fcda2956806810648b79e
https://github.com/acl2/acl2/commit/a97917c3f4a341625b4fcda2956806810648b79e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize generation of proof fixtypes.
Generalize the code to generate multiple fixtypes, organized in cliques,
according to the organization of the predicates.
https://github.com/acl2/acl2/commit/83920ef0755c6825703b5041658d99d6eb81bf74
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
R books/kestrel/c/syntax/abstract-syntax-symbols.lisp
A books/kestrel/c/syntax/exported-symbols.lisp
M books/kestrel/c/transformation/package.lsp
Log Message:
-----------
[C$] Rename file.
Commit: a97917c3f4a341625b4fcda2956806810648b79e
https://github.com/acl2/acl2/commit/a97917c3f4a341625b4fcda2956806810648b79e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-27 (Mon, 27 Jul 2026)
Changed paths:
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Generalize generation of proof fixtypes.
Generalize the code to generate multiple fixtypes, organized in cliques,
according to the organization of the predicates.
Alessandro Coglio
Jul 28, 2026, 12:08:38 AM (yesterday) Jul 28
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages