[acl2/acl2] 938ba2: [axe/x86] Organize rule-list.

0 views
Skip to first unread message

Eric W. Smith

unread,
Sep 25, 2025, 10:58:54 PM (16 hours ago) Sep 25
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 938ba25026dbcfc63c3688c8f9fb32819febc529
https://github.com/acl2/acl2/commit/938ba25026dbcfc63c3688c8f9fb32819febc529
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-21 (Sun, 21 Sep 2025)

Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp

Log Message:
-----------
[axe/x86] Organize rule-list.


Commit: 21a3ed70c42f340f5f6e2f935ac7ba2f736769d1
https://github.com/acl2/acl2/commit/21a3ed70c42f340f5f6e2f935ac7ba2f736769d1
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/apt/schemalg-doc.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/merge-nodes-into-dag-array.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/run-until-return.lisp
M books/kestrel/axe/risc-v/unroll.lisp
M books/kestrel/axe/utilities.lisp
M books/kestrel/bv-lists/bv-array-conversions2.lisp
M books/kestrel/c/syntax/reader.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions64.lisp
M books/kestrel/x86/read-and-write2.lisp
M books/kestrel/x86/read-bytes-and-write-bytes.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/zmm.lisp
A books/kestrel/xml/build-book-for-xml-file.lisp
M books/kestrel/xml/xml-parser.lisp
M books/projects/codewalker/basic-demo.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: c6623bda9ff1bc2e63045998ecb1522a27d92bcc
https://github.com/acl2/acl2/commit/c6623bda9ff1bc2e63045998ecb1522a27d92bcc
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-23 (Tue, 23 Sep 2025)

Changed paths:
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-call-or-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/language/dynamic-semantics.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-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocess-file.lisp
M books/kestrel/c/syntax/printer.lisp
A books/kestrel/c/syntax/printing.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/input-files.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0-doc.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/tests/call-graph/call-graph.lisp
M books/kestrel/c/transformation/tests/constant-propagation/constant-propagation.lisp
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp
M books/kestrel/c/transformation/tests/rename/rename.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/bin.lisp
M books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast-int-to-long.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast-long-to-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/constant.lisp
M books/kestrel/c/transformation/tests/simpadd0/decl.lisp
M books/kestrel/c/transformation/tests/simpadd0/file-scope.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/global.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-const.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-param.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-return.lisp
M books/kestrel/c/transformation/tests/simpadd0/noninteger.lisp
M books/kestrel/c/transformation/tests/simpadd0/nosimp-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/nosimp-short.lisp
M books/kestrel/c/transformation/tests/simpadd0/nosimp-ulong.lisp
M books/kestrel/c/transformation/tests/simpadd0/paren.lisp
M books/kestrel/c/transformation/tests/simpadd0/return-void.lisp
M books/kestrel/c/transformation/tests/simpadd0/stmt-null.lisp
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/var.lisp
M books/kestrel/c/transformation/tests/simpadd0/while.lisp
M books/kestrel/c/transformation/tests/specialize/specialize.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-fn-when/split-fn-when.lisp
M books/kestrel/c/transformation/tests/split-fn/split-fn.lisp
M books/kestrel/c/transformation/tests/splitgso/splitgso.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
A books/kestrel/fty/any-nat-map.lisp
M books/kestrel/fty/bin-digit-char-list.lisp
A books/kestrel/fty/character-any-map.lisp
A books/kestrel/fty/character-set.lisp
M books/kestrel/fty/dec-digit-char-list.lisp
M books/kestrel/fty/hex-digit-char-list.lisp
M books/kestrel/fty/oct-digit-char-list.lisp
M books/kestrel/fty/string-stringlist-alist.lisp
A books/kestrel/fty/string-stringlist-map.lisp
M books/kestrel/fty/strings-decimal-fty.lisp
M books/kestrel/fty/symbol-pseudoeventform-alist.lisp
M books/kestrel/fty/symbol-pseudoterm-alist.lisp
M books/kestrel/fty/top.lisp
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/hol-in-acl2/acl2/package.lsp
M books/projects/hol-in-acl2/acl2/theories.lisp
A books/projects/hol-in-acl2/acl2/typ.lisp
M books/projects/hol-in-acl2/examples/README
A books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
A books/projects/hol-in-acl2/examples/eval-poly-thy-alt.lisp
A books/projects/hol-in-acl2/to-do.txt
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: 8e9235df760fa6f1315e139260c975edff63191c
https://github.com/acl2/acl2/commit/8e9235df760fa6f1315e139260c975edff63191c
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/grammar.abnf
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/keywords.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/output-files-doc.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/unambiguity.lisp
M books/kestrel/c/syntax/validator.lisp
A books/kestrel/c/transformation/input-processing.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/top.lisp

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


