[acl2/acl2] 59efce: [C2C] Improve some variable names.
0 views
Skip to first unread message
Alessandro Coglio
Dec 3, 2025, 9:25:56 AM (5 days ago) Dec 3
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 59efce71e39296171bc68039691e6f7e037475a2
https://github.com/acl2/acl2/commit/59efce71e39296171bc68039691e6f7e037475a2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: 7e147256519ed4adc5e3c388e222d481e0f0db41
https://github.com/acl2/acl2/commit/7e147256519ed4adc5e3c388e222d481e0f0db41
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: 6a4eb4d5cd8a39b7aaffd1e6ac43617325339d91
https://github.com/acl2/acl2/commit/6a4eb4d5cd8a39b7aaffd1e6ac43617325339d91
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: c8406a2fce5f941bc0dfbdb9cd7ed428d04814e1
https://github.com/acl2/acl2/commit/c8406a2fce5f941bc0dfbdb9cd7ed428d04814e1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: 57dfa1d654cb0178333b371791e138299f00cd3c
https://github.com/acl2/acl2/commit/57dfa1d654cb0178333b371791e138299f00cd3c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: 9bfa6e3e366601104e7e7cba6d046e55d7cf0f6c
https://github.com/acl2/acl2/commit/9bfa6e3e366601104e7e7cba6d046e55d7cf0f6c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: 574de091c64c231d5760c6b01720c2c0bb3ea6d2
https://github.com/acl2/acl2/commit/574de091c64c231d5760c6b01720c2c0bb3ea6d2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Extend characterization of formalized subset.
Match `exec-expr`.
Commit: f6eb71d192dd7a097567e1c94d05db278fa584fe
https://github.com/acl2/acl2/commit/f6eb71d192dd7a097567e1c94d05db278fa584fe
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/logand.c
M books/kestrel/c/transformation/tests/simpadd0/old/logor.c
Log Message:
-----------
[C2C] Extend proof generation.
Add support for non-strict binary expressions with non-pure operands.
Also add tests to demonstrate this added support.
Commit: 48bca8037985a9c430da354f5253718431553bda
https://github.com/acl2/acl2/commit/48bca8037985a9c430da354f5253718431553bda
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Extend characterization of formalized subset.
Match `exec-initer` for initializers.
Commit: 73c2be888a689ab9fab0bc0688196100a8f57295
https://github.com/acl2/acl2/commit/73c2be888a689ab9fab0bc0688196100a8f57295
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Extend characterization of formalized subset.
Update according to `exec-stmt`.
Commit: f378436caf88702a9bac7d06761c8fa9550c021e
https://github.com/acl2/acl2/commit/f378436caf88702a9bac7d06761c8fa9550c021e
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M acl2-fns.lisp
M axioms.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Improved error message for #!(foo) etc. Avoided hard Lisp errors from er calls.
Quoting :DOC note-8-7:
Improved the error message when the package name is missing
immediately after `#!', as in #!(foo).
Some ill-formed hard errors, for example from calls of er, caused raw
Lisp errors. This has been fixed. Thanks to Eric Smith for
reporting this bug with an example.
Commit: af571c5a54ed19fc8b2d17d4e519aca0ad10ec7d
https://github.com/acl2/acl2/commit/af571c5a54ed19fc8b2d17d4e519aca0ad10ec7d
Author: Eric McCarthy <bend...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
Log Message:
-----------
[axe] more comments on the abs test case
Commit: aae3d00a5921a356f2d16b9532a5b76aaf4e64e4
https://github.com/acl2/acl2/commit/aae3d00a5921a356f2d16b9532a5b76aaf4e64e4
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
Log Message:
-----------
Merge commit 'af571c5a54ed19fc8b2d17d4e519aca0ad10ec7d' into HEAD
Commit: fe7b58d59124ccd48d6fc58732d250e7aa46dd67
https://github.com/acl2/acl2/commit/fe7b58d59124ccd48d6fc58732d250e7aa46dd67
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M axioms.lisp
Log Message:
-----------
Improved on fix from earlier today, for error messages from certain bad er calls.
Commit: 557343f250cf6846ae9df7bbb7430e118768e798
https://github.com/acl2/acl2/commit/557343f250cf6846ae9df7bbb7430e118768e798
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
Log Message:
-----------
[C$] Remove some code no longer needed.
Commit: 16f40eb3df24146bd4d7aa5a0a43365ae6fc8223
https://github.com/acl2/acl2/commit/16f40eb3df24146bd4d7aa5a0a43365ae6fc8223
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
Log Message:
-----------
[C$] Remove some code no longer needed.
Commit: b9d8e0bbd889eb55c690ee0779fb7e17a0e6bb5b
https://github.com/acl2/acl2/commit/b9d8e0bbd889eb55c690ee0779fb7e17a0e6bb5b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
Log Message:
-----------
[C$] Improve formulation of formalized subset.
Avoid use of the `...-pure-formalp` predicates, which will be removed.
Commit: d1959f568073461030b6e987f5fd32f9096412a1
https://github.com/acl2/acl2/commit/d1959f568073461030b6e987f5fd32f9096412a1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Remove some code no longer needed.
Commit: d2dd755c28f0ed79131b046c06c6f5bf1c4d2e66
https://github.com/acl2/acl2/commit/d2dd755c28f0ed79131b046c06c6f5bf1c4d2e66
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/ternary_int.c
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
Log Message:
-----------
[C2C] Extend proof generation.
Add support for non-pure conditional expressions.
We just had to remove the checks for purity, as everything else was already in
place.
Also add a test to demonstrate support.
Commit: aa917a1237e54a78796b584fe8b681ff76dbd6f3
https://github.com/acl2/acl2/commit/aa917a1237e54a78796b584fe8b681ff76dbd6f3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/tests/simpadd0/old/logand.c
Log Message:
-----------
[C2C] Tweak test.
Commit: d561de221862c72b0822aacc858e195803afa1bd
https://github.com/acl2/acl2/commit/d561de221862c72b0822aacc858e195803afa1bd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/gg.c
Log Message:
-----------
[C2C] Extend proof generation.
Add support for non-pure initializers.
We just had to remove the purity test, since everything else was already in
place.
Also add a test to demonstrate support.
Commit: 66d7fc9428a3accb51fd8049c22363855b6948e2
https://github.com/acl2/acl2/commit/66d7fc9428a3accb51fd8049c22363855b6948e2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/if.c
M books/kestrel/c/transformation/tests/simpadd0/old/ifelse.c
Log Message:
-----------
[C2C] Extend proof generation.
Add support for `if` and `if-else` with non-pure expression tests. We just had
to remove the purity checks, because everything else was already in place.
Also add some tests to demonstrate support.
Commit: 2605d85378d42a27d5a2cecdf49571427590ff93
https://github.com/acl2/acl2/commit/2605d85378d42a27d5a2cecdf49571427590ff93
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/tests/simpadd0/old/while.c
M books/kestrel/c/transformation/tests/simpadd0/while.lisp
Log Message:
-----------
[C2C] Add a test for `while` loops.
This demonstrates support for non-pure test expressions.
Commit: 295bc4a9cb39548a032d4fd69574601d30cbec24
https://github.com/acl2/acl2/commit/295bc4a9cb39548a032d4fd69574601d30cbec24
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/tests/simpadd0/dowhile.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/dowhile.c
Log Message:
-----------
[C2C] Add a test for `do-while` loops.
Demonstrate support for non-pure test expressions.
Commit: c6e3c8f4eb83993d92212c617de05e2dba27024a
https://github.com/acl2/acl2/commit/c6e3c8f4eb83993d92212c617de05e2dba27024a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/gg.c
Log Message:
-----------
[C2C] Improve a test.
Demonstrate support for non-pure return expressions.
Commit: daa977b6a3b9588e8993e542113a4a93c19c9320
https://github.com/acl2/acl2/commit/daa977b6a3b9588e8993e542113a4a93c19c9320
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Trim some hints in generated proofs.
Commit: 9322aec2bc6f8f6488ee8a7ad2d163e19a2ecdd5
https://github.com/acl2/acl2/commit/9322aec2bc6f8f6488ee8a7ad2d163e19a2ecdd5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M acl2-fns.lisp
M axioms.lisp
M books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/d1486dbf67a4...9322aec2bc6f
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 59efce71e39296171bc68039691e6f7e037475a2
https://github.com/acl2/acl2/commit/59efce71e39296171bc68039691e6f7e037475a2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: 7e147256519ed4adc5e3c388e222d481e0f0db41
https://github.com/acl2/acl2/commit/7e147256519ed4adc5e3c388e222d481e0f0db41
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: 6a4eb4d5cd8a39b7aaffd1e6ac43617325339d91
https://github.com/acl2/acl2/commit/6a4eb4d5cd8a39b7aaffd1e6ac43617325339d91
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: c8406a2fce5f941bc0dfbdb9cd7ed428d04814e1
https://github.com/acl2/acl2/commit/c8406a2fce5f941bc0dfbdb9cd7ed428d04814e1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: 57dfa1d654cb0178333b371791e138299f00cd3c
https://github.com/acl2/acl2/commit/57dfa1d654cb0178333b371791e138299f00cd3c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: 9bfa6e3e366601104e7e7cba6d046e55d7cf0f6c
https://github.com/acl2/acl2/commit/9bfa6e3e366601104e7e7cba6d046e55d7cf0f6c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Improve some variable names.
Commit: 574de091c64c231d5760c6b01720c2c0bb3ea6d2
https://github.com/acl2/acl2/commit/574de091c64c231d5760c6b01720c2c0bb3ea6d2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Extend characterization of formalized subset.
Match `exec-expr`.
Commit: f6eb71d192dd7a097567e1c94d05db278fa584fe
https://github.com/acl2/acl2/commit/f6eb71d192dd7a097567e1c94d05db278fa584fe
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/logand.c
M books/kestrel/c/transformation/tests/simpadd0/old/logor.c
Log Message:
-----------
[C2C] Extend proof generation.
Add support for non-strict binary expressions with non-pure operands.
Also add tests to demonstrate this added support.
Commit: 48bca8037985a9c430da354f5253718431553bda
https://github.com/acl2/acl2/commit/48bca8037985a9c430da354f5253718431553bda
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Extend characterization of formalized subset.
Match `exec-initer` for initializers.
Commit: 73c2be888a689ab9fab0bc0688196100a8f57295
https://github.com/acl2/acl2/commit/73c2be888a689ab9fab0bc0688196100a8f57295
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Extend characterization of formalized subset.
Update according to `exec-stmt`.
Commit: f378436caf88702a9bac7d06761c8fa9550c021e
https://github.com/acl2/acl2/commit/f378436caf88702a9bac7d06761c8fa9550c021e
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M acl2-fns.lisp
M axioms.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Improved error message for #!(foo) etc. Avoided hard Lisp errors from er calls.
Quoting :DOC note-8-7:
Improved the error message when the package name is missing
immediately after `#!', as in #!(foo).
Some ill-formed hard errors, for example from calls of er, caused raw
Lisp errors. This has been fixed. Thanks to Eric Smith for
reporting this bug with an example.
Commit: af571c5a54ed19fc8b2d17d4e519aca0ad10ec7d
https://github.com/acl2/acl2/commit/af571c5a54ed19fc8b2d17d4e519aca0ad10ec7d
Author: Eric McCarthy <bend...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
Log Message:
-----------
[axe] more comments on the abs test case
Commit: aae3d00a5921a356f2d16b9532a5b76aaf4e64e4
https://github.com/acl2/acl2/commit/aae3d00a5921a356f2d16b9532a5b76aaf4e64e4
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
Log Message:
-----------
Merge commit 'af571c5a54ed19fc8b2d17d4e519aca0ad10ec7d' into HEAD
Commit: fe7b58d59124ccd48d6fc58732d250e7aa46dd67
https://github.com/acl2/acl2/commit/fe7b58d59124ccd48d6fc58732d250e7aa46dd67
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M axioms.lisp
Log Message:
-----------
Improved on fix from earlier today, for error messages from certain bad er calls.
Commit: 557343f250cf6846ae9df7bbb7430e118768e798
https://github.com/acl2/acl2/commit/557343f250cf6846ae9df7bbb7430e118768e798
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
Log Message:
-----------
[C$] Remove some code no longer needed.
Commit: 16f40eb3df24146bd4d7aa5a0a43365ae6fc8223
https://github.com/acl2/acl2/commit/16f40eb3df24146bd4d7aa5a0a43365ae6fc8223
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
Log Message:
-----------
[C$] Remove some code no longer needed.
Commit: b9d8e0bbd889eb55c690ee0779fb7e17a0e6bb5b
https://github.com/acl2/acl2/commit/b9d8e0bbd889eb55c690ee0779fb7e17a0e6bb5b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
Log Message:
-----------
[C$] Improve formulation of formalized subset.
Avoid use of the `...-pure-formalp` predicates, which will be removed.
Commit: d1959f568073461030b6e987f5fd32f9096412a1
https://github.com/acl2/acl2/commit/d1959f568073461030b6e987f5fd32f9096412a1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Remove some code no longer needed.
Commit: d2dd755c28f0ed79131b046c06c6f5bf1c4d2e66
https://github.com/acl2/acl2/commit/d2dd755c28f0ed79131b046c06c6f5bf1c4d2e66
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/ternary_int.c
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
Log Message:
-----------
[C2C] Extend proof generation.
Add support for non-pure conditional expressions.
We just had to remove the checks for purity, as everything else was already in
place.
Also add a test to demonstrate support.
Commit: aa917a1237e54a78796b584fe8b681ff76dbd6f3
https://github.com/acl2/acl2/commit/aa917a1237e54a78796b584fe8b681ff76dbd6f3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/tests/simpadd0/old/logand.c
Log Message:
-----------
[C2C] Tweak test.
Commit: d561de221862c72b0822aacc858e195803afa1bd
https://github.com/acl2/acl2/commit/d561de221862c72b0822aacc858e195803afa1bd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/gg.c
Log Message:
-----------
[C2C] Extend proof generation.
Add support for non-pure initializers.
We just had to remove the purity test, since everything else was already in
place.
Also add a test to demonstrate support.
Commit: 66d7fc9428a3accb51fd8049c22363855b6948e2
https://github.com/acl2/acl2/commit/66d7fc9428a3accb51fd8049c22363855b6948e2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/if.c
M books/kestrel/c/transformation/tests/simpadd0/old/ifelse.c
Log Message:
-----------
[C2C] Extend proof generation.
Add support for `if` and `if-else` with non-pure expression tests. We just had
to remove the purity checks, because everything else was already in place.
Also add some tests to demonstrate support.
Commit: 2605d85378d42a27d5a2cecdf49571427590ff93
https://github.com/acl2/acl2/commit/2605d85378d42a27d5a2cecdf49571427590ff93
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/tests/simpadd0/old/while.c
M books/kestrel/c/transformation/tests/simpadd0/while.lisp
Log Message:
-----------
[C2C] Add a test for `while` loops.
This demonstrates support for non-pure test expressions.
Commit: 295bc4a9cb39548a032d4fd69574601d30cbec24
https://github.com/acl2/acl2/commit/295bc4a9cb39548a032d4fd69574601d30cbec24
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/tests/simpadd0/dowhile.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/dowhile.c
Log Message:
-----------
[C2C] Add a test for `do-while` loops.
Demonstrate support for non-pure test expressions.
Commit: c6e3c8f4eb83993d92212c617de05e2dba27024a
https://github.com/acl2/acl2/commit/c6e3c8f4eb83993d92212c617de05e2dba27024a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/gg.c
Log Message:
-----------
[C2C] Improve a test.
Demonstrate support for non-pure return expressions.
Commit: daa977b6a3b9588e8993e542113a4a93c19c9320
https://github.com/acl2/acl2/commit/daa977b6a3b9588e8993e542113a4a93c19c9320
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Trim some hints in generated proofs.
Commit: 9322aec2bc6f8f6488ee8a7ad2d163e19a2ecdd5
https://github.com/acl2/acl2/commit/9322aec2bc6f8f6488ee8a7ad2d163e19a2ecdd5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)
Changed paths:
M acl2-fns.lisp
M axioms.lisp
M books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/d1486dbf67a4...9322aec2bc6f
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Dec 3, 2025, 11:10:29 AM (4 days ago) Dec 3
to acl2-...@googlegroups.com
Alessandro Coglio
Dec 3, 2025, 11:11:38 AM (4 days ago) Dec 3
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Dec 3, 2025, 2:02:50 PM (4 days ago) Dec 3
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
M axioms.lisp
Compare: https://github.com/acl2/acl2/compare/af571c5a54ed...9322aec2bc6f
Commit: f378436caf88702a9bac7d06761c8fa9550c021e
https://github.com/acl2/acl2/commit/f378436caf88702a9bac7d06761c8fa9550c021e
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
https://github.com/acl2/acl2/commit/f378436caf88702a9bac7d06761c8fa9550c021e
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M acl2-fns.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
Log Message:
-----------
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Improved error message for #!(foo) etc. Avoided hard Lisp errors from er calls.
Quoting :DOC note-8-7:
Improved the error message when the package name is missing
immediately after `#!', as in #!(foo).
Some ill-formed hard errors, for example from calls of er, caused raw
Lisp errors. This has been fixed. Thanks to Eric Smith for
reporting this bug with an example.
Quoting :DOC note-8-7:
Improved the error message when the package name is missing
immediately after `#!', as in #!(foo).
Some ill-formed hard errors, for example from calls of er, caused raw
Lisp errors. This has been fixed. Thanks to Eric Smith for
reporting this bug with an example.
Commit: aae3d00a5921a356f2d16b9532a5b76aaf4e64e4
https://github.com/acl2/acl2/commit/aae3d00a5921a356f2d16b9532a5b76aaf4e64e4
Author: ACL2 Build Server <acl2bui...@gmail.com>
https://github.com/acl2/acl2/commit/aae3d00a5921a356f2d16b9532a5b76aaf4e64e4
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
Changed paths:
M books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
Log Message:
-----------
Merge commit 'af571c5a54ed19fc8b2d17d4e519aca0ad10ec7d' into HEAD
Commit: fe7b58d59124ccd48d6fc58732d250e7aa46dd67
https://github.com/acl2/acl2/commit/fe7b58d59124ccd48d6fc58732d250e7aa46dd67
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Log Message:
-----------
Merge commit 'af571c5a54ed19fc8b2d17d4e519aca0ad10ec7d' into HEAD
Commit: fe7b58d59124ccd48d6fc58732d250e7aa46dd67
https://github.com/acl2/acl2/commit/fe7b58d59124ccd48d6fc58732d250e7aa46dd67
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
Changed paths:
M axioms.lisp
Log Message:
-----------
Improved on fix from earlier today, for error messages from certain bad er calls.
Log Message:
-----------
Improved on fix from earlier today, for error messages from certain bad er calls.
Alessandro Coglio
Dec 3, 2025, 3:54:50 PM (4 days ago) Dec 3
to acl2-...@googlegroups.com
Branch: refs/heads/testing-acl2s
Compare: https://github.com/acl2/acl2/compare/f378436caf88...9322aec2bc6f
Commit: af571c5a54ed19fc8b2d17d4e519aca0ad10ec7d
https://github.com/acl2/acl2/commit/af571c5a54ed19fc8b2d17d4e519aca0ad10ec7d
Author: Eric McCarthy <bend...@gmail.com>
https://github.com/acl2/acl2/commit/af571c5a54ed19fc8b2d17d4e519aca0ad10ec7d
Author: Eric McCarthy <bend...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)
Changed paths:
M books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
Log Message:
-----------
Changed paths:
M books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
Log Message:
-----------
[axe] more comments on the abs test case
Reply all
Reply to author
Forward
0 new messages