[acl2/acl2] 95f878: Add proof of a distributive law for a HOL expressi...

0 views
Skip to first unread message

MattKaufmann

unread,
Sep 22, 2025, 6:51:33 PM (3 days ago) Sep 22
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 95f8781ee227053c49ae00d04982e0959a3a2f85
https://github.com/acl2/acl2/commit/95f8781ee227053c49ae00d04982e0959a3a2f85
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
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

Log Message:
-----------
Add proof of a distributive law for a HOL expression evaluator, carried out by reducing it to a trivial proof of a corresponding theorem about an ACL2 expression evaluator.

See books/projects/hol-in-acl2/examples/eval-poly-proof.lisp. This
work takes advantage of the translation from HOL to ACL2 carried out
with Konrad Slind, by applying Konrad's translator and my defhol macro
to translate the desired HOL theorem into ACL2 as extended by the ZF
set theory books.



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

acl2buildserver

unread,
Sep 22, 2025, 6:52:34 PM (3 days ago) Sep 22
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Sep 23, 2025, 4:04:35 PM (2 days ago) Sep 23
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 95f8781ee227053c49ae00d04982e0959a3a2f85
https://github.com/acl2/acl2/commit/95f8781ee227053c49ae00d04982e0959a3a2f85
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
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

Log Message:
-----------
Add proof of a distributive law for a HOL expression evaluator, carried out by reducing it to a trivial proof of a corresponding theorem about an ACL2 expression evaluator.

See books/projects/hol-in-acl2/examples/eval-poly-proof.lisp. This
work takes advantage of the translation from HOL to ACL2 carried out
with Konrad Slind, by applying Konrad's translator and my defhol macro
to translate the desired HOL theorem into ACL2 as extended by the ZF
set theory books.


Commit: 45c9f854b72a1d67d02dbfdc5c3c3e576c65f9da
https://github.com/acl2/acl2/commit/45c9f854b72a1d67d02dbfdc5c3c3e576c65f9da
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/projects/hol-in-acl2/to-do.txt

Log Message:
-----------
Add a to-do item.


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

Changed paths:
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/simpadd0.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

Log Message:
-----------
[C2C] Improve interface of `simpadd0`.

Have it take keyword inputs `:const-old` and `:const-new`.


Commit: 271ae997abda9304c74f41bed4eaed72b0b3319a
https://github.com/acl2/acl2/commit/271ae997abda9304c74f41bed4eaed72b0b3319a
Author: ACL2 Build Server <acl2bui...@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/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

Log Message:
-----------
Merge commit '4aeac394cf784a1ccc1e3af7393fb7b70bfad79d' into HEAD


Commit: a363e56ae660dade937ea1fc80f3bef908b1904b
https://github.com/acl2/acl2/commit/a363e56ae660dade937ea1fc80f3bef908b1904b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 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] Improve formalization of dynamic semantics.

Make `exec-expr-call-or-asg` also return a result, besides the new computation
state, for more uniformity.


Commit: 23858b1641d9eb3f488d4c9f7ac9783022349757
https://github.com/acl2/acl2/commit/23858b1641d9eb3f488d4c9f7ac9783022349757
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 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

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


Commit: 06f4921340ab65ad55c3103d0779ac0f23f540ef
https://github.com/acl2/acl2/commit/06f4921340ab65ad55c3103d0779ac0f23f540ef
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/printer.lisp
A books/kestrel/c/syntax/printing.lisp
M books/kestrel/c/syntax/top.lisp

Log Message:
-----------
[C$] Add a file and topic for printing.

Put the printer under there.


Commit: 1e34c90c2f0ef1d1316b21cf7095d03978999d6c
https://github.com/acl2/acl2/commit/1e34c90c2f0ef1d1316b21cf7095d03978999d6c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
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

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


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Improve some AST names.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/splitgso.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Improve some AST names.


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

Changed paths:
A books/kestrel/fty/character-set.lisp
M books/kestrel/fty/top.lisp