Commit: cf623124d8f7fe26ea590206b0879b31d9e588f9
https://github.com/acl2/acl2/commit/cf623124d8f7fe26ea590206b0879b31d9e588f9
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/kestrel/bv/bvmult.lisp

Log Message:
-----------
[bv] Add a rule.


Commit: 48b8f188da51abb0e275ff0cf33627c4871c2e3c
https://github.com/acl2/acl2/commit/48b8f188da51abb0e275ff0cf33627c4871c2e3c
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/kestrel/axe/evaluator-basic.lisp

Log Message:
-----------
[axe] Add comment.


Commit: b0259239979b8aa614b8d994f5ec37dcd26e5472
https://github.com/acl2/acl2/commit/b0259239979b8aa614b8d994f5ec37dcd26e5472
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/kestrel/axe/risc-v/rule-lists.lisp

Log Message:
-----------
[axe/risc-v] Tweak rule-list.


Commit: 4a5cee54261ef5ab2db9e968b0029cfb678e6925
https://github.com/acl2/acl2/commit/4a5cee54261ef5ab2db9e968b0029cfb678e6925
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/kestrel/axe/rules3.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv-lists/bv-array-read.lisp

Log Message:
-----------
[bv-lists] Gather/improve array pattern rules.


Commit: 9541a9e11d30f07a76b2dadc193059a8f4666f04
https://github.com/acl2/acl2/commit/9541a9e11d30f07a76b2dadc193059a8f4666f04
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp

Log Message:
-----------
[axe/x86] Add comment.


Commit: b03b6e7a80185f4e63dbe0f1b294938aa7ed192d
https://github.com/acl2/acl2/commit/b03b6e7a80185f4e63dbe0f1b294938aa7ed192d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.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/grammar.abnf
M books/kestrel/c/syntax/keywords.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/parser.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/simpadd0.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


Commit: b470281fd1a8b0947aea59f6dca1291920b03943
https://github.com/acl2/acl2/commit/b470281fd1a8b0947aea59f6dca1291920b03943
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/kestrel/axe/risc-v/README.md
A books/kestrel/axe/risc-v/examples/README.md

Log Message:
-----------
[axe/risc-v] Tweak READMEs.


Commit: 642b054f04b53ac562dffca28b4f5238bf2b0318
https://github.com/acl2/acl2/commit/642b054f04b53ac562dffca28b4f5238bf2b0318
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/kestrel/axe/risc-v/read-and-write.lisp

Log Message:
-----------
[axe/risc-v] Simplify hints.


Commit: 853bb202a3041212596836bdeabf48b74fbd6c22
https://github.com/acl2/acl2/commit/853bb202a3041212596836bdeabf48b74fbd6c22
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/kestrel/axe/arithmetic-rules-axe.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/rules3.lisp

Log Message:
-----------
[axe] Organize some rules.

Also simplify some hints.


Commit: b7e8235684c3fdddcc6012df83c55ce41764f357
https://github.com/acl2/acl2/commit/b7e8235684c3fdddcc6012df83c55ce41764f357
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/kestrel/axe/rule-lists.lisp

Log Message:
-----------
[axe] Comment out a rule.


Commit: eb30a543fa6bdf1290e3c259b3e2f3c96cd81602
https://github.com/acl2/acl2/commit/eb30a543fa6bdf1290e3c259b3e2f3c96cd81602
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-25 (Thu, 25 Sep 2025)

Changed paths:
M books/kestrel/axe/risc-v/unroll.lisp

Log Message:
-----------
[axe/risc-v] Fix file header.


