[acl2/acl2] 96b8fe: [bv] Improve comments.
0 views
Skip to first unread message
Eric W. Smith
Sep 19, 2025, 4:44:10 PM (6 days ago) Sep 19
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 96b8fe214e9f8aaf5b4c12fb2f8c461359de4657
https://github.com/acl2/acl2/commit/96b8fe214e9f8aaf5b4c12fb2f8c461359de4657
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/trim.lisp
Log Message:
-----------
[bv] Improve comments.
Commit: 34ae943ccc05fa64d2d1bd8989ac3561b4fe4b6c
https://github.com/acl2/acl2/commit/34ae943ccc05fa64d2d1bd8989ac3561b4fe4b6c
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/trim-elim-rules-non-bv.lisp
Log Message:
-----------
[bv] Add some rules about bvif.
Commit: 9b987f5c66cc130478a37684dad83d0225cd5b25
https://github.com/acl2/acl2/commit/9b987f5c66cc130478a37684dad83d0225cd5b25
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/axe/axe-syntax-functions-bv.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/rule-lists.lisp
Log Message:
-----------
[axe] Improve handling of if/bvif.
Use the trim mechanism to turn if into bvif.
Commit: cacebe5555fbe9283aec85c10e16f1b0c03c23b7
https://github.com/acl2/acl2/commit/cacebe5555fbe9283aec85c10e16f1b0c03c23b7
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: 0a873bf94307fbe72a25fd8ffe9c97383e3509f5
https://github.com/acl2/acl2/commit/0a873bf94307fbe72a25fd8ffe9c97383e3509f5
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/utilities/extend-pathname-dollar.lisp
Log Message:
-----------
[utilities] Improve book on extend-pathname$.
This was enabled by an improvement Grant Jurgensen made to another book.
Commit: 5500a3d4c99fac63ffba5f3cbf41bfc27eb51350
https://github.com/acl2/acl2/commit/5500a3d4c99fac63ffba5f3cbf41bfc27eb51350
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 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
A books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/top.lisp
R books/kestrel/c/language/variable-preservation-in-execution.lisp
A books/kestrel/c/language/variable-resolution-preservation.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/projects/x86isa/doc.lisp
M books/projects/x86isa/linux/doc.lisp
M books/system/apply/apply-prim.lisp
Log Message:
-----------
Merge.
Commit: 42692fc87aabe3e9b214d678e4a1aa67b0f05339
https://github.com/acl2/acl2/commit/42692fc87aabe3e9b214d678e4a1aa67b0f05339
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/make-rewriter-simple.lisp
Log Message:
-----------
[axe] Tweak printing.
Commit: 49b59e833d55f3cf628d609006d49232c7dc2bb2
https://github.com/acl2/acl2/commit/49b59e833d55f3cf628d609006d49232c7dc2bb2
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/tactic-prover.lisp
Log Message:
-----------
[axe] Tweak.
Commit: 9270108e8e6aacc466e7b75bb3cb7cda6eadc2a7
https://github.com/acl2/acl2/commit/9270108e8e6aacc466e7b75bb3cb7cda6eadc2a7
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/x86/tester.lisp
Log Message:
-----------
[axe/x86] Clean up a bit.
Commit: 176cedfdd56dae816f874f001bc10bf1e6fa9d65
https://github.com/acl2/acl2/commit/176cedfdd56dae816f874f001bc10bf1e6fa9d65
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv/bv-syntax.lisp
Log Message:
-----------
[bv/axe] Support logext when converting args to BVs.
Commit: 4f71e4e37ac01ca79ba5d125034afb9e7d182a40
https://github.com/acl2/acl2/commit/4f71e4e37ac01ca79ba5d125034afb9e7d182a40
Author: Eric Smith <ews...@gmail.com>
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: 09ff46a196fbad7d13fe2bbed46bfd90f9747c8d
https://github.com/acl2/acl2/commit/09ff46a196fbad7d13fe2bbed46bfd90f9747c8d
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
M books/kestrel/json-parser/parse-json.lisp
M books/kestrel/utilities/make-ord.lisp
Log Message:
-----------
Merge.
Commit: d7c3c1b21a13e30fa5dc9371121a9da8513072eb
https://github.com/acl2/acl2/commit/d7c3c1b21a13e30fa5dc9371121a9da8513072eb
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-19 (Fri, 19 Sep 2025)
Changed paths:
M books/demos/defabsstobj-example-1.lisp
M books/interface/emacs/acl2-indent.el
M books/kestrel/c/atc/symbolic-computation-states.lisp
M books/kestrel/c/atc/theorem-generation.lisp
M books/kestrel/c/language/computation-states.lisp
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
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
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
A books/kestrel/c/syntax/compilation-db.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/implementation-environments.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
A books/kestrel/c/syntax/tests/compilation-db.lisp
A books/kestrel/c/syntax/tests/compile_commands.json
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/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/splitgso.lisp
A books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
A books/kestrel/c/transformation/tests/simpadd0/old/blocks.c
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/c67f6ecbe936...d7c3c1b21a13
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 96b8fe214e9f8aaf5b4c12fb2f8c461359de4657
https://github.com/acl2/acl2/commit/96b8fe214e9f8aaf5b4c12fb2f8c461359de4657
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/trim.lisp
Log Message:
-----------
[bv] Improve comments.
Commit: 34ae943ccc05fa64d2d1bd8989ac3561b4fe4b6c
https://github.com/acl2/acl2/commit/34ae943ccc05fa64d2d1bd8989ac3561b4fe4b6c
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/trim-elim-rules-non-bv.lisp
Log Message:
-----------
[bv] Add some rules about bvif.
Commit: 9b987f5c66cc130478a37684dad83d0225cd5b25
https://github.com/acl2/acl2/commit/9b987f5c66cc130478a37684dad83d0225cd5b25
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/axe/axe-syntax-functions-bv.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/rule-lists.lisp
Log Message:
-----------
[axe] Improve handling of if/bvif.
Use the trim mechanism to turn if into bvif.
Commit: cacebe5555fbe9283aec85c10e16f1b0c03c23b7
https://github.com/acl2/acl2/commit/cacebe5555fbe9283aec85c10e16f1b0c03c23b7
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: 0a873bf94307fbe72a25fd8ffe9c97383e3509f5
https://github.com/acl2/acl2/commit/0a873bf94307fbe72a25fd8ffe9c97383e3509f5
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-16 (Tue, 16 Sep 2025)
Changed paths:
M books/kestrel/utilities/extend-pathname-dollar.lisp
Log Message:
-----------
[utilities] Improve book on extend-pathname$.
This was enabled by an improvement Grant Jurgensen made to another book.
Commit: 5500a3d4c99fac63ffba5f3cbf41bfc27eb51350
https://github.com/acl2/acl2/commit/5500a3d4c99fac63ffba5f3cbf41bfc27eb51350
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 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
A books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/top.lisp
R books/kestrel/c/language/variable-preservation-in-execution.lisp
A books/kestrel/c/language/variable-resolution-preservation.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/projects/x86isa/doc.lisp
M books/projects/x86isa/linux/doc.lisp
M books/system/apply/apply-prim.lisp
Log Message:
-----------
Merge.
Commit: 42692fc87aabe3e9b214d678e4a1aa67b0f05339
https://github.com/acl2/acl2/commit/42692fc87aabe3e9b214d678e4a1aa67b0f05339
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/make-rewriter-simple.lisp
Log Message:
-----------
[axe] Tweak printing.
Commit: 49b59e833d55f3cf628d609006d49232c7dc2bb2
https://github.com/acl2/acl2/commit/49b59e833d55f3cf628d609006d49232c7dc2bb2
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/tactic-prover.lisp
Log Message:
-----------
[axe] Tweak.
Commit: 9270108e8e6aacc466e7b75bb3cb7cda6eadc2a7
https://github.com/acl2/acl2/commit/9270108e8e6aacc466e7b75bb3cb7cda6eadc2a7
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/x86/tester.lisp
Log Message:
-----------
[axe/x86] Clean up a bit.
Commit: 176cedfdd56dae816f874f001bc10bf1e6fa9d65
https://github.com/acl2/acl2/commit/176cedfdd56dae816f874f001bc10bf1e6fa9d65
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-17 (Wed, 17 Sep 2025)
Changed paths:
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv/bv-syntax.lisp
Log Message:
-----------
[bv/axe] Support logext when converting args to BVs.
Commit: 4f71e4e37ac01ca79ba5d125034afb9e7d182a40
https://github.com/acl2/acl2/commit/4f71e4e37ac01ca79ba5d125034afb9e7d182a40
Author: Eric Smith <ews...@gmail.com>
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: 09ff46a196fbad7d13fe2bbed46bfd90f9747c8d
https://github.com/acl2/acl2/commit/09ff46a196fbad7d13fe2bbed46bfd90f9747c8d
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
M books/kestrel/json-parser/parse-json.lisp
M books/kestrel/utilities/make-ord.lisp
Log Message:
-----------
Merge.
Commit: d7c3c1b21a13e30fa5dc9371121a9da8513072eb
https://github.com/acl2/acl2/commit/d7c3c1b21a13e30fa5dc9371121a9da8513072eb
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-19 (Fri, 19 Sep 2025)
Changed paths:
M books/demos/defabsstobj-example-1.lisp
M books/interface/emacs/acl2-indent.el
M books/kestrel/c/atc/symbolic-computation-states.lisp
M books/kestrel/c/atc/theorem-generation.lisp
M books/kestrel/c/language/computation-states.lisp
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
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
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
A books/kestrel/c/syntax/compilation-db.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/implementation-environments.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
A books/kestrel/c/syntax/tests/compilation-db.lisp
A books/kestrel/c/syntax/tests/compile_commands.json
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/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/splitgso.lisp
A books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
A books/kestrel/c/transformation/tests/simpadd0/old/blocks.c
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/c67f6ecbe936...d7c3c1b21a13
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Eric W. Smith
Sep 19, 2025, 6:15:27 PM (6 days ago) Sep 19
to acl2-...@googlegroups.com
Branch: refs/heads/master
Eric W. Smith
Sep 19, 2025, 6:16:36 PM (6 days ago) Sep 19
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Sep 20, 2025, 4:23:21 PM (5 days ago) Sep 20
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: 01b666a932f09b539d4585404ee98eb16bcf866e
https://github.com/acl2/acl2/commit/01b666a932f09b539d4585404ee98eb16bcf866e
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/x86/package.lsp
Log Message:
-----------
[axe/x86] Improve packages.
Commit: ed800093942dd52210c670a5732b878c7caba1a4
https://github.com/acl2/acl2/commit/ed800093942dd52210c670a5732b878c7caba1a4
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: a2130b561fe602fa69e516a07c49d007a036aed9
https://github.com/acl2/acl2/commit/a2130b561fe602fa69e516a07c49d007a036aed9
Author: David Taylor <jdavid...@outlook.com>
Log Message:
-----------
Mention CONST property in DEFCONST docs
Commit: c67f6ecbe93636a3f01d4a3be910e01f8d28830e
https://github.com/acl2/acl2/commit/c67f6ecbe93636a3f01d4a3be910e01f8d28830e
Author: Grant Jurgensen <gr...@jurgensen.dev>
Log Message:
-----------
[interface] Make elisp function argument optional
This addresses an issue observed when attempting to do `M-x
customize-variable`. This seemed to be calling indent-sexp with zero
arguments, while it is defined in acl2-indent.el with 1 argument. Making
the argument optional fixes the issue.
Commit: 21b3574ca723d98a71804f4fbe9ffeb966ff4473
https://github.com/acl2/acl2/commit/21b3574ca723d98a71804f4fbe9ffeb966ff4473
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
Commit: 578373a3841e7f18ec11a18551e83c05cd925de5
https://github.com/acl2/acl2/commit/578373a3841e7f18ec11a18551e83c05cd925de5
M books/kestrel/axe/axe-syntax-functions-bv.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/trim-elim-rules-non-bv.lisp
M books/kestrel/bv/trim.lisp
Commit: 12724cc8d6e2685a2acee323df496259e24758e7
https://github.com/acl2/acl2/commit/12724cc8d6e2685a2acee323df496259e24758e7
M books/kestrel/x86/package.lsp
Log Message:
-----------
[x86] Organize package symbols.
Commit: fe38cffeb0a81bc21afa150109974e4767ea8f48
https://github.com/acl2/acl2/commit/fe38cffeb0a81bc21afa150109974e4767ea8f48
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C$] Extend calculation of types from annotations.
Add support for `while` loops.
Commit: ad5e69d986ff1a67be25876bfec2d7e6565a9845
https://github.com/acl2/acl2/commit/ad5e69d986ff1a67be25876bfec2d7e6565a9845
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C2C] Import symbol into package.
Commit: 8d95bca2fff3680608f72ecff63f1c1839368d49
https://github.com/acl2/acl2/commit/8d95bca2fff3680608f72ecff63f1c1839368d49
Author: David Taylor <jdavid...@outlook.com>
Log Message:
-----------
Display GETPROPC link in typewriter font
Commit: 073777782c96b97f2a91052ed5f48fa7474c8bbf
https://github.com/acl2/acl2/commit/073777782c96b97f2a91052ed5f48fa7474c8bbf
Author: MattKaufmann <kauf...@cs.utexas.edu>
Log Message:
-----------
Merge pull request #1848 from copperteal/defconst/const-prop
Mention CONST property in DEFCONST docs
Commit: 5b53fbe31dbf7929986d873226047895ffe33844
https://github.com/acl2/acl2/commit/5b53fbe31dbf7929986d873226047895ffe33844
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Synch doc.lisp etc.
Commit: 03230f90a941ae77bc57d54ae7d7f0e035fb49e3
https://github.com/acl2/acl2/commit/03230f90a941ae77bc57d54ae7d7f0e035fb49e3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M books/interface/emacs/acl2-indent.el
M books/kestrel/axe/axe-syntax-functions-bv.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/trim-elim-rules-non-bv.lisp
M books/kestrel/bv/trim.lisp
M books/kestrel/utilities/extend-pathname-dollar.lisp
M books/kestrel/x86/package.lsp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Merge.
Commit: fc8b3a23464f8f7aa737b7ec89436977f0fce1ba
https://github.com/acl2/acl2/commit/fc8b3a23464f8f7aa737b7ec89436977f0fce1ba
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Move code to dedicated function.
Commit: 4f5fd59e424c3ad4af3f4be906e1f482b8b91316
https://github.com/acl2/acl2/commit/4f5fd59e424c3ad4af3f4be906e1f482b8b91316
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Add a predicate about variables in computation states.
This lifts the predicate for single variables and types to variable-type maps.
This is needed to prove general supporting theorems for `while` loops.
Commit: d90bfed4ea65d52fcc265c55e7de34e1a3b9a502
https://github.com/acl2/acl2/commit/d90bfed4ea65d52fcc265c55e7de34e1a3b9a502
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Add supporting theorems for `while` loops.
Commit: 61c34683e3e9a056cb462a7b2ab3601babb7c0b6
https://github.com/acl2/acl2/commit/61c34683e3e9a056cb462a7b2ab3601babb7c0b6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Extend `simpadd0` proof generation.
Add support for `while` loops.
Commit: ae8c229bb5d933d9df3015553dcf7a2e102f258c
https://github.com/acl2/acl2/commit/ae8c229bb5d933d9df3015553dcf7a2e102f258c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
A books/kestrel/c/transformation/tests/simpadd0/old/while.c
A books/kestrel/c/transformation/tests/simpadd0/while.lisp
Log Message:
-----------
[C2C] Add a `simpadd0` test for `while` loops.
Compare: https://github.com/acl2/acl2/compare/9d7049f4c90b...ae8c229bb5d9
https://github.com/acl2/acl2/commit/01b666a932f09b539d4585404ee98eb16bcf866e
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/x86/package.lsp
Log Message:
-----------
[axe/x86] Improve packages.
Commit: ed800093942dd52210c670a5732b878c7caba1a4
https://github.com/acl2/acl2/commit/ed800093942dd52210c670a5732b878c7caba1a4
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: a2130b561fe602fa69e516a07c49d007a036aed9
https://github.com/acl2/acl2/commit/a2130b561fe602fa69e516a07c49d007a036aed9
Author: David Taylor <jdavid...@outlook.com>
Date: 2025-09-18 (Thu, 18 Sep 2025)
Changed paths:
M books/system/doc/acl2-doc.lisp
Changed paths:
Log Message:
-----------
Mention CONST property in DEFCONST docs
Commit: c67f6ecbe93636a3f01d4a3be910e01f8d28830e
https://github.com/acl2/acl2/commit/c67f6ecbe93636a3f01d4a3be910e01f8d28830e
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2025-09-19 (Fri, 19 Sep 2025)
Changed paths:
M books/interface/emacs/acl2-indent.el
Changed paths:
Log Message:
-----------
[interface] Make elisp function argument optional
This addresses an issue observed when attempting to do `M-x
customize-variable`. This seemed to be calling indent-sexp with zero
arguments, while it is defined in acl2-indent.el with 1 argument. Making
the argument optional fixes the issue.
Commit: 21b3574ca723d98a71804f4fbe9ffeb966ff4473
https://github.com/acl2/acl2/commit/21b3574ca723d98a71804f4fbe9ffeb966ff4473
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-19 (Fri, 19 Sep 2025)
Changed paths:
M books/demos/defabsstobj-example-1.lisp
M books/interface/emacs/acl2-indent.el
Date: 2025-09-19 (Fri, 19 Sep 2025)
Changed paths:
M books/demos/defabsstobj-example-1.lisp
M books/interface/emacs/acl2-indent.el
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/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/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/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
https://github.com/acl2/acl2/commit/578373a3841e7f18ec11a18551e83c05cd925de5
M books/kestrel/axe/axe-syntax-functions-bv.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/trim-elim-rules-non-bv.lisp
M books/kestrel/bv/trim.lisp
M books/kestrel/utilities/extend-pathname-dollar.lisp
Log Message:
-----------
Merge.
Log Message:
-----------
Commit: 12724cc8d6e2685a2acee323df496259e24758e7
https://github.com/acl2/acl2/commit/12724cc8d6e2685a2acee323df496259e24758e7
M books/kestrel/x86/package.lsp
Log Message:
-----------
[x86] Organize package symbols.
Commit: fe38cffeb0a81bc21afa150109974e4767ea8f48
https://github.com/acl2/acl2/commit/fe38cffeb0a81bc21afa150109974e4767ea8f48
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-19 (Fri, 19 Sep 2025)
Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
Changed paths:
Log Message:
-----------
[C$] Extend calculation of types from annotations.
Add support for `while` loops.
Commit: ad5e69d986ff1a67be25876bfec2d7e6565a9845
https://github.com/acl2/acl2/commit/ad5e69d986ff1a67be25876bfec2d7e6565a9845
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-19 (Fri, 19 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/package.lsp
Changed paths:
Log Message:
-----------
[C2C] Import symbol into package.
Commit: 8d95bca2fff3680608f72ecff63f1c1839368d49
https://github.com/acl2/acl2/commit/8d95bca2fff3680608f72ecff63f1c1839368d49
Author: David Taylor <jdavid...@outlook.com>
Date: 2025-09-19 (Fri, 19 Sep 2025)
Changed paths:
M books/system/doc/acl2-doc.lisp
Changed paths:
Log Message:
-----------
Display GETPROPC link in typewriter font
Commit: 073777782c96b97f2a91052ed5f48fa7474c8bbf
https://github.com/acl2/acl2/commit/073777782c96b97f2a91052ed5f48fa7474c8bbf
Author: MattKaufmann <kauf...@cs.utexas.edu>
Date: 2025-09-19 (Fri, 19 Sep 2025)
Changed paths:
M books/system/doc/acl2-doc.lisp
Changed paths:
Log Message:
-----------
Merge pull request #1848 from copperteal/defconst/const-prop
Mention CONST property in DEFCONST docs
Commit: 5b53fbe31dbf7929986d873226047895ffe33844
https://github.com/acl2/acl2/commit/5b53fbe31dbf7929986d873226047895ffe33844
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Synch doc.lisp etc.
Commit: 03230f90a941ae77bc57d54ae7d7f0e035fb49e3
https://github.com/acl2/acl2/commit/03230f90a941ae77bc57d54ae7d7f0e035fb49e3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M books/interface/emacs/acl2-indent.el
M books/kestrel/axe/axe-syntax-functions-bv.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/trim-elim-rules-non-bv.lisp
M books/kestrel/bv/trim.lisp
M books/kestrel/utilities/extend-pathname-dollar.lisp
M books/kestrel/x86/package.lsp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Merge.
Commit: fc8b3a23464f8f7aa737b7ec89436977f0fce1ba
https://github.com/acl2/acl2/commit/fc8b3a23464f8f7aa737b7ec89436977f0fce1ba
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Move code to dedicated function.
Commit: 4f5fd59e424c3ad4af3f4be906e1f482b8b91316
https://github.com/acl2/acl2/commit/4f5fd59e424c3ad4af3f4be906e1f482b8b91316
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Add a predicate about variables in computation states.
This lifts the predicate for single variables and types to variable-type maps.
This is needed to prove general supporting theorems for `while` loops.
Commit: d90bfed4ea65d52fcc265c55e7de34e1a3b9a502
https://github.com/acl2/acl2/commit/d90bfed4ea65d52fcc265c55e7de34e1a3b9a502
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Add supporting theorems for `while` loops.
Commit: 61c34683e3e9a056cb462a7b2ab3601babb7c0b6
https://github.com/acl2/acl2/commit/61c34683e3e9a056cb462a7b2ab3601babb7c0b6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Extend `simpadd0` proof generation.
Add support for `while` loops.
Commit: ae8c229bb5d933d9df3015553dcf7a2e102f258c
https://github.com/acl2/acl2/commit/ae8c229bb5d933d9df3015553dcf7a2e102f258c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)
Changed paths:
A books/kestrel/c/transformation/tests/simpadd0/old/while.c
A books/kestrel/c/transformation/tests/simpadd0/while.lisp
Log Message:
-----------
[C2C] Add a `simpadd0` test for `while` loops.
Compare: https://github.com/acl2/acl2/compare/9d7049f4c90b...ae8c229bb5d9
Reply all
Reply to author
Forward
0 new messages