[acl2/acl2] 0d0431: Fixed bugs involving large arrays not created by d...
1 view
Skip to first unread message
MattKaufmann
Nov 25, 2025, 5:12:17 AM (13 days ago) Nov 25
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 0d043185a65ccbb79c20458d9d64c22754f23b3f
https://github.com/acl2/acl2/commit/0d043185a65ccbb79c20458d9d64c22754f23b3f
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-25 (Tue, 25 Nov 2025)
Changed paths:
M axioms.lisp
M books/system/doc/acl2-doc.lisp
M defthm.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M rewrite.lisp
Log Message:
-----------
Fixed bugs involving large arrays not created by defstobj due to :non-executable t and in :pr.
Quoting :DOC note-8-7:
Fixed a bug that was causing errors for [stobj]s introduced with
[defstobj] keyword argument :non-executable t in the presence of
large arrays. This should not have caused an error, since that
keyword argument prevents attempts at contructing the stobj (with
its arrays).
Fixed a bug in :[pr] to work on function symbols introduced by
[defstobj] (GitHub Issue 1851). Thanks to David Taylor for
reporting this bug.
Quoting an implementation-level comment in (defxdoc note-8-7 ...):
; Fixed function find-rules-of-rune to work on runes introduced by defstobj.
; This is related to the fix for :pr: both use a new function,
; world-to-next-non-deeper-event, in place of world-to-next-event.
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 0d043185a65ccbb79c20458d9d64c22754f23b3f
https://github.com/acl2/acl2/commit/0d043185a65ccbb79c20458d9d64c22754f23b3f
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-25 (Tue, 25 Nov 2025)
Changed paths:
M axioms.lisp
M books/system/doc/acl2-doc.lisp
M defthm.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M rewrite.lisp
Log Message:
-----------
Fixed bugs involving large arrays not created by defstobj due to :non-executable t and in :pr.
Quoting :DOC note-8-7:
Fixed a bug that was causing errors for [stobj]s introduced with
[defstobj] keyword argument :non-executable t in the presence of
large arrays. This should not have caused an error, since that
keyword argument prevents attempts at contructing the stobj (with
its arrays).
Fixed a bug in :[pr] to work on function symbols introduced by
[defstobj] (GitHub Issue 1851). Thanks to David Taylor for
reporting this bug.
Quoting an implementation-level comment in (defxdoc note-8-7 ...):
; Fixed function find-rules-of-rune to work on runes introduced by defstobj.
; This is related to the fix for :pr: both use a new function,
; world-to-next-non-deeper-event, in place of world-to-next-event.
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
MattKaufmann
Nov 25, 2025, 5:12:38 AM (13 days ago) Nov 25
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Dec 1, 2025, 8:24:22 AM (7 days ago) Dec 1
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Commit: e1ac360f5950fe526bd2699d81b76fd244807eea
https://github.com/acl2/acl2/commit/e1ac360f5950fe526bd2699d81b76fd244807eea
Author: ACL2 Build Server <acl2bui...@gmail.com>
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/node-replacement-array3.lisp
M books/kestrel/axe/prove-with-stp-tests.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/bv-lists/top.lisp
M books/kestrel/bv/bif.lisp
M books/kestrel/bv/bit-to-bool.lisp
M books/kestrel/bv/bitnot.lisp
M books/kestrel/bv/bitwise.lisp
M books/kestrel/bv/bitxnor.lisp
M books/kestrel/bv/bool-to-bit.lisp
M books/kestrel/bv/bvminus-rules.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvnot.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/rules12.lisp
M books/kestrel/bv/std.lisp
M books/kestrel/bv/validation-stp.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
M books/kestrel/prime-fields/bv-rules-axe.lisp
Log Message:
-----------
Merge commit 'a313551efed3a18bbbdc9c75b3250c4f2ba9a9ba' into HEAD
Commit: 291f9dee9dfe61322f8117ddd9f7b13f2ed69fbe
https://github.com/acl2/acl2/commit/291f9dee9dfe61322f8117ddd9f7b13f2ed69fbe
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)
Changed paths:
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/integer-length.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv/bvlt.lisp
Log Message:
-----------
Merge commit '22cc9f8fa90c8f58603d4390585b0a01921ff5bd' into HEAD
Commit: 2e73b603578429e91d218415dab9d77d9be0b098
https://github.com/acl2/acl2/commit/2e73b603578429e91d218415dab9d77d9be0b098
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)
Changed paths:
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/x86-rules.lisp
A books/kestrel/x86/support64.lisp
M books/kestrel/x86/top.lisp
Log Message:
-----------
Merge commit '4f7504ea70b04a7bd9ed43550aa3f398a6091d2a' into HEAD
Commit: 0636b6304902cb95dcd726f89c4d1d2eb33a1431
https://github.com/acl2/acl2/commit/0636b6304902cb95dcd726f89c4d1d2eb33a1431
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-28 (Fri, 28 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Add a theorem.
Commit: aafcf7a68e65a016782dc696041f995fe60f580d
https://github.com/acl2/acl2/commit/aafcf7a68e65a016782dc696041f995fe60f580d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-28 (Fri, 28 Nov 2025)
Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
Log Message:
-----------
[C] Extend dynamic semantics.
Allow non-pure expressions as `do-while` tests.
Commit: 189925dac938e57a3bfd92048ee1a745042c95e7
https://github.com/acl2/acl2/commit/189925dac938e57a3bfd92048ee1a745042c95e7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-28 (Fri, 28 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Adapt to dynamic semantics changes.
This also adds support for `do-while` loops with non-pure expressions as tests.
Commit: cd9bbfd91e55de63a71782e9b40917dbf5cc61ae
https://github.com/acl2/acl2/commit/cd9bbfd91e55de63a71782e9b40917dbf5cc61ae
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
Log Message:
-----------
[C] Extend dynamic semantics.
Support non-pure expressions as tests of `if` statements.
Commit: f242a8f04c33ff10c5677d2576b21571898988e9
https://github.com/acl2/acl2/commit/f242a8f04c33ff10c5677d2576b21571898988e9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
Log Message:
-----------
[ATC] Adjust to changes to dynamic semantics.
Commit: 8a249d9950edc28899703872e5e9f88c53ab862b
https://github.com/acl2/acl2/commit/8a249d9950edc28899703872e5e9f88c53ab862b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Extend proof generation.
Add support for `if` statements with non-pure test expressions.
Commit: ed58b23929e1f275b8b51e3599d025165fe1cb56
https://github.com/acl2/acl2/commit/ed58b23929e1f275b8b51e3599d025165fe1cb56
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
Log Message:
-----------
[C] Extend dynamic semantics.
Add support for non-pure expression tests in `if-else` statements.
Commit: 444a7d99814b72cea40627094383cac667f31ee8
https://github.com/acl2/acl2/commit/444a7d99814b72cea40627094383cac667f31ee8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
Log Message:
-----------
[ATC] Adapt to changes to dynamic semantics.
Commit: f765f03a62c540b5d12596a00ab8ba8726bcce6e
https://github.com/acl2/acl2/commit/f765f03a62c540b5d12596a00ab8ba8726bcce6e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Extend proof generation.
Add support for `if-else` statements with non-pure expressions.
Commit: 10d0f67bf3d25fbf0d2239e85be5d3c2fa9d7f82
https://github.com/acl2/acl2/commit/10d0f67bf3d25fbf0d2239e85be5d3c2fa9d7f82
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
Log Message:
-----------
[C] Extend dynamic semantics.
Add support for non-pure test expressions in `while` loops.
Commit: f57671ef522c72973b2c1ef177734c7dc73082ea
https://github.com/acl2/acl2/commit/f57671ef522c72973b2c1ef177734c7dc73082ea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/statement-generation.lisp
Log Message:
-----------
[ATC] Adapt to changes to dynamic semantics.
Commit: c26081af54e9a02ce8428cac8f6d15ca836e5ee2
https://github.com/acl2/acl2/commit/c26081af54e9a02ce8428cac8f6d15ca836e5ee2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Extend proof generation.
Add support for non-pure test expressions in `while` loops.
Commit: 7667d34215afee3991c6bbe4ed13a8f8cc11c064
https://github.com/acl2/acl2/commit/7667d34215afee3991c6bbe4ed13a8f8cc11c064
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/system/doc/acl2-doc.lisp
Log Message:
-----------
Fixed a proof-builder bug that could occasionally cause two goals to exist with the same name.
Quoting :DOC note-8-7:
Fixed a [proof-builder] bug that could occasionally cause two goals
to exist with the same name.
Commit: a1016361580819d88f132cb2e4c7bad4d0725ab5
https://github.com/acl2/acl2/commit/a1016361580819d88f132cb2e4c7bad4d0725ab5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/language/pure-expression-execution.lisp
Log Message:
-----------
[C] Fix doc comment.
Commit: dc4ff805a826b62473285ad2f277a69fa89b841a
https://github.com/acl2/acl2/commit/dc4ff805a826b62473285ad2f277a69fa89b841a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/atc/tag-generation.lisp
M books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C] Rename a theorem.
Commit: 93a2e6f825ae142e8a822fdb34ab6b67ebc5a9a9
https://github.com/acl2/acl2/commit/93a2e6f825ae142e8a822fdb34ab6b67ebc5a9a9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/language/pure-expression-execution.lisp
Log Message:
-----------
[C] Add a theorem.
Commit: 17570c62d9116710c30f1cdecd4376add023a3f5
https://github.com/acl2/acl2/commit/17570c62d9116710c30f1cdecd4376add023a3f5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Rework a proof slightly.
Avoid using a rule that will be eventually removed.
Commit: 32ecc9827d6e0a77147cff19893593ee4134f683
https://github.com/acl2/acl2/commit/32ecc9827d6e0a77147cff19893593ee4134f683
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M other-events.lisp
Log Message:
-----------
Fixed SBCL handling of the :native option of trace! and trace$.
Quoting :DOC note-8-7:
The :native option of [trace!] and [trace$] did not work as one would
reasonably expect when SBCL is the host Lisp; now it does.
Also updated :DOC trace$ and :DOC trace!.
Commit: eb14ae4b051a785a82d3b831df3a53931731a5d0
https://github.com/acl2/acl2/commit/eb14ae4b051a785a82d3b831df3a53931731a5d0
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/utilities/er-soft-plus.lisp
M books/tools/er-soft-logic.lisp
Log Message:
-----------
Fixed some :DOC that erroneously said that (er soft ...) is not logic-mode code.
That was program-mode code in ACL2 Version 8.5 but has been logic-mode
code since Version 8.6.
Commit: edce2f81c223b79182b717edd90f54b7e47c71d2
https://github.com/acl2/acl2/commit/edce2f81c223b79182b717edd90f54b7e47c71d2
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/rewrite-stobj2.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/terms-light/termp.lisp
Log Message:
-----------
Merge commit '0d9850806570052d8555c999af7ce5431f7ddbb4' into HEAD
Commit: 60f7e43ac2bf0985069a4b346377a2ba27136207
https://github.com/acl2/acl2/commit/60f7e43ac2bf0985069a4b346377a2ba27136207
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-12-01 (Mon, 01 Dec 2025)
Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/memory/memory-regions.lisp
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/package.lsp
Log Message:
-----------
Merge commit '41f8cbc4e52073d8a9e9588ccf001e3eda1f4c70' into HEAD
Commit: 840f87f254ec7ad56bcbefa8e6b75773457ed7df
https://github.com/acl2/acl2/commit/840f87f254ec7ad56bcbefa8e6b75773457ed7df
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-01 (Mon, 01 Dec 2025)
Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/rewrite-stobj2.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/memory/memory-regions.lisp
M books/kestrel/terms-light/termp.lisp
M books/kestrel/utilities/er-soft-plus.lisp
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/package.lsp
M books/system/doc/acl2-doc.lisp
M books/tools/er-soft-logic.lisp
M proof-builder-a.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/41f8cbc4e520...840f87f254ec
https://github.com/acl2/acl2/commit/e1ac360f5950fe526bd2699d81b76fd244807eea
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-11-25 (Tue, 25 Nov 2025)
Changed paths:
M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
Changed paths:
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/node-replacement-array3.lisp
M books/kestrel/axe/prove-with-stp-tests.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/bv-lists/top.lisp
M books/kestrel/bv/bif.lisp
M books/kestrel/bv/bit-to-bool.lisp
M books/kestrel/bv/bitnot.lisp
M books/kestrel/bv/bitwise.lisp
M books/kestrel/bv/bitxnor.lisp
M books/kestrel/bv/bool-to-bit.lisp
M books/kestrel/bv/bvminus-rules.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvnot.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/rules12.lisp
M books/kestrel/bv/std.lisp
M books/kestrel/bv/validation-stp.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
M books/kestrel/prime-fields/bv-rules-axe.lisp
Log Message:
-----------
Merge commit 'a313551efed3a18bbbdc9c75b3250c4f2ba9a9ba' into HEAD
Commit: 291f9dee9dfe61322f8117ddd9f7b13f2ed69fbe
https://github.com/acl2/acl2/commit/291f9dee9dfe61322f8117ddd9f7b13f2ed69fbe
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)
Changed paths:
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/integer-length.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv/bvlt.lisp
Log Message:
-----------
Merge commit '22cc9f8fa90c8f58603d4390585b0a01921ff5bd' into HEAD
Commit: 2e73b603578429e91d218415dab9d77d9be0b098
https://github.com/acl2/acl2/commit/2e73b603578429e91d218415dab9d77d9be0b098
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-11-26 (Wed, 26 Nov 2025)
Changed paths:
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/x86-rules.lisp
A books/kestrel/x86/support64.lisp
M books/kestrel/x86/top.lisp
Log Message:
-----------
Merge commit '4f7504ea70b04a7bd9ed43550aa3f398a6091d2a' into HEAD
Commit: 0636b6304902cb95dcd726f89c4d1d2eb33a1431
https://github.com/acl2/acl2/commit/0636b6304902cb95dcd726f89c4d1d2eb33a1431
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-28 (Fri, 28 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C2C] Add a theorem.
Commit: aafcf7a68e65a016782dc696041f995fe60f580d
https://github.com/acl2/acl2/commit/aafcf7a68e65a016782dc696041f995fe60f580d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-28 (Fri, 28 Nov 2025)
Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
Log Message:
-----------
[C] Extend dynamic semantics.
Allow non-pure expressions as `do-while` tests.
Commit: 189925dac938e57a3bfd92048ee1a745042c95e7
https://github.com/acl2/acl2/commit/189925dac938e57a3bfd92048ee1a745042c95e7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-28 (Fri, 28 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Adapt to dynamic semantics changes.
This also adds support for `do-while` loops with non-pure expressions as tests.
Commit: cd9bbfd91e55de63a71782e9b40917dbf5cc61ae
https://github.com/acl2/acl2/commit/cd9bbfd91e55de63a71782e9b40917dbf5cc61ae
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
Log Message:
-----------
[C] Extend dynamic semantics.
Support non-pure expressions as tests of `if` statements.
Commit: f242a8f04c33ff10c5677d2576b21571898988e9
https://github.com/acl2/acl2/commit/f242a8f04c33ff10c5677d2576b21571898988e9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
Log Message:
-----------
[ATC] Adjust to changes to dynamic semantics.
Commit: 8a249d9950edc28899703872e5e9f88c53ab862b
https://github.com/acl2/acl2/commit/8a249d9950edc28899703872e5e9f88c53ab862b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Extend proof generation.
Add support for `if` statements with non-pure test expressions.
Commit: ed58b23929e1f275b8b51e3599d025165fe1cb56
https://github.com/acl2/acl2/commit/ed58b23929e1f275b8b51e3599d025165fe1cb56
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
Log Message:
-----------
[C] Extend dynamic semantics.
Add support for non-pure expression tests in `if-else` statements.
Commit: 444a7d99814b72cea40627094383cac667f31ee8
https://github.com/acl2/acl2/commit/444a7d99814b72cea40627094383cac667f31ee8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
Log Message:
-----------
[ATC] Adapt to changes to dynamic semantics.
Commit: f765f03a62c540b5d12596a00ab8ba8726bcce6e
https://github.com/acl2/acl2/commit/f765f03a62c540b5d12596a00ab8ba8726bcce6e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-29 (Sat, 29 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Extend proof generation.
Add support for `if-else` statements with non-pure expressions.
Commit: 10d0f67bf3d25fbf0d2239e85be5d3c2fa9d7f82
https://github.com/acl2/acl2/commit/10d0f67bf3d25fbf0d2239e85be5d3c2fa9d7f82
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
Log Message:
-----------
[C] Extend dynamic semantics.
Add support for non-pure test expressions in `while` loops.
Commit: f57671ef522c72973b2c1ef177734c7dc73082ea
https://github.com/acl2/acl2/commit/f57671ef522c72973b2c1ef177734c7dc73082ea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/statement-generation.lisp
Log Message:
-----------
[ATC] Adapt to changes to dynamic semantics.
Commit: c26081af54e9a02ce8428cac8f6d15ca836e5ee2
https://github.com/acl2/acl2/commit/c26081af54e9a02ce8428cac8f6d15ca836e5ee2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Extend proof generation.
Add support for non-pure test expressions in `while` loops.
Commit: 7667d34215afee3991c6bbe4ed13a8f8cc11c064
https://github.com/acl2/acl2/commit/7667d34215afee3991c6bbe4ed13a8f8cc11c064
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M proof-builder-a.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Fixed a proof-builder bug that could occasionally cause two goals to exist with the same name.
Quoting :DOC note-8-7:
Fixed a [proof-builder] bug that could occasionally cause two goals
to exist with the same name.
Commit: a1016361580819d88f132cb2e4c7bad4d0725ab5
https://github.com/acl2/acl2/commit/a1016361580819d88f132cb2e4c7bad4d0725ab5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/language/pure-expression-execution.lisp
Log Message:
-----------
[C] Fix doc comment.
Commit: dc4ff805a826b62473285ad2f277a69fa89b841a
https://github.com/acl2/acl2/commit/dc4ff805a826b62473285ad2f277a69fa89b841a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/atc/tag-generation.lisp
M books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C] Rename a theorem.
Commit: 93a2e6f825ae142e8a822fdb34ab6b67ebc5a9a9
https://github.com/acl2/acl2/commit/93a2e6f825ae142e8a822fdb34ab6b67ebc5a9a9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/language/pure-expression-execution.lisp
Log Message:
-----------
[C] Add a theorem.
Commit: 17570c62d9116710c30f1cdecd4376add023a3f5
https://github.com/acl2/acl2/commit/17570c62d9116710c30f1cdecd4376add023a3f5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/c/transformation/proof-generation-theorems.lisp
Log Message:
-----------
[C2C] Rework a proof slightly.
Avoid using a rule that will be eventually removed.
Commit: 32ecc9827d6e0a77147cff19893593ee4134f683
https://github.com/acl2/acl2/commit/32ecc9827d6e0a77147cff19893593ee4134f683
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M other-events.lisp
Log Message:
-----------
Fixed SBCL handling of the :native option of trace! and trace$.
Quoting :DOC note-8-7:
The :native option of [trace!] and [trace$] did not work as one would
reasonably expect when SBCL is the host Lisp; now it does.
Also updated :DOC trace$ and :DOC trace!.
Commit: eb14ae4b051a785a82d3b831df3a53931731a5d0
https://github.com/acl2/acl2/commit/eb14ae4b051a785a82d3b831df3a53931731a5d0
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/utilities/er-soft-plus.lisp
M books/tools/er-soft-logic.lisp
Log Message:
-----------
Fixed some :DOC that erroneously said that (er soft ...) is not logic-mode code.
That was program-mode code in ACL2 Version 8.5 but has been logic-mode
code since Version 8.6.
Commit: edce2f81c223b79182b717edd90f54b7e47c71d2
https://github.com/acl2/acl2/commit/edce2f81c223b79182b717edd90f54b7e47c71d2
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-11-30 (Sun, 30 Nov 2025)
Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/rewrite-stobj2.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/terms-light/termp.lisp
Log Message:
-----------
Merge commit '0d9850806570052d8555c999af7ce5431f7ddbb4' into HEAD
Commit: 60f7e43ac2bf0985069a4b346377a2ba27136207
https://github.com/acl2/acl2/commit/60f7e43ac2bf0985069a4b346377a2ba27136207
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-12-01 (Mon, 01 Dec 2025)
Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/memory/memory-regions.lisp
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/package.lsp
Log Message:
-----------
Merge commit '41f8cbc4e52073d8a9e9588ccf001e3eda1f4c70' into HEAD
Commit: 840f87f254ec7ad56bcbefa8e6b75773457ed7df
https://github.com/acl2/acl2/commit/840f87f254ec7ad56bcbefa8e6b75773457ed7df
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-01 (Mon, 01 Dec 2025)
Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/rewrite-stobj2.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/memory/memory-regions.lisp
M books/kestrel/terms-light/termp.lisp
M books/kestrel/utilities/er-soft-plus.lisp
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/package.lsp
M books/system/doc/acl2-doc.lisp
M books/tools/er-soft-logic.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M proof-builder-a.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/41f8cbc4e520...840f87f254ec
Reply all
Reply to author
Forward
0 new messages