Commit: 2b113549a80456353d525909df3490c69d10ada2
https://github.com/acl2/acl2/commit/2b113549a80456353d525909df3490c69d10ada2
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-25 (Thu, 25 Sep 2025)

Changed paths:
M books/kestrel/axe/jvm/examples/formal-unit-tester/AbsLong.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearch.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearchBuggy.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/Prefix.lisp
R books/kestrel/axe/jvm/formal-unit-tester-exec.acl2
R books/kestrel/axe/jvm/formal-unit-tester-exec.lisp
R books/kestrel/axe/jvm/formal-unit-tester.acl2
R books/kestrel/axe/jvm/formal-unit-tester.lisp
A books/kestrel/axe/jvm/tester-exec.acl2
A books/kestrel/axe/jvm/tester-exec.lisp
A books/kestrel/axe/jvm/tester.acl2
A books/kestrel/axe/jvm/tester.lisp
M books/kestrel/axe/jvm/top.lisp

Log Message:
-----------
[axe/jvm] Rename formal-unit-tester.lisp to just tester.lisp.

For consistency with the x86 variant.


Commit: bd62998d4d150fb57d8dde03db7c4483967a5380
https://github.com/acl2/acl2/commit/bd62998d4d150fb57d8dde03db7c4483967a5380
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-25 (Thu, 25 Sep 2025)

Changed paths:
M books/kestrel/axe/x86/tester.lisp

Log Message:
-----------
[axe/x86] Remove unneeded rule.


Commit: 50e668fb6d148ef96884840c32bd60ea7cc47e79
https://github.com/acl2/acl2/commit/50e668fb6d148ef96884840c32bd60ea7cc47e79
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-25 (Thu, 25 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/split-all-gso.lisp

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


Commit: f22faeb631e405a4ec73307180e71349684bd3bf
https://github.com/acl2/acl2/commit/f22faeb631e405a4ec73307180e71349684bd3bf
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-25 (Thu, 25 Sep 2025)

Changed paths:
M books/kestrel/c/language/variable-resolution-preservation.lisp

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


Commit: 44ca7d6d97b018774ca2d5c6ea1480db7672a789
https://github.com/acl2/acl2/commit/44ca7d6d97b018774ca2d5c6ea1480db7672a789
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-25 (Thu, 25 Sep 2025)

Changed paths:
M books/kestrel/axe/x86/unroll-x86-code.lisp

Log Message:
-----------
[axe/x86] Add comment.


Compare: https://github.com/acl2/acl2/compare/c4b0e52b2b57...44ca7d6d97b0

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

Eric W. Smith

unread,
12:00 PM (3 hours ago) 12:00 PM
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: d2cb879140cc45a158091c5d7d4430d762e4f98f
https://github.com/acl2/acl2/commit/d2cb879140cc45a158091c5d7d4430d762e4f98f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-25 (Thu, 25 Sep 2025)

Changed paths:
M books/kestrel/axe/jvm/.gitignore
R books/kestrel/axe/jvm/formal-unit-tester.sh
R books/kestrel/axe/jvm/save-exec-for-fut.sh
A books/kestrel/axe/jvm/save-exec-for-tester.sh
A books/kestrel/axe/jvm/tester.sh

Log Message:
-----------
[axe/jvm] Update formal-unit-tester scripts.

Leftover files acl2-with-fut* can be safely deleted.


Compare: https://github.com/acl2/acl2/compare/c4b0e52b2b57...d2cb879140cc

Eric W. Smith

unread,
12:00 PM (3 hours ago) 12:00 PM
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
2:09 PM (22 minutes ago) 2:09 PM
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: 0c642af8a18ff27f2e683645e4daef3cfd055c0a
https://github.com/acl2/acl2/commit/0c642af8a18ff27f2e683645e4daef3cfd055c0a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-24 (Wed, 24 Sep 2025)

Changed paths:
M books/std/omaps/core.lisp

Log Message:
-----------
[Std/omaps] Improve XDOC hierarchy.


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

Changed paths:
M books/kestrel/c/atc/doc.lisp

Log Message:
-----------
[ATC] Improve user doc.
Commit: 32a5fb19b1dfc3812b004fb93cfa4374fe108630
https://github.com/acl2/acl2/commit/32a5fb19b1dfc3812b004fb93cfa4374fe108630
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2025-09-25 (Thu, 25 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/split-all-gso.lisp

Log Message:
-----------
[C$] Add :keep-going option to input-files

Also adds `keep-going` arguments to the parser, disambiguator, and
validator.


Commit: 50e668fb6d148ef96884840c32bd60ea7cc47e79
https://github.com/acl2/acl2/commit/50e668fb6d148ef96884840c32bd60ea7cc47e79
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-25 (Thu, 25 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/split-all-gso.lisp

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


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

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/split-all-gso.lisp

Log Message:
-----------
Merge commit '32a5fb19b1dfc3812b004fb93cfa4374fe108630' into HEAD


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

Changed paths:
M books/kestrel/c/atc/atc.lisp

Log Message:
-----------
[ATC] Clarify some dev doc.


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

Changed paths:
M books/kestrel/c/atc/variable-tables.lisp

Log Message:
-----------
[ATC] Avoid some proof hints.


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

Changed paths:
M books/kestrel/c/atc/function-tables.lisp

Log Message:
-----------
[ATC] Make some dev doc more readable.


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

Changed paths:
M books/kestrel/c/atc/generation-contexts.lisp

Log Message:
-----------
[ATC] Improve some dev doc.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/top.lisp

Log Message:
-----------
[C$] Improve organization of code related to abstract syntax.


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

Changed paths:
M books/kestrel/c/atc/expression-generation.lisp

Log Message:
-----------
[ATC] Improve some dev doc.


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

Changed paths:
M books/kestrel/c/atc/generation.lisp

Log Message:
-----------
[ATC] Update some dev doc.


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

Changed paths:
M books/kestrel/c/atc/theorem-generation.lisp

Log Message:
-----------
[ATC] Improve some dev doc.
Commit: 9ccd6cd000ad9614bfd7c0d30c744f34246d222b
https://github.com/acl2/acl2/commit/9ccd6cd000ad9614bfd7c0d30c744f34246d222b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-25 (Thu, 25 Sep 2025)

Changed paths:
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.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/grammar.abnf
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.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/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/tests/validator.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/simpadd0.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


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

Changed paths:
M books/kestrel/c/language/dynamic-semantics.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

Log Message:
-----------
[C] Extend dynamic semantics.

Have assignment expressions also return their value, besides performing their
side effect.


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

Changed paths:
M books/kestrel/c/atc/expression-generation.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-call-or-asg.lisp
M books/kestrel/c/atc/tag-generation.lisp

Log Message:
-----------
[ATC] Adapt to extended dynamic semantics.


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

Changed paths:
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.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/grammar.abnf
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/keywords.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/tests/validator.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/simpadd0.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


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

Changed paths:
M books/kestrel/axe/arithmetic-rules-axe.lisp
M books/kestrel/axe/evaluator-basic.lisp
M books/kestrel/axe/jvm/.gitignore
M books/kestrel/axe/jvm/examples/formal-unit-tester/AbsLong.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearch.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearchBuggy.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/Prefix.lisp
R books/kestrel/axe/jvm/formal-unit-tester-exec.acl2
R books/kestrel/axe/jvm/formal-unit-tester-exec.lisp
R books/kestrel/axe/jvm/formal-unit-tester.acl2
R books/kestrel/axe/jvm/formal-unit-tester.lisp
R books/kestrel/axe/jvm/formal-unit-tester.sh
R books/kestrel/axe/jvm/save-exec-for-fut.sh
A books/kestrel/axe/jvm/save-exec-for-tester.sh
A books/kestrel/axe/jvm/tester-exec.acl2
A books/kestrel/axe/jvm/tester-exec.lisp
A books/kestrel/axe/jvm/tester.acl2
A books/kestrel/axe/jvm/tester.lisp
A books/kestrel/axe/jvm/tester.sh
M books/kestrel/axe/jvm/top.lisp
M books/kestrel/axe/risc-v/README.md
A books/kestrel/axe/risc-v/examples/README.md
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/unroll.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv-lists/bv-array-read.lisp
M books/kestrel/bv/bvmult.lisp

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


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/top.lisp

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


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

Changed paths:
M books/std/omaps/core.lisp

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


Commit: 54c64ff0697e52c5d3f0e55d3f7c99e5dc10d942
https://github.com/acl2/acl2/commit/54c64ff0697e52c5d3f0e55d3f7c99e5dc10d942
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-26 (Fri, 26 Sep 2025)

Changed paths:
M books/kestrel/axe/arithmetic-rules-axe.lisp
M books/kestrel/axe/evaluator-basic.lisp
M books/kestrel/axe/jvm/.gitignore
M books/kestrel/axe/jvm/examples/formal-unit-tester/AbsLong.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearch.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearchBuggy.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/Prefix.lisp
R books/kestrel/axe/jvm/formal-unit-tester-exec.acl2
R books/kestrel/axe/jvm/formal-unit-tester-exec.lisp
R books/kestrel/axe/jvm/formal-unit-tester.acl2
R books/kestrel/axe/jvm/formal-unit-tester.lisp
R books/kestrel/axe/jvm/formal-unit-tester.sh
R books/kestrel/axe/jvm/save-exec-for-fut.sh
A books/kestrel/axe/jvm/save-exec-for-tester.sh
A books/kestrel/axe/jvm/tester-exec.acl2
A books/kestrel/axe/jvm/tester-exec.lisp
A books/kestrel/axe/jvm/tester.acl2
A books/kestrel/axe/jvm/tester.lisp
A books/kestrel/axe/jvm/tester.sh
M books/kestrel/axe/jvm/top.lisp
M books/kestrel/axe/risc-v/README.md
A books/kestrel/axe/risc-v/examples/README.md
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/unroll.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv-lists/bv-array-read.lisp
M books/kestrel/bv/bvmult.lisp

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


Commit: 5fdd2cf02a7bbd12089d04fa9bf336d3a31c97c5
https://github.com/acl2/acl2/commit/5fdd2cf02a7bbd12089d04fa9bf336d3a31c97c5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-26 (Fri, 26 Sep 2025)

Changed paths:
M books/kestrel/axe/arithmetic-rules-axe.lisp
M books/kestrel/axe/evaluator-basic.lisp
M books/kestrel/axe/jvm/.gitignore
M books/kestrel/axe/jvm/examples/formal-unit-tester/AbsLong.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearch.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/BinarySearchBuggy.lisp
M books/kestrel/axe/jvm/examples/formal-unit-tester/Prefix.lisp
R books/kestrel/axe/jvm/formal-unit-tester-exec.acl2
R books/kestrel/axe/jvm/formal-unit-tester-exec.lisp
R books/kestrel/axe/jvm/formal-unit-tester.acl2
R books/kestrel/axe/jvm/formal-unit-tester.lisp
R books/kestrel/axe/jvm/formal-unit-tester.sh
R books/kestrel/axe/jvm/save-exec-for-fut.sh
A books/kestrel/axe/jvm/save-exec-for-tester.sh
A books/kestrel/axe/jvm/tester-exec.acl2
A books/kestrel/axe/jvm/tester-exec.lisp
A books/kestrel/axe/jvm/tester.acl2
A books/kestrel/axe/jvm/tester.lisp
A books/kestrel/axe/jvm/tester.sh
M books/kestrel/axe/jvm/top.lisp
M books/kestrel/axe/risc-v/README.md
A books/kestrel/axe/risc-v/examples/README.md
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/unroll.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
M books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv-lists/bv-array-read.lisp
M books/kestrel/bv/bvmult.lisp

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


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

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

Log Message:
-----------
[C2C] Adapt to extended dynamic semantics.


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

Changed paths:

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


Commit: 3b41c1b75215b7ceffca754809cf2eb48490ac03
https://github.com/acl2/acl2/commit/3b41c1b75215b7ceffca754809cf2eb48490ac03
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-26 (Fri, 26 Sep 2025)

Changed paths:

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


Compare: https://github.com/acl2/acl2/compare/89e1c9425be6...3b41c1b75215
Reply all
Reply to author
Forward
0 new messages