[acl2/acl2] d22901: [C] Refactor some code.
0 views
Skip to first unread message
acl2buildserver
Sep 16, 2025, 4:22:29 PM (9 days ago) Sep 16
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: d22901d4bfb969f99bbc973639a082037ba726c0
https://github.com/acl2/acl2/commit/d22901d4bfb969f99bbc973639a082037ba726c0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
A books/kestrel/c/language/frame-and-scope-peeling.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/language/variable-preservation-in-execution.lisp
Log Message:
-----------
[C] Refactor some code.
Put the functions to peel frames and scopes, with accompanying theorems, into a
dedicated file and XDOC topic.
Commit: ba9209d65399706cbbea0349e8319805af75e5cb
https://github.com/acl2/acl2/commit/ba9209d65399706cbbea0349e8319805af75e5cb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/top.lisp
R books/kestrel/c/language/variable-preservation-in-execution.lisp
A books/kestrel/c/language/variable-visibility-preservation.lisp
Log Message:
-----------
[C] Improve characterization of a property.
Commit: 2481bf5a9c8c7e149b7a2ec0867db01395df9d94
https://github.com/acl2/acl2/commit/2481bf5a9c8c7e149b7a2ec0867db01395df9d94
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add and extend some theorems.
Commit: 47ea33958b7d9b90343e170e5aad06c8bda933b0
https://github.com/acl2/acl2/commit/47ea33958b7d9b90343e170e5aad06c8bda933b0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Adapt some proofs.
Commit: c715e536c4968ee96a71f5e4344ba7332d7b85bb
https://github.com/acl2/acl2/commit/c715e536c4968ee96a71f5e4344ba7332d7b85bb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/object-designators.lisp
Log Message:
-----------
[C] Add a theorem about object designators.
Commit: 6755505650118eb6c25cdc57eb7a456ede57f3a5
https://github.com/acl2/acl2/commit/6755505650118eb6c25cdc57eb7a456ede57f3a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C] Extend a theorem.
Adapt a proof that uses the theorem.
Commit: eaddacfc298dbc58390e248b41ca1d9639da67f8
https://github.com/acl2/acl2/commit/eaddacfc298dbc58390e248b41ca1d9639da67f8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/axe/x86/tests/ndsu/README.md
A books/kestrel/axe/x86/tests/ndsu/run-tests-vpadd128.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-vpadd128.lisp
A books/kestrel/axe/x86/tests/ndsu/vpadd128.c
A books/kestrel/axe/x86/tests/ndsu/vpadd128.elf64
A books/kestrel/axe/x86/tests/ndsu/vpadd128.macho64
Log Message:
-----------
Merge.
Commit: 4baaff86b160c4bab0d47e921c7c32267c7026b2
https://github.com/acl2/acl2/commit/4baaff86b160c4bab0d47e921c7c32267c7026b2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add a theorem about `create-var`.
Commit: 5640db425c2db30bd143055ff1d48520d8067b70
https://github.com/acl2/acl2/commit/5640db425c2db30bd143055ff1d48520d8067b70
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add a theorem about `read-object` and `create-var`.
Commit: 3e61df7c504f3a0c1e417883624d3fa35d07af92
https://github.com/acl2/acl2/commit/3e61df7c504f3a0c1e417883624d3fa35d07af92
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/variable-visibility-preservation.lisp
Log Message:
-----------
[C] Fix doc and improve file layout.
Commit: fc2dd94bed266a89f254183bd6c1539ab089a274
https://github.com/acl2/acl2/commit/fc2dd94bed266a89f254183bd6c1539ab089a274
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/alists-light/lookup-equal.lisp
M books/kestrel/arithmetic-light/ash.lisp
M books/kestrel/axe/bitops-rules.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/bv/adder.lisp
M books/kestrel/bv/ash.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules4.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/sbvlt-rules.lisp
M books/kestrel/utilities/extend-pathname-dollar.lisp
Log Message:
-----------
Merge.
Commit: 835ebc629d5f84968f27b49ae388deca22590b1a
https://github.com/acl2/acl2/commit/835ebc629d5f84968f27b49ae388deca22590b1a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/input-files-doc.lisp
Log Message:
-----------
[C$] Clarify some `input-files` user doc.
Commit: c23047cdb70ce70d35a61b27c5f6a922cdd52575
https://github.com/acl2/acl2/commit/c23047cdb70ce70d35a61b27c5f6a922cdd52575
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/system/extend-pathname.lisp
Log Message:
-----------
Merge.
Commit: de5c65445ab3b9f56f57ea6e76977e488a1bdade
https://github.com/acl2/acl2/commit/de5c65445ab3b9f56f57ea6e76977e488a1bdade
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
A books/kestrel/c/language/frame-and-scope-peeling.lisp
M books/kestrel/c/language/object-designators.lisp
M books/kestrel/c/language/top.lisp
R books/kestrel/c/language/variable-preservation-in-execution.lisp
A books/kestrel/c/language/variable-visibility-preservation.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Merge commit 'c23047cdb70ce70d35a61b27c5f6a922cdd52575' into HEAD
Compare: https://github.com/acl2/acl2/compare/fc327bd7c20f...de5c65445ab3
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: d22901d4bfb969f99bbc973639a082037ba726c0
https://github.com/acl2/acl2/commit/d22901d4bfb969f99bbc973639a082037ba726c0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
A books/kestrel/c/language/frame-and-scope-peeling.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/language/variable-preservation-in-execution.lisp
Log Message:
-----------
[C] Refactor some code.
Put the functions to peel frames and scopes, with accompanying theorems, into a
dedicated file and XDOC topic.
Commit: ba9209d65399706cbbea0349e8319805af75e5cb
https://github.com/acl2/acl2/commit/ba9209d65399706cbbea0349e8319805af75e5cb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/top.lisp
R books/kestrel/c/language/variable-preservation-in-execution.lisp
A books/kestrel/c/language/variable-visibility-preservation.lisp
Log Message:
-----------
[C] Improve characterization of a property.
Commit: 2481bf5a9c8c7e149b7a2ec0867db01395df9d94
https://github.com/acl2/acl2/commit/2481bf5a9c8c7e149b7a2ec0867db01395df9d94
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add and extend some theorems.
Commit: 47ea33958b7d9b90343e170e5aad06c8bda933b0
https://github.com/acl2/acl2/commit/47ea33958b7d9b90343e170e5aad06c8bda933b0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Adapt some proofs.
Commit: c715e536c4968ee96a71f5e4344ba7332d7b85bb
https://github.com/acl2/acl2/commit/c715e536c4968ee96a71f5e4344ba7332d7b85bb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/object-designators.lisp
Log Message:
-----------
[C] Add a theorem about object designators.
Commit: 6755505650118eb6c25cdc57eb7a456ede57f3a5
https://github.com/acl2/acl2/commit/6755505650118eb6c25cdc57eb7a456ede57f3a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C] Extend a theorem.
Adapt a proof that uses the theorem.
Commit: eaddacfc298dbc58390e248b41ca1d9639da67f8
https://github.com/acl2/acl2/commit/eaddacfc298dbc58390e248b41ca1d9639da67f8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/axe/x86/tests/ndsu/README.md
A books/kestrel/axe/x86/tests/ndsu/run-tests-vpadd128.acl2
A books/kestrel/axe/x86/tests/ndsu/run-tests-vpadd128.lisp
A books/kestrel/axe/x86/tests/ndsu/vpadd128.c
A books/kestrel/axe/x86/tests/ndsu/vpadd128.elf64
A books/kestrel/axe/x86/tests/ndsu/vpadd128.macho64
Log Message:
-----------
Merge.
Commit: 4baaff86b160c4bab0d47e921c7c32267c7026b2
https://github.com/acl2/acl2/commit/4baaff86b160c4bab0d47e921c7c32267c7026b2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add a theorem about `create-var`.
Commit: 5640db425c2db30bd143055ff1d48520d8067b70
https://github.com/acl2/acl2/commit/5640db425c2db30bd143055ff1d48520d8067b70
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add a theorem about `read-object` and `create-var`.
Commit: 3e61df7c504f3a0c1e417883624d3fa35d07af92
https://github.com/acl2/acl2/commit/3e61df7c504f3a0c1e417883624d3fa35d07af92
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/variable-visibility-preservation.lisp
Log Message:
-----------
[C] Fix doc and improve file layout.
Commit: fc2dd94bed266a89f254183bd6c1539ab089a274
https://github.com/acl2/acl2/commit/fc2dd94bed266a89f254183bd6c1539ab089a274
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/alists-light/lookup-equal.lisp
M books/kestrel/arithmetic-light/ash.lisp
M books/kestrel/axe/bitops-rules.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/bv/adder.lisp
M books/kestrel/bv/ash.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules4.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/sbvlt-rules.lisp
M books/kestrel/utilities/extend-pathname-dollar.lisp
Log Message:
-----------
Merge.
Commit: 835ebc629d5f84968f27b49ae388deca22590b1a
https://github.com/acl2/acl2/commit/835ebc629d5f84968f27b49ae388deca22590b1a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/input-files-doc.lisp
Log Message:
-----------
[C$] Clarify some `input-files` user doc.
Commit: c23047cdb70ce70d35a61b27c5f6a922cdd52575
https://github.com/acl2/acl2/commit/c23047cdb70ce70d35a61b27c5f6a922cdd52575
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/system/extend-pathname.lisp
Log Message:
-----------
Merge.
Commit: de5c65445ab3b9f56f57ea6e76977e488a1bdade
https://github.com/acl2/acl2/commit/de5c65445ab3b9f56f57ea6e76977e488a1bdade
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
A books/kestrel/c/language/frame-and-scope-peeling.lisp
M books/kestrel/c/language/object-designators.lisp
M books/kestrel/c/language/top.lisp
R books/kestrel/c/language/variable-preservation-in-execution.lisp
A books/kestrel/c/language/variable-visibility-preservation.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Merge commit 'c23047cdb70ce70d35a61b27c5f6a922cdd52575' into HEAD
Compare: https://github.com/acl2/acl2/compare/fc327bd7c20f...de5c65445ab3
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
acl2buildserver
Sep 16, 2025, 4:23:34 PM (9 days ago) Sep 16
to acl2-...@googlegroups.com
Branch: refs/heads/testing
acl2buildserver
Sep 16, 2025, 4:36:25 PM (9 days ago) Sep 16
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Commit: fc327bd7c20f4d81ca7bcda2a9e9b3ac80855b14
https://github.com/acl2/acl2/commit/fc327bd7c20f4d81ca7bcda2a9e9b3ac80855b14
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Log Message:
-----------
Fix certification failure using devel build; now "make devel-check" succeeds.
Commit: de5c65445ab3b9f56f57ea6e76977e488a1bdade
https://github.com/acl2/acl2/commit/de5c65445ab3b9f56f57ea6e76977e488a1bdade
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
A books/kestrel/c/language/frame-and-scope-peeling.lisp
M books/kestrel/c/language/object-designators.lisp
M books/kestrel/c/language/top.lisp
R books/kestrel/c/language/variable-preservation-in-execution.lisp
A books/kestrel/c/language/variable-visibility-preservation.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Merge commit 'c23047cdb70ce70d35a61b27c5f6a922cdd52575' into HEAD
Compare: https://github.com/acl2/acl2/compare/924c97385fd3...de5c65445ab3
https://github.com/acl2/acl2/commit/fc327bd7c20f4d81ca7bcda2a9e9b3ac80855b14
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/system/apply/apply-prim.lisp
Changed paths:
Log Message:
-----------
Fix certification failure using devel build; now "make devel-check" succeeds.
Commit: de5c65445ab3b9f56f57ea6e76977e488a1bdade
https://github.com/acl2/acl2/commit/de5c65445ab3b9f56f57ea6e76977e488a1bdade
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
A books/kestrel/c/language/frame-and-scope-peeling.lisp
M books/kestrel/c/language/object-designators.lisp
M books/kestrel/c/language/top.lisp
R books/kestrel/c/language/variable-preservation-in-execution.lisp
A books/kestrel/c/language/variable-visibility-preservation.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Merge commit 'c23047cdb70ce70d35a61b27c5f6a922cdd52575' into HEAD
Alessandro Coglio
Sep 19, 2025, 12:54:08 PM (7 days ago) Sep 19
to acl2-...@googlegroups.com
Branch: refs/heads/testing-acl2s
Commit: 2a764a90edf6063f951751520bd90111b727a63b
https://github.com/acl2/acl2/commit/2a764a90edf6063f951751520bd90111b727a63b
Author: Eric Smith <ews...@gmail.com>
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/x86/canonical-unsigned.lisp
Log Message:
-----------
[axe/x86] Improve some axe-smt rules.
Commit: 3e61df7c504f3a0c1e417883624d3fa35d07af92
https://github.com/acl2/acl2/commit/3e61df7c504f3a0c1e417883624d3fa35d07af92
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/variable-visibility-preservation.lisp
Log Message:
-----------
[C] Fix doc and improve file layout.
Commit: 2aabc03b9f6ec60557e6236a40bf9a47bce182e5
https://github.com/acl2/acl2/commit/2aabc03b9f6ec60557e6236a40bf9a47bce182e5
Author: Eric Smith <ews...@gmail.com>
Log Message:
-----------
[x86] Standardize code.
Put :guards before :stobjs.
Commit: b67802f7a8173ac2bf5501abb2905e000c0c0e30
https://github.com/acl2/acl2/commit/b67802f7a8173ac2bf5501abb2905e000c0c0e30
Author: Eric Smith <ews...@gmail.com>
Log Message:
-----------
[axe/x86] Fix message.
Commit: 2d15f74a20630893a1bc3aeff72ad07e7d655c4e
https://github.com/acl2/acl2/commit/2d15f74a20630893a1bc3aeff72ad07e7d655c4e
Author: Eric Smith <ews...@gmail.com>
https://github.com/acl2/acl2/commit/d185b454b92fff51675bf619a7bc9632d6c3a622
Author: Eric Smith <ews...@gmail.com>
Log Message:
-----------
[axe] Improve printing.
Commit: 172298fbf5c92e96702ca910ae7372a02b2e49f8
https://github.com/acl2/acl2/commit/172298fbf5c92e96702ca910ae7372a02b2e49f8
Author: Eric Smith <ews...@gmail.com>
Log Message:
-----------
[axe/x86] Use SMT to show canonical.
Only as a last resort as SMT is much slower than rewriting.
Commit: 210771d4a80dd3b43bb61c60600450e6a3a0c61d
https://github.com/acl2/acl2/commit/210771d4a80dd3b43bb61c60600450e6a3a0c61d
Author: Eric Smith <ews...@gmail.com>
M books/kestrel/x86/read-over-write-rules64.lisp
Log Message:
-----------
[x86] Comment out some old rules.
Commit: 92df758098035a17b45cbdf1a9810730df81ffe3
https://github.com/acl2/acl2/commit/92df758098035a17b45cbdf1a9810730df81ffe3
Author: Grant Jurgensen <gr...@jurgensen.dev>
Commit: 6a523919f8e554a5df4ae38eb58e2a9400fe1921
https://github.com/acl2/acl2/commit/6a523919f8e554a5df4ae38eb58e2a9400fe1921
Author: Grant Jurgensen <gr...@jurgensen.dev>
Commit: fc2dd94bed266a89f254183bd6c1539ab089a274
https://github.com/acl2/acl2/commit/fc2dd94bed266a89f254183bd6c1539ab089a274
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/alists-light/lookup-equal.lisp
M books/kestrel/arithmetic-light/ash.lisp
M books/kestrel/axe/bitops-rules.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/bv/adder.lisp
M books/kestrel/bv/ash.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules4.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/sbvlt-rules.lisp
M books/kestrel/utilities/extend-pathname-dollar.lisp
Log Message:
-----------
Merge.
Commit: 924c97385fd31d9867b8678db857815fd2582c6e
https://github.com/acl2/acl2/commit/924c97385fd31d9867b8678db857815fd2582c6e
Author: MattKaufmann <kauf...@cs.utexas.edu>
Log Message:
-----------
Merge pull request #1847 from gjurgensen/gj-extend-pathname
[system] Localize in-theory event
Commit: 0cfc1db253e9b25dcf56872104a755d8a680cc21
https://github.com/acl2/acl2/commit/0cfc1db253e9b25dcf56872104a755d8a680cc21
Commit: c8ce726fa64373963e0d4e6e8f93452f4824a8cb
https://github.com/acl2/acl2/commit/c8ce726fa64373963e0d4e6e8f93452f4824a8cb
Author: Eric Smith <ews...@gmail.com>
https://github.com/acl2/acl2/commit/04d08bb21b1072f8bf4845e0d69f79e6c174d696
Commit: 17bb71e776bc6d255c93433d47434379e7b5bd7e
https://github.com/acl2/acl2/commit/17bb71e776bc6d255c93433d47434379e7b5bd7e
M books/kestrel/c/language/top.lisp
Log Message:
-----------
[C] Add some general theorems about execution.
These are about the preservation of existing objects and their types.
Commit: 230bb71a6da9d3a516db31a7ab002605feec4077
https://github.com/acl2/acl2/commit/230bb71a6da9d3a516db31a7ab002605feec4077
Log Message:
-----------
Merge.
Commit: 0c29896f0f11ab2f4090cf423b8fa776104c4ba5
https://github.com/acl2/acl2/commit/0c29896f0f11ab2f4090cf423b8fa776104c4ba5
Author: Eric Smith <ews...@gmail.com>
Commit: 07e67fe00ff8efcac56e5db500bb3d71b55d6cac
https://github.com/acl2/acl2/commit/07e67fe00ff8efcac56e5db500bb3d71b55d6cac
Author: Eric Smith <ews...@gmail.com>
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-and-write2.lisp
Log Message:
-----------
[axe/x86] Slightly improve read and write machinery.
Commit: af2381701ba91cd12ae067d0f3d2fad80d463103
https://github.com/acl2/acl2/commit/af2381701ba91cd12ae067d0f3d2fad80d463103
Log Message:
-----------
[C] Remove local events no longer needed.
Commit: 3837b828581f207f6ef7b05326a05d69cfe8c5ee
https://github.com/acl2/acl2/commit/3837b828581f207f6ef7b05326a05d69cfe8c5ee
Log Message:
-----------
[C] Eliminate some unnecessary hypotheses.
Commit: 68c6c754667c5c232fe2ea06439aea8b715ced38
https://github.com/acl2/acl2/commit/68c6c754667c5c232fe2ea06439aea8b715ced38
Log Message:
-----------
[C] Remove some unnecessary hypotheses.
Commit: 39b3b650daa7cdd3935a8df764651ce6ea7e042f
https://github.com/acl2/acl2/commit/39b3b650daa7cdd3935a8df764651ce6ea7e042f
Author: Yahya Sohail <ya...@yahyasohail.com>
M books/projects/x86isa/linux/doc.lisp
Log Message:
-----------
Clarify x86isa model build instructions in context of Linux boot
Commit: 7919f043f8904229171b3e67ce9aa4adbacb71fc
https://github.com/acl2/acl2/commit/7919f043f8904229171b3e67ce9aa4adbacb71fc
Log Message:
-----------
[C] Add a theorem.
Commit: 62f4046ebc239478f00065ff6d85ec10760add6b
https://github.com/acl2/acl2/commit/62f4046ebc239478f00065ff6d85ec10760add6b
Log Message:
-----------
[C] Fix two XDOC links.
Commit: 7436ac2bee83cae3820b99d55dd9cb54b1857eac
https://github.com/acl2/acl2/commit/7436ac2bee83cae3820b99d55dd9cb54b1857eac
Log Message:
-----------
[C] Tweak ordering.
Commit: 94d8185d494f10d4be6ad46baf4efb95b7e897ae
https://github.com/acl2/acl2/commit/94d8185d494f10d4be6ad46baf4efb95b7e897ae
Author: Yahya Sohail <ya...@yahyasohail.com>
M books/projects/x86isa/linux/doc.lisp
Log Message:
-----------
Merge pull request #1846 from yaso9/x86isa-build-doc-update
Clarify x86isa model build instructions in context of Linux boot
Commit: 44cc70a4def35a08c21034a0d6bbacd56b408e5f
https://github.com/acl2/acl2/commit/44cc70a4def35a08c21034a0d6bbacd56b408e5f
Commit: 892e948bef1001793859ef347370240e43031f9b
https://github.com/acl2/acl2/commit/892e948bef1001793859ef347370240e43031f9b
Log Message:
-----------
[C] Improve some names.
Commit: bfb78a2b9c7b6da1a2c46354116accb3dbb2b483
https://github.com/acl2/acl2/commit/bfb78a2b9c7b6da1a2c46354116accb3dbb2b483
Log Message:
-----------
[C] Improve some names.
Commit: fb1d1e683e99c7458dd544442e0b4af52088cb83
https://github.com/acl2/acl2/commit/fb1d1e683e99c7458dd544442e0b4af52088cb83
Commit: 5ee7bed3c1b5ad33828e9f65887e9b36d175d405
https://github.com/acl2/acl2/commit/5ee7bed3c1b5ad33828e9f65887e9b36d175d405
A books/kestrel/c/language/variable-resolution-preservation.lisp
Log Message:
-----------
[C] Add theorems about the dynamic semantics.
These are about the preservation of variable resolution, which needs to be
suitably weakened for the execution of object declarations, block items, and
lists of block items.
Commit: 006f00dfb07e363e41a269f32ba2f71f1642b6a8
https://github.com/acl2/acl2/commit/006f00dfb07e363e41a269f32ba2f71f1642b6a8
M books/projects/x86isa/linux/doc.lisp
Log Message:
-----------
Merge.
Commit: 30100ed4083070fe6d14fb3f7e556df5039eafdd
https://github.com/acl2/acl2/commit/30100ed4083070fe6d14fb3f7e556df5039eafdd
Log Message:
-----------
[C] Fix XDOC typo.
Commit: b4417ac5a13081a1c2c420045c22678f64a121bb
https://github.com/acl2/acl2/commit/b4417ac5a13081a1c2c420045c22678f64a121bb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Improve/fix some doc.
Also include files that will be used shortly.
Commit: fa269ec4747523bc0cc478f6b96be6785b9a4e93
https://github.com/acl2/acl2/commit/fa269ec4747523bc0cc478f6b96be6785b9a4e93
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
M books/kestrel/c/language/frame-and-scope-peeling.lisp
A books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/top.lisp
A books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp
M books/projects/x86isa/doc.lisp
M books/projects/x86isa/linux/doc.lisp
Log Message:
-----------
Merge.
Commit: 81548f69f15a38f228719f678aab0a126f0dd613
https://github.com/acl2/acl2/commit/81548f69f15a38f228719f678aab0a126f0dd613
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
Commit: fafadef51473241b4a449139048561557f8ffaf1
https://github.com/acl2/acl2/commit/fafadef51473241b4a449139048561557f8ffaf1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Simplify a supporting theorem proof.
Commit: 10b47436d341b69645b6c90e497b949b9df11743
https://github.com/acl2/acl2/commit/10b47436d341b69645b6c90e497b949b9df11743
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Slightly weaken some intermediate theorems.
Add hypotheses saying that there is at least one frame, for the theorems about
the execution of constructs in a function's body. The top-level theorems for
functions are not weakened; their proofs are just slightly extended to establish
the non-emptiness of the frame stack in the body (since the function is
executing, there is a frame for it).
Adapt the proofs of the intermediate theorems to propagate the new hypotheses
when composing sub-proofs for sub-constructs.
This added hypotheses are needed for upcoming extensions, whose supporting
theorems have those hypotheses.
Commit: f6a3bf78e658be904fac6ea69ccc3bb860dabecf
https://github.com/acl2/acl2/commit/f6a3bf78e658be904fac6ea69ccc3bb860dabecf
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/read-and-write2.lisp
Log Message:
-----------
[x86] Move some rules.
Commit: 6ff4e6617459fcbf1ca3b8afdc30b74b1221da8c
https://github.com/acl2/acl2/commit/6ff4e6617459fcbf1ca3b8afdc30b74b1221da8c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Slightly weaken a theorem and simplify its proof.
Commit: a0d0639452a4bd925d0b92a9756e9cc8c931fd44
https://github.com/acl2/acl2/commit/a0d0639452a4bd925d0b92a9756e9cc8c931fd44
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Tweak hints for consistency.
Commit: 086e680c2bff6f1fbfed84118b753ad450fd9771
https://github.com/acl2/acl2/commit/086e680c2bff6f1fbfed84118b753ad450fd9771
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Tweak theorem formulation for consistency.
Commit: 1b482df5e0d313820017c8f81759045ca2d41a0c
https://github.com/acl2/acl2/commit/1b482df5e0d313820017c8f81759045ca2d41a0c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Tweak a theorem and simplify a proof.
Commit: fcd7ede83503886897a519dda7db5feb6e89f3ae
https://github.com/acl2/acl2/commit/fcd7ede83503886897a519dda7db5feb6e89f3ae
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/read-and-write2.lisp
Log Message:
-----------
[x86] Generalize 2 rules.
Commit: 8266d3cf9d5f5b28b261be42c2e3948fb3b865a8
https://github.com/acl2/acl2/commit/8266d3cf9d5f5b28b261be42c2e3948fb3b865a8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
A books/kestrel/c/language/implementation-environments/bool-formats.lisp
M books/kestrel/c/language/implementation-environments/top.lisp
Log Message:
-----------
[C] Formalize `_Bool` formats.
Commit: 5286eb5b5ed663f6bb01ca674b04ba67061e4db0
https://github.com/acl2/acl2/commit/5286eb5b5ed663f6bb01ca674b04ba67061e4db0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments/integer-formats.lisp
M books/kestrel/c/language/implementation-environments/top.lisp
Log Message:
-----------
[C] Extend implementation environments.
Include the `_Bool` format into the implementation environment.
Commit: e67f3f5191b518eb0ceff0d206237bb39a9e8d0c
https://github.com/acl2/acl2/commit/e67f3f5191b518eb0ceff0d206237bb39a9e8d0c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments/top.lisp
Log Message:
-----------
[C] Add two operations on implementation environments.
Commit: 56eafc62327cbe0ba3237145ecf0cce82c0140a8
https://github.com/acl2/acl2/commit/56eafc62327cbe0ba3237145ecf0cce82c0140a8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/simpadd0.lisp
Add supporting theorems.
Extend implementation, but something else needs to be done before making that
active.
Commit: e6a3232a21a8672172d44e746dc0994004e9cdf4
https://github.com/acl2/acl2/commit/e6a3232a21a8672172d44e746dc0994004e9cdf4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Improve generated proofs.
For lists of block items, avoid generating assertions about variables at the end
of the block items. We are not tracking them, also because they are not needed,
given that scopes end at the end of the lists of block items.
Commit: e9afbf6e15f6460c1d6613f11cc66cb8f18542b0
https://github.com/acl2/acl2/commit/e9afbf6e15f6460c1d6613f11cc66cb8f18542b0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Add more support for compound statements.
Refine the generated proof hints.
Commit: 599a7420d2ed9b3ab396eb77f860f5d29fe0990a
https://github.com/acl2/acl2/commit/599a7420d2ed9b3ab396eb77f860f5d29fe0990a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-and-write2.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
Log Message:
-----------
Merge.
Commit: 8588ed520b59d73ee03fe3c213b8764f3a36be62
https://github.com/acl2/acl2/commit/8588ed520b59d73ee03fe3c213b8764f3a36be62
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
A books/kestrel/c/syntax/disambiguation.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/unambiguity.lisp
Log Message:
-----------
[C$] Add new file and topic for disambiguation.
Put unambiguity and disambiguator under it.
Commit: 237effbc5db778e6feeaf40529459a176360419f
https://github.com/acl2/acl2/commit/237effbc5db778e6feeaf40529459a176360419f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add a theorem.
Commit: 8b7bb47f0825f76ffc60d21317bcb72d72803888
https://github.com/acl2/acl2/commit/8b7bb47f0825f76ffc60d21317bcb72d72803888
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/atc/symbolic-computation-states.lisp
M books/kestrel/c/atc/theorem-generation.lisp
Log Message:
-----------
[ATC] Rename a theorem.
Commit: ea220e05a067ddd68c178801cd5f8a889169ac9f
https://github.com/acl2/acl2/commit/ea220e05a067ddd68c178801cd5f8a889169ac9f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-and-write2.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
Log Message:
-----------
Merge.
Commit: b91c6105dc90ce7100439e1fae965330b9d04a3b
https://github.com/acl2/acl2/commit/b91c6105dc90ce7100439e1fae965330b9d04a3b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add a theorem.
Commit: f3fe2b93add52ebda1c715cc02c3468b33c837d7
https://github.com/acl2/acl2/commit/f3fe2b93add52ebda1c715cc02c3468b33c837d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Add supporting theorem.
Commit: c700cd51a3240ff805dd3ee6ef7b6f0f12ce525b
https://github.com/acl2/acl2/commit/c700cd51a3240ff805dd3ee6ef7b6f0f12ce525b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.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/formalized.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/standard.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/split-all-gso.lisp
M books/kestrel/c/transformation/splitgso.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: 07a74b822d18541d2725ee486ead4f6fba8d26c7
https://github.com/acl2/acl2/commit/07a74b822d18541d2725ee486ead4f6fba8d26c7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.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/formalized.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/standard.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/split-all-gso.lisp
M books/kestrel/c/transformation/splitgso.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: 0c24c52f2e1e68a18a23c6f49b79e51328215110
https://github.com/acl2/acl2/commit/0c24c52f2e1e68a18a23c6f49b79e51328215110
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/parser.lisp
Log Message:
-----------
[C$] Improve name of a lexing function.
Commit: 9d3706c7c83015d369a80177042d020657507733
https://github.com/acl2/acl2/commit/9d3706c7c83015d369a80177042d020657507733
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/tests/parser.lisp
Log Message:
-----------
[C$] Add some lexer tests.
Commit: a202b1dfd0bfc636ce0a23f06ce28d0941c1b132
https://github.com/acl2/acl2/commit/a202b1dfd0bfc636ce0a23f06ce28d0941c1b132
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
Log Message:
-----------
[C$] Extend type calculation from annotation.
Add support for compound statements.
Commit: f48772e275f70d15e4e54acbe775603dddde1117
https://github.com/acl2/acl2/commit/f48772e275f70d15e4e54acbe775603dddde1117
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Extend `simpadd0` proof generation.
Finish adding support for compound statements.
Commit: 2745ff12deea6814afc5a73324250001d0ec0996
https://github.com/acl2/acl2/commit/2745ff12deea6814afc5a73324250001d0ec0996
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
A books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
A books/kestrel/c/transformation/tests/simpadd0/old/blocks.c
Log Message:
-----------
[C2C] Add `simpadd0` tests for compound statements.
Commit: 672df7ce4c63c24e948885fbd572bc022bb6a228
https://github.com/acl2/acl2/commit/672df7ce4c63c24e948885fbd572bc022bb6a228
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
A books/kestrel/c/syntax/disambiguation.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.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/standard.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/unambiguity.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/split-all-gso.lisp
M books/kestrel/c/transformation/splitgso.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
Merge.
Commit: c29dd1ff6ad43fd1666706931defdb973f351398
https://github.com/acl2/acl2/commit/c29dd1ff6ad43fd1666706931defdb973f351398
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
A books/kestrel/c/language/implementation-environments/bool-formats.lisp
M books/kestrel/c/language/implementation-environments/integer-formats.lisp
M books/kestrel/c/language/implementation-environments/top.lisp
Log Message:
-----------
Merge.
Commit: f612b1eed0ff959c195c364a198b95911e448c38
https://github.com/acl2/acl2/commit/f612b1eed0ff959c195c364a198b95911e448c38
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
Log Message:
-----------
[C$] Adapt to extension of implementation environments.
Commit: 300d80db68d1aa206805b71f682900406cff444f
https://github.com/acl2/acl2/commit/300d80db68d1aa206805b71f682900406cff444f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-18 (Thu, 18 Sep 2025)
Changed paths:
M books/kestrel/json-parser/parse-json.lisp
M books/kestrel/utilities/make-ord.lisp
Log Message:
-----------
[utilities] Collect some rules about make-ord.
Commit: 28df1b052313e7b65c6f2bdce9a57516f51f4c84
https://github.com/acl2/acl2/commit/28df1b052313e7b65c6f2bdce9a57516f51f4c84
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-18 (Thu, 18 Sep 2025)
Changed paths:
M books/kestrel/axe/x86/examples/add/add-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/formal-unit-tests/add/run-test.lisp
M books/kestrel/axe/x86/examples/tea/tea-elf64.lisp
M books/kestrel/axe/x86/examples/tea/tea-macho64.lisp
Log Message:
-----------
[axe/x86] Exclude some examples when STP is not installed.
Thanks to Matt Kaufmann for reporting this issue.
Commit: b5c997467e781217b5228f3918fe0b684c759f6a
https://github.com/acl2/acl2/commit/b5c997467e781217b5228f3918fe0b684c759f6a
Changed paths:
M books/kestrel/axe/x86/examples/add/add-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/formal-unit-tests/add/run-test.lisp
M books/kestrel/axe/x86/examples/tea/tea-elf64.lisp
M books/kestrel/axe/x86/examples/tea/tea-macho64.lisp
M books/kestrel/json-parser/parse-json.lisp
M books/kestrel/utilities/make-ord.lisp
Log Message:
-----------
Merge commit '28df1b052313e7b65c6f2bdce9a57516f51f4c84' into HEAD
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: 839bfa97dfb9911ab7c1f1da4d74152cc7a01e4d
https://github.com/acl2/acl2/commit/839bfa97dfb9911ab7c1f1da4d74152cc7a01e4d
Author: Grant Jurgensen <gr...@jurgensen.dev>
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:
-----------
[C$] Add compilation database utilities
The JSON compilation database file format is used by the clang
ecosystem. See the newly introduced xdoc for more information.
Commit: 059564e9b1525347427e86d430d1cd4dacc6d56b
https://github.com/acl2/acl2/commit/059564e9b1525347427e86d430d1cd4dacc6d56b
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
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
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
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
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
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
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
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
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
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
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
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
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
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
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/8fbaeed3ce10...9d7049f4c90b
https://github.com/acl2/acl2/commit/2a764a90edf6063f951751520bd90111b727a63b
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
Changed paths:
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/x86/canonical-unsigned.lisp
Log Message:
-----------
[axe/x86] Improve some axe-smt rules.
Commit: 3e61df7c504f3a0c1e417883624d3fa35d07af92
https://github.com/acl2/acl2/commit/3e61df7c504f3a0c1e417883624d3fa35d07af92
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/c/language/variable-visibility-preservation.lisp
Log Message:
-----------
[C] Fix doc and improve file layout.
https://github.com/acl2/acl2/commit/2aabc03b9f6ec60557e6236a40bf9a47bce182e5
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/x86/read-and-write.lisp
Changed paths:
Log Message:
-----------
[x86] Standardize code.
Put :guards before :stobjs.
Commit: b67802f7a8173ac2bf5501abb2905e000c0c0e30
https://github.com/acl2/acl2/commit/b67802f7a8173ac2bf5501abb2905e000c0c0e30
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
M books/kestrel/axe/x86/unroll-x86-code.lisp
Changed paths:
Log Message:
-----------
[axe/x86] Fix message.
Commit: 2d15f74a20630893a1bc3aeff72ad07e7d655c4e
https://github.com/acl2/acl2/commit/2d15f74a20630893a1bc3aeff72ad07e7d655c4e
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-15 (Mon, 15 Sep 2025)
Changed paths:
Changed paths:
M books/kestrel/alists-light/lookup-equal.lisp
M books/kestrel/arithmetic-light/ash.lisp
M books/kestrel/axe/bitops-rules.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/bv/adder.lisp
M books/kestrel/bv/ash.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules4.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/sbvlt-rules.lisp
M books/kestrel/utilities/extend-pathname-dollar.lisp
Log Message:
-----------
Merge.
Commit: d185b454b92fff51675bf619a7bc9632d6c3a622
M books/kestrel/arithmetic-light/ash.lisp
M books/kestrel/axe/bitops-rules.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/bv/adder.lisp
M books/kestrel/bv/ash.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules4.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/sbvlt-rules.lisp
M books/kestrel/utilities/extend-pathname-dollar.lisp
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/d185b454b92fff51675bf619a7bc9632d6c3a622
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/axe/make-rewriter-simple.lisp
Changed paths:
Log Message:
-----------
[axe] Improve printing.
Commit: 172298fbf5c92e96702ca910ae7372a02b2e49f8
https://github.com/acl2/acl2/commit/172298fbf5c92e96702ca910ae7372a02b2e49f8
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
Changed paths:
Log Message:
-----------
[axe/x86] Use SMT to show canonical.
Only as a last resort as SMT is much slower than rewriting.
Commit: 210771d4a80dd3b43bb61c60600450e6a3a0c61d
https://github.com/acl2/acl2/commit/210771d4a80dd3b43bb61c60600450e6a3a0c61d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/x86/read-and-write.lisp
Changed paths:
M books/kestrel/x86/read-over-write-rules64.lisp
Log Message:
-----------
[x86] Comment out some old rules.
Commit: 92df758098035a17b45cbdf1a9810730df81ffe3
https://github.com/acl2/acl2/commit/92df758098035a17b45cbdf1a9810730df81ffe3
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/system/extend-pathname.lisp
Log Message:
-----------
[system] Localize in-theory event
Changed paths:
M books/system/extend-pathname.lisp
Log Message:
-----------
Commit: 6a523919f8e554a5df4ae38eb58e2a9400fe1921
https://github.com/acl2/acl2/commit/6a523919f8e554a5df4ae38eb58e2a9400fe1921
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/system/extend-pathname.lisp
Log Message:
-----------
[system] Remove verify-termination of on logic-mode function
Changed paths:
M books/system/extend-pathname.lisp
Log Message:
-----------
Commit: fc2dd94bed266a89f254183bd6c1539ab089a274
https://github.com/acl2/acl2/commit/fc2dd94bed266a89f254183bd6c1539ab089a274
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/alists-light/lookup-equal.lisp
M books/kestrel/arithmetic-light/ash.lisp
M books/kestrel/axe/bitops-rules.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/bv/adder.lisp
M books/kestrel/bv/ash.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules4.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/sbvlt-rules.lisp
M books/kestrel/utilities/extend-pathname-dollar.lisp
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/924c97385fd31d9867b8678db857815fd2582c6e
Author: MattKaufmann <kauf...@cs.utexas.edu>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/system/extend-pathname.lisp
Changed paths:
Log Message:
-----------
Merge pull request #1847 from gjurgensen/gj-extend-pathname
[system] Localize in-theory event
https://github.com/acl2/acl2/commit/0cfc1db253e9b25dcf56872104a755d8a680cc21
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Tweak code layout.
Log Message:
-----------
Commit: c8ce726fa64373963e0d4e6e8f93452f4824a8cb
https://github.com/acl2/acl2/commit/c8ce726fa64373963e0d4e6e8f93452f4824a8cb
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/system/extend-pathname.lisp
Log Message:
-----------
Merge.
Commit: 04d08bb21b1072f8bf4845e0d69f79e6c174d696
Changed paths:
M books/system/extend-pathname.lisp
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/04d08bb21b1072f8bf4845e0d69f79e6c174d696
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add a theorem about `read-object` and `write-object`.
Log Message:
-----------
Commit: 17bb71e776bc6d255c93433d47434379e7b5bd7e
https://github.com/acl2/acl2/commit/17bb71e776bc6d255c93433d47434379e7b5bd7e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
A books/kestrel/c/language/object-type-preservation.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/top.lisp
Log Message:
-----------
[C] Add some general theorems about execution.
These are about the preservation of existing objects and their types.
Commit: 230bb71a6da9d3a516db31a7ab002605feec4077
https://github.com/acl2/acl2/commit/230bb71a6da9d3a516db31a7ab002605feec4077
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/system/apply/apply-prim.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Log Message:
-----------
Merge.
Commit: 0c29896f0f11ab2f4090cf423b8fa776104c4ba5
https://github.com/acl2/acl2/commit/0c29896f0f11ab2f4090cf423b8fa776104c4ba5
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
A books/kestrel/c/language/frame-and-scope-peeling.lisp
M books/kestrel/c/language/object-designators.lisp
M books/kestrel/c/language/top.lisp
R books/kestrel/c/language/variable-preservation-in-execution.lisp
A books/kestrel/c/language/variable-visibility-preservation.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Changed paths:
M books/kestrel/c/language/computation-states.lisp
A books/kestrel/c/language/frame-and-scope-peeling.lisp
M books/kestrel/c/language/object-designators.lisp
M books/kestrel/c/language/top.lisp
R books/kestrel/c/language/variable-preservation-in-execution.lisp
A books/kestrel/c/language/variable-visibility-preservation.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
M books/system/apply/apply-prim.lisp
Log Message:
-----------
Merge.
Log Message:
-----------
Commit: 07e67fe00ff8efcac56e5db500bb3d71b55d6cac
https://github.com/acl2/acl2/commit/07e67fe00ff8efcac56e5db500bb3d71b55d6cac
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/axe/x86/x86-rules.lisp
Changed paths:
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-and-write2.lisp
Log Message:
-----------
[axe/x86] Slightly improve read and write machinery.
Commit: af2381701ba91cd12ae067d0f3d2fad80d463103
https://github.com/acl2/acl2/commit/af2381701ba91cd12ae067d0f3d2fad80d463103
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/object-type-preservation.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Log Message:
-----------
[C] Remove local events no longer needed.
Commit: 3837b828581f207f6ef7b05326a05d69cfe8c5ee
https://github.com/acl2/acl2/commit/3837b828581f207f6ef7b05326a05d69cfe8c5ee
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/variable-visibility-preservation.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Log Message:
-----------
[C] Eliminate some unnecessary hypotheses.
Commit: 68c6c754667c5c232fe2ea06439aea8b715ced38
https://github.com/acl2/acl2/commit/68c6c754667c5c232fe2ea06439aea8b715ced38
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/object-type-preservation.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Log Message:
-----------
[C] Remove some unnecessary hypotheses.
Commit: 39b3b650daa7cdd3935a8df764651ce6ea7e042f
https://github.com/acl2/acl2/commit/39b3b650daa7cdd3935a8df764651ce6ea7e042f
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/projects/x86isa/doc.lisp
Changed paths:
M books/projects/x86isa/linux/doc.lisp
Log Message:
-----------
Clarify x86isa model build instructions in context of Linux boot
Commit: 7919f043f8904229171b3e67ce9aa4adbacb71fc
https://github.com/acl2/acl2/commit/7919f043f8904229171b3e67ce9aa4adbacb71fc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/frame-and-scope-peeling.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Log Message:
-----------
[C] Add a theorem.
Commit: 62f4046ebc239478f00065ff6d85ec10760add6b
https://github.com/acl2/acl2/commit/62f4046ebc239478f00065ff6d85ec10760add6b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/object-type-preservation.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Log Message:
-----------
[C] Fix two XDOC links.
Commit: 7436ac2bee83cae3820b99d55dd9cb54b1857eac
https://github.com/acl2/acl2/commit/7436ac2bee83cae3820b99d55dd9cb54b1857eac
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/frame-and-scope-peeling.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Log Message:
-----------
[C] Tweak ordering.
Commit: 94d8185d494f10d4be6ad46baf4efb95b7e897ae
https://github.com/acl2/acl2/commit/94d8185d494f10d4be6ad46baf4efb95b7e897ae
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/projects/x86isa/doc.lisp
Changed paths:
M books/projects/x86isa/linux/doc.lisp
Log Message:
-----------
Merge pull request #1846 from yaso9/x86isa-build-doc-update
Clarify x86isa model build instructions in context of Linux boot
Commit: 44cc70a4def35a08c21034a0d6bbacd56b408e5f
https://github.com/acl2/acl2/commit/44cc70a4def35a08c21034a0d6bbacd56b408e5f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add a theorem.
Log Message:
-----------
Commit: 892e948bef1001793859ef347370240e43031f9b
https://github.com/acl2/acl2/commit/892e948bef1001793859ef347370240e43031f9b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/variable-visibility-preservation.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Log Message:
-----------
[C] Improve some names.
Commit: bfb78a2b9c7b6da1a2c46354116accb3dbb2b483
https://github.com/acl2/acl2/commit/bfb78a2b9c7b6da1a2c46354116accb3dbb2b483
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/variable-visibility-preservation.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Log Message:
-----------
[C] Improve some names.
Commit: fb1d1e683e99c7458dd544442e0b4af52088cb83
https://github.com/acl2/acl2/commit/fb1d1e683e99c7458dd544442e0b4af52088cb83
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/object-type-preservation.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/variable-visibility-preservation.lisp
Log Message:
-----------
[C] Reorder some theorems for consistency.
Log Message:
-----------
Commit: 5ee7bed3c1b5ad33828e9f65887e9b36d175d405
https://github.com/acl2/acl2/commit/5ee7bed3c1b5ad33828e9f65887e9b36d175d405
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/top.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
A books/kestrel/c/language/variable-resolution-preservation.lisp
Log Message:
-----------
[C] Add theorems about the dynamic semantics.
These are about the preservation of variable resolution, which needs to be
suitably weakened for the execution of object declarations, block items, and
lists of block items.
Commit: 006f00dfb07e363e41a269f32ba2f71f1642b6a8
https://github.com/acl2/acl2/commit/006f00dfb07e363e41a269f32ba2f71f1642b6a8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/projects/x86isa/doc.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/projects/x86isa/linux/doc.lisp
Log Message:
-----------
Merge.
Commit: 30100ed4083070fe6d14fb3f7e556df5039eafdd
https://github.com/acl2/acl2/commit/30100ed4083070fe6d14fb3f7e556df5039eafdd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/c/language/variable-resolution-preservation.lisp
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
Log Message:
-----------
[C] Fix XDOC typo.
Commit: b4417ac5a13081a1c2c420045c22678f64a121bb
https://github.com/acl2/acl2/commit/b4417ac5a13081a1c2c420045c22678f64a121bb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Also include files that will be used shortly.
Commit: fa269ec4747523bc0cc478f6b96be6785b9a4e93
https://github.com/acl2/acl2/commit/fa269ec4747523bc0cc478f6b96be6785b9a4e93
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
M books/kestrel/c/language/frame-and-scope-peeling.lisp
A books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/top.lisp
A books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp
M books/projects/x86isa/doc.lisp
M books/projects/x86isa/linux/doc.lisp
Log Message:
-----------
Merge.
Commit: 81548f69f15a38f228719f678aab0a126f0dd613
https://github.com/acl2/acl2/commit/81548f69f15a38f228719f678aab0a126f0dd613
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp
Log Message:
-----------
[C] Strengthen some theorems.
Log Message:
-----------
Commit: fafadef51473241b4a449139048561557f8ffaf1
https://github.com/acl2/acl2/commit/fafadef51473241b4a449139048561557f8ffaf1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Commit: 10b47436d341b69645b6c90e497b949b9df11743
https://github.com/acl2/acl2/commit/10b47436d341b69645b6c90e497b949b9df11743
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Slightly weaken some intermediate theorems.
Add hypotheses saying that there is at least one frame, for the theorems about
the execution of constructs in a function's body. The top-level theorems for
functions are not weakened; their proofs are just slightly extended to establish
the non-emptiness of the frame stack in the body (since the function is
executing, there is a frame for it).
Adapt the proofs of the intermediate theorems to propagate the new hypotheses
when composing sub-proofs for sub-constructs.
This added hypotheses are needed for upcoming extensions, whose supporting
theorems have those hypotheses.
Commit: f6a3bf78e658be904fac6ea69ccc3bb860dabecf
https://github.com/acl2/acl2/commit/f6a3bf78e658be904fac6ea69ccc3bb860dabecf
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/read-and-write2.lisp
Log Message:
-----------
[x86] Move some rules.
Commit: 6ff4e6617459fcbf1ca3b8afdc30b74b1221da8c
https://github.com/acl2/acl2/commit/6ff4e6617459fcbf1ca3b8afdc30b74b1221da8c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Commit: a0d0639452a4bd925d0b92a9756e9cc8c931fd44
https://github.com/acl2/acl2/commit/a0d0639452a4bd925d0b92a9756e9cc8c931fd44
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Commit: 086e680c2bff6f1fbfed84118b753ad450fd9771
https://github.com/acl2/acl2/commit/086e680c2bff6f1fbfed84118b753ad450fd9771
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Commit: 1b482df5e0d313820017c8f81759045ca2d41a0c
https://github.com/acl2/acl2/commit/1b482df5e0d313820017c8f81759045ca2d41a0c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Commit: fcd7ede83503886897a519dda7db5feb6e89f3ae
https://github.com/acl2/acl2/commit/fcd7ede83503886897a519dda7db5feb6e89f3ae
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/read-and-write2.lisp
Log Message:
-----------
[x86] Generalize 2 rules.
Commit: 8266d3cf9d5f5b28b261be42c2e3948fb3b865a8
https://github.com/acl2/acl2/commit/8266d3cf9d5f5b28b261be42c2e3948fb3b865a8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
A books/kestrel/c/language/implementation-environments/bool-formats.lisp
M books/kestrel/c/language/implementation-environments/top.lisp
Log Message:
-----------
[C] Formalize `_Bool` formats.
Commit: 5286eb5b5ed663f6bb01ca674b04ba67061e4db0
https://github.com/acl2/acl2/commit/5286eb5b5ed663f6bb01ca674b04ba67061e4db0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments/integer-formats.lisp
M books/kestrel/c/language/implementation-environments/top.lisp
Log Message:
-----------
[C] Extend implementation environments.
Include the `_Bool` format into the implementation environment.
Commit: e67f3f5191b518eb0ceff0d206237bb39a9e8d0c
https://github.com/acl2/acl2/commit/e67f3f5191b518eb0ceff0d206237bb39a9e8d0c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/implementation-environments/top.lisp
Log Message:
-----------
[C] Add two operations on implementation environments.
Commit: 56eafc62327cbe0ba3237145ecf0cce82c0140a8
https://github.com/acl2/acl2/commit/56eafc62327cbe0ba3237145ecf0cce82c0140a8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Extend proof generation for compound statements.
Log Message:
-----------
Add supporting theorems.
Extend implementation, but something else needs to be done before making that
active.
Commit: e6a3232a21a8672172d44e746dc0994004e9cdf4
https://github.com/acl2/acl2/commit/e6a3232a21a8672172d44e746dc0994004e9cdf4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Improve generated proofs.
For lists of block items, avoid generating assertions about variables at the end
of the block items. We are not tracking them, also because they are not needed,
given that scopes end at the end of the lists of block items.
Commit: e9afbf6e15f6460c1d6613f11cc66cb8f18542b0
https://github.com/acl2/acl2/commit/e9afbf6e15f6460c1d6613f11cc66cb8f18542b0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Add more support for compound statements.
Refine the generated proof hints.
Commit: 599a7420d2ed9b3ab396eb77f860f5d29fe0990a
https://github.com/acl2/acl2/commit/599a7420d2ed9b3ab396eb77f860f5d29fe0990a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-and-write2.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
Log Message:
-----------
Merge.
Commit: 8588ed520b59d73ee03fe3c213b8764f3a36be62
https://github.com/acl2/acl2/commit/8588ed520b59d73ee03fe3c213b8764f3a36be62
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
A books/kestrel/c/syntax/disambiguation.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/unambiguity.lisp
Log Message:
-----------
[C$] Add new file and topic for disambiguation.
Put unambiguity and disambiguator under it.
Commit: 237effbc5db778e6feeaf40529459a176360419f
https://github.com/acl2/acl2/commit/237effbc5db778e6feeaf40529459a176360419f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
Commit: 8b7bb47f0825f76ffc60d21317bcb72d72803888
https://github.com/acl2/acl2/commit/8b7bb47f0825f76ffc60d21317bcb72d72803888
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/atc/symbolic-computation-states.lisp
M books/kestrel/c/atc/theorem-generation.lisp
Log Message:
-----------
[ATC] Rename a theorem.
Commit: ea220e05a067ddd68c178801cd5f8a889169ac9f
https://github.com/acl2/acl2/commit/ea220e05a067ddd68c178801cd5f8a889169ac9f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-and-write2.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
Log Message:
-----------
Merge.
Commit: b91c6105dc90ce7100439e1fae965330b9d04a3b
https://github.com/acl2/acl2/commit/b91c6105dc90ce7100439e1fae965330b9d04a3b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
Commit: f3fe2b93add52ebda1c715cc02c3468b33c837d7
https://github.com/acl2/acl2/commit/f3fe2b93add52ebda1c715cc02c3468b33c837d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Commit: c700cd51a3240ff805dd3ee6ef7b6f0f12ce525b
https://github.com/acl2/acl2/commit/c700cd51a3240ff805dd3ee6ef7b6f0f12ce525b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.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/formalized.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/standard.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/split-all-gso.lisp
M books/kestrel/c/transformation/splitgso.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: 07a74b822d18541d2725ee486ead4f6fba8d26c7
https://github.com/acl2/acl2/commit/07a74b822d18541d2725ee486ead4f6fba8d26c7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.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/formalized.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/standard.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/split-all-gso.lisp
M books/kestrel/c/transformation/splitgso.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: 0c24c52f2e1e68a18a23c6f49b79e51328215110
https://github.com/acl2/acl2/commit/0c24c52f2e1e68a18a23c6f49b79e51328215110
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/parser.lisp
Log Message:
-----------
[C$] Improve name of a lexing function.
Commit: 9d3706c7c83015d369a80177042d020657507733
https://github.com/acl2/acl2/commit/9d3706c7c83015d369a80177042d020657507733
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/tests/parser.lisp
Log Message:
-----------
[C$] Add some lexer tests.
Commit: a202b1dfd0bfc636ce0a23f06ce28d0941c1b132
https://github.com/acl2/acl2/commit/a202b1dfd0bfc636ce0a23f06ce28d0941c1b132
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
Log Message:
-----------
[C$] Extend type calculation from annotation.
Add support for compound statements.
Commit: f48772e275f70d15e4e54acbe775603dddde1117
https://github.com/acl2/acl2/commit/f48772e275f70d15e4e54acbe775603dddde1117
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Extend `simpadd0` proof generation.
Finish adding support for compound statements.
Commit: 2745ff12deea6814afc5a73324250001d0ec0996
https://github.com/acl2/acl2/commit/2745ff12deea6814afc5a73324250001d0ec0996
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
A books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
A books/kestrel/c/transformation/tests/simpadd0/old/blocks.c
Log Message:
-----------
[C2C] Add `simpadd0` tests for compound statements.
Commit: 672df7ce4c63c24e948885fbd572bc022bb6a228
https://github.com/acl2/acl2/commit/672df7ce4c63c24e948885fbd572bc022bb6a228
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
A books/kestrel/c/syntax/disambiguation.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.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/standard.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/unambiguity.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/split-all-gso.lisp
M books/kestrel/c/transformation/splitgso.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
Merge.
Commit: c29dd1ff6ad43fd1666706931defdb973f351398
https://github.com/acl2/acl2/commit/c29dd1ff6ad43fd1666706931defdb973f351398
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
A books/kestrel/c/language/implementation-environments/bool-formats.lisp
M books/kestrel/c/language/implementation-environments/integer-formats.lisp
M books/kestrel/c/language/implementation-environments/top.lisp
Log Message:
-----------
Merge.
Commit: f612b1eed0ff959c195c364a198b95911e448c38
https://github.com/acl2/acl2/commit/f612b1eed0ff959c195c364a198b95911e448c38
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
Log Message:
-----------
[C$] Adapt to extension of implementation environments.
Commit: 300d80db68d1aa206805b71f682900406cff444f
https://github.com/acl2/acl2/commit/300d80db68d1aa206805b71f682900406cff444f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-18 (Thu, 18 Sep 2025)
Changed paths:
M books/kestrel/json-parser/parse-json.lisp
M books/kestrel/utilities/make-ord.lisp
Log Message:
-----------
[utilities] Collect some rules about make-ord.
Commit: 28df1b052313e7b65c6f2bdce9a57516f51f4c84
https://github.com/acl2/acl2/commit/28df1b052313e7b65c6f2bdce9a57516f51f4c84
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-18 (Thu, 18 Sep 2025)
Changed paths:
M books/kestrel/axe/x86/examples/add/add-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/formal-unit-tests/add/run-test.lisp
M books/kestrel/axe/x86/examples/tea/tea-elf64.lisp
M books/kestrel/axe/x86/examples/tea/tea-macho64.lisp
Log Message:
-----------
[axe/x86] Exclude some examples when STP is not installed.
Thanks to Matt Kaufmann for reporting this issue.
Commit: b5c997467e781217b5228f3918fe0b684c759f6a
https://github.com/acl2/acl2/commit/b5c997467e781217b5228f3918fe0b684c759f6a
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-09-18 (Thu, 18 Sep 2025)
Changed paths:
M books/kestrel/axe/x86/examples/add/add-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/formal-unit-tests/add/run-test.lisp
M books/kestrel/axe/x86/examples/tea/tea-elf64.lisp
M books/kestrel/axe/x86/examples/tea/tea-macho64.lisp
M books/kestrel/json-parser/parse-json.lisp
M books/kestrel/utilities/make-ord.lisp
Log Message:
-----------
Merge commit '28df1b052313e7b65c6f2bdce9a57516f51f4c84' into HEAD
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: 839bfa97dfb9911ab7c1f1da4d74152cc7a01e4d
https://github.com/acl2/acl2/commit/839bfa97dfb9911ab7c1f1da4d74152cc7a01e4d
Author: Grant Jurgensen <gr...@jurgensen.dev>
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:
-----------
[C$] Add compilation database utilities
The JSON compilation database file format is used by the clang
ecosystem. See the newly introduced xdoc for more information.
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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.
Log Message:
-----------
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:
-----------
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/8fbaeed3ce10...9d7049f4c90b
Reply all
Reply to author
Forward
0 new messages