Log Message:
-----------
[FTY] Add fixtype of osets of characters.


Commit: 4cc080371e8f624cf285a550fb6f0adfffe47739
https://github.com/acl2/acl2/commit/4cc080371e8f624cf285a550fb6f0adfffe47739
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
A books/kestrel/fty/any-nat-map.lisp
M books/kestrel/fty/top.lisp

Log Message:
-----------
[FTY] Add fixtype of omaps from anything to naturals.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Improve some AST names.


Commit: 7583eede2b6ac7ead0912cc9c210f7387b28bc45
https://github.com/acl2/acl2/commit/7583eede2b6ac7ead0912cc9c210f7387b28bc45
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
A books/kestrel/fty/character-any-map.lisp
M books/kestrel/fty/top.lisp

Log Message:
-----------
[FTY] Add fixtype of omaps from characters to anything.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
A books/kestrel/c/syntax/printing.lisp
M books/kestrel/c/syntax/standard.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.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/splitgso.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


Commit: 85d14dd4076f2813b722641f23104c37fbb965e5
https://github.com/acl2/acl2/commit/85d14dd4076f2813b722641f23104c37fbb965e5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
A books/kestrel/fty/any-nat-map.lisp
A books/kestrel/fty/character-any-map.lisp
A books/kestrel/fty/character-set.lisp
M books/kestrel/fty/top.lisp

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


Commit: 8e392a36d1128fcb70487f403673e88be81573cf
https://github.com/acl2/acl2/commit/8e392a36d1128fcb70487f403673e88be81573cf
Author: David Taylor <jdavid...@outlook.com>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/system/doc/acl2-doc.lisp

Log Message:
-----------
Minor corrections in acl2-doc


Commit: 54d516353d962e62eb7669c6f5161f274c5a8a32
https://github.com/acl2/acl2/commit/54d516353d962e62eb7669c6f5161f274c5a8a32
Author: MattKaufmann <kauf...@cs.utexas.edu>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/system/doc/acl2-doc.lisp

Log Message:
-----------
Merge pull request #1856 from copperteal/minor-doc-fixes

Minor corrections in acl2-doc


Commit: 2f56a758c818c219981c1f1d7d7f573ba3de6e4e
https://github.com/acl2/acl2/commit/2f56a758c818c219981c1f1d7d7f573ba3de6e4e
Author: ACL2 Build Server <acl2bui...@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/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.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/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/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/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
A books/kestrel/fty/any-nat-map.lisp
A books/kestrel/fty/character-any-map.lisp
A books/kestrel/fty/character-set.lisp
M books/kestrel/fty/top.lisp

Log Message:
-----------
Merge commit '85d14dd4076f2813b722641f23104c37fbb965e5' into HEAD


Commit: e4cd8b21533f9dd75f938fcb20543db4f562b479
https://github.com/acl2/acl2/commit/e4cd8b21533f9dd75f938fcb20543db4f562b479
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-09-23 (Tue, 23 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: 2b7554cc9ba2a9290b8867982a3b8d7c9c7a5215
https://github.com/acl2/acl2/commit/2b7554cc9ba2a9290b8867982a3b8d7c9c7a5215
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2025-09-23 (Tue, 23 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/preprocess-file.lisp
M books/kestrel/c/syntax/tests/input-files.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

Log Message:
-----------
Merge commit '0e4a6ef6defe1faf8ee372d7404b08d6e68791eb' into HEAD


Commit: 41d19a76b750623bffa8f86e368c92e98ac56275
https://github.com/acl2/acl2/commit/41d19a76b750623bffa8f86e368c92e98ac56275
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-23 (Tue, 23 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/preprocess-file.lisp
A books/kestrel/fty/string-stringlist-map.lisp
M books/kestrel/fty/top.lisp

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


Compare: https://github.com/acl2/acl2/compare/932e0fb45ffb...41d19a76b750
Reply all
Reply to author
Forward
0 new messages