[acl2/acl2] 21e7fd: Fixed overly-general (but not wrong) theorem.

0 views
Skip to first unread message

MattKaufmann

unread,
Sep 18, 2025, 12:46:51 PM (7 days ago) Sep 18
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 21e7fd0de022213a787c692c1b094be747c42a70
https://github.com/acl2/acl2/commit/21e7fd0de022213a787c692c1b094be747c42a70
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/demos/defabsstobj-example-1.lisp

Log Message:
-----------
Fixed overly-general (but not wrong) theorem.



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

MattKaufmann

unread,
Sep 18, 2025, 12:47:39 PM (7 days ago) Sep 18
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Sep 19, 2025, 2:37:33 AM (6 days ago) Sep 19
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 21e7fd0de022213a787c692c1b094be747c42a70
https://github.com/acl2/acl2/commit/21e7fd0de022213a787c692c1b094be747c42a70
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/demos/defabsstobj-example-1.lisp

Log Message:
-----------
Fixed overly-general (but not wrong) theorem.


Commit: 059564e9b1525347427e86d430d1cd4dacc6d56b
https://github.com/acl2/acl2/commit/059564e9b1525347427e86d430d1cd4dacc6d56b
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
A books/kestrel/c/syntax/compilation-db.lisp
A books/kestrel/c/syntax/tests/compilation-db.lisp
A books/kestrel/c/syntax/tests/compile_commands.json
M books/kestrel/c/syntax/top.lisp

Log Message:
-----------
Merge commit '839bfa97dfb9911ab7c1f1da4d74152cc7a01e4d' into HEAD


Commit: c65338c02f92e36568fdb254cda8bd4a9255c2ca
https://github.com/acl2/acl2/commit/c65338c02f92e36568fdb254cda8bd4a9255c2ca
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for assignments.

Make the theorem about variables in computation states into a rewrite rule,
avoiding the `:use` hints for that theorem.


Commit: f5050ba8af0f85721104503e574d48f57faa9434
https://github.com/acl2/acl2/commit/f5050ba8af0f85721104503e574d48f57faa9434
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proof generation for initializers.


Commit: d7daeeb7df3e4d4752e958b04bbb5e0d03bdb1b1
https://github.com/acl2/acl2/commit/d7daeeb7df3e4d4752e958b04bbb5e0d03bdb1b1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for null statements.


Commit: ba41c17a64e25bab645beeee2c4ab83691f4fa75
https://github.com/acl2/acl2/commit/ba41c17a64e25bab645beeee2c4ab83691f4fa75
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for expression statements.


Commit: 427e118747bb2f975f2b9c3988bb68d8e82b54cc
https://github.com/acl2/acl2/commit/427e118747bb2f975f2b9c3988bb68d8e82b54cc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for return statements.


Commit: 25627b6caa1499581c89a489988c339b47567f4f
https://github.com/acl2/acl2/commit/25627b6caa1499581c89a489988c339b47567f4f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for `if` statements.


Commit: 377cb33d2c54bc2b3bb4a855d5fbc02ffdeade18
https://github.com/acl2/acl2/commit/377cb33d2c54bc2b3bb4a855d5fbc02ffdeade18
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optizmie `simpadd0` proofs for `if-else` statements.


Commit: 7c8f19090ccac3202b4554387df3f477467f209f
https://github.com/acl2/acl2/commit/7c8f19090ccac3202b4554387df3f477467f209f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp

Log Message:
-----------
[C2C] Reorder some code within a file.


Commit: 658183449ed9859d4fdeb1afefb01b6aae34817f
https://github.com/acl2/acl2/commit/658183449ed9859d4fdeb1afefb01b6aae34817f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for compound statements.


Commit: 63c748a9d7d318ce61a6c19605861e100f043e0b
https://github.com/acl2/acl2/commit/63c748a9d7d318ce61a6c19605861e100f043e0b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Improve some AST names.


Commit: ac3b97c464bfcd128482ce73b22d0ec25390f41c
https://github.com/acl2/acl2/commit/ac3b97c464bfcd128482ce73b22d0ec25390f41c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for object declarations.


Commit: fd0433b9a781cca536749a2ee770c4675be99f47
https://github.com/acl2/acl2/commit/fd0433b9a781cca536749a2ee770c4675be99f47
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for object declarations further.


Commit: 15bf6275e825c5691d2b872ab33e41622a6a5398
https://github.com/acl2/acl2/commit/15bf6275e825c5691d2b872ab33e41622a6a5398
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp

Log Message:
-----------
[C2C] Slightly simplify generated `simpadd0` proof hints.


Commit: bd635eec669729dabcb09ce4c556588e353dab53
https://github.com/acl2/acl2/commit/bd635eec669729dabcb09ce4c556588e353dab53
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for block item statements.


Commit: cf594aff8c937e2832dd6ed711bfa2bf6d246898
https://github.com/acl2/acl2/commit/cf594aff8c937e2832dd6ed711bfa2bf6d246898
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for block item declarations.


Commit: 9ed87d21990e260a3526d914d6d986b7bd4c777e
https://github.com/acl2/acl2/commit/9ed87d21990e260a3526d914d6d986b7bd4c777e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for empty lists of blocks.


Commit: 4dce3fdb145efabe0bc9760394ccb4563b7efbaa
https://github.com/acl2/acl2/commit/4dce3fdb145efabe0bc9760394ccb4563b7efbaa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Optimize `simpadd0` proofs for non-empty lists of blocks.


Commit: 962a188d63f27681f95381d59cb18d2ee1babaec
https://github.com/acl2/acl2/commit/962a188d63f27681f95381d59cb18d2ee1babaec
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
[C2C] Simplify some supporting theorems and speed up some proofs.

We don't really need the `syntaxp` hyps for these.


Commit: 1ab1d98ca53caedaf1bdcf9f51253b303f820310
https://github.com/acl2/acl2/commit/1ab1d98ca53caedaf1bdcf9f51253b303f820310
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/demos/defabsstobj-example-1.lisp
A books/kestrel/c/syntax/compilation-db.lisp
A books/kestrel/c/syntax/tests/compilation-db.lisp
A books/kestrel/c/syntax/tests/compile_commands.json
M books/kestrel/c/syntax/top.lisp

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


Commit: 9d7049f4c90bb7815caf38fd97308093793e9254
https://github.com/acl2/acl2/commit/9d7049f4c90bb7815caf38fd97308093793e9254
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-18 (Thu, 18 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


Compare: https://github.com/acl2/acl2/compare/839bfa97dfb9...9d7049f4c90b
Reply all
Reply to author
Forward
0 new messages