[acl2/acl2] 63c445: [C$] Downcase some code (forgotten).

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 63c44578ede629d46a1d9c8f490193cf3ad95a95
https://github.com/acl2/acl2/commit/63c44578ede629d46a1d9c8f490193cf3ad95a95
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-15 (Sun, 15 Mar 2026)

Changed paths:
M books/kestrel/c/proof-support/const-ast-accessors.lisp

Log Message:
-----------
[C$] Downcase some code (forgotten).


Commit: 7becd0e4ce030737a2e48c506aa36ea77dcb0c50
https://github.com/acl2/acl2/commit/7becd0e4ce030737a2e48c506aa36ea77dcb0c50
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-15 (Sun, 15 Mar 2026)

Changed paths:
M books/kestrel/c/proof-support/exec-stmt-openers.lisp

Log Message:
-----------
[C$] Improve organization of statement openers.


Commit: ec2a445514462a0c674559b75cf11fb7ea1e46da
https://github.com/acl2/acl2/commit/ec2a445514462a0c674559b75cf11fb7ea1e46da
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-15 (Sun, 15 Mar 2026)

Changed paths:
M books/kestrel/c/proof-support/exec-stmt-while-openers.lisp

Log Message:
-----------
[C] Improve organization of `while` opener rules.


Commit: 77bfa5034ce189acd0238aa7764676a13db0b739
https://github.com/acl2/acl2/commit/77bfa5034ce189acd0238aa7764676a13db0b739
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-15 (Sun, 15 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/syntaxp.lisp

Log Message:
-----------
[ATC] Use controlled configuration.


Commit: 37371ab6cd7f7bb273533d6905ae4413ce1c1dc2
https://github.com/acl2/acl2/commit/37371ab6cd7f7bb273533d6905ae4413ce1c1dc2
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/doc/publications.lisp

Log Message:
-----------
[xdoc] Ensure pubs-workshops get updated when needed.


Commit: 13f98f1bffeffa8467c0afef9577387bdf46feb7
https://github.com/acl2/acl2/commit/13f98f1bffeffa8467c0afef9577387bdf46feb7
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/workshops/references/workshops.bib

Log Message:
-----------
[workshops] Add bibtex for 2025 workshop.

This is the raw bibtex from EPTCS. Next I will edit it to match the format of previous years.


Commit: 5da6a3236ae9579dc751c4ab5be147ebd99b52e0
https://github.com/acl2/acl2/commit/5da6a3236ae9579dc751c4ab5be147ebd99b52e0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M bin/purity-acl2.sh
M books/defexec/dag-unification/dag-unification-l.lisp
M books/defexec/dag-unification/dag-unification-rules.lisp
M books/defexec/dag-unification/dag-unification-st.lisp
M books/defexec/dag-unification/dags.lisp
M books/defexec/dag-unification/list-unification-rules.lisp
M books/defexec/dag-unification/matching.lisp
M books/defexec/dag-unification/subsumption-subst.lisp
M books/defexec/dag-unification/subsumption.lisp
M books/defexec/dag-unification/terms-as-dag.lisp
M books/defexec/dag-unification/terms-dag-stobj.lisp
M books/defexec/dag-unification/terms.lisp
M books/doc/practices.lisp
M books/doc/relnotes.lisp
M books/doc/top.lisp
M books/kestrel/bitcoin/bech32.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-files.lisp
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/token-concatenation.lisp
M books/kestrel/x86/assumptions-new.lisp
A books/misc/character-encoding-test.acl2
M books/misc/character-encoding-test.lisp
M books/projects/acl2-in-hol/lisp/a2ml.bash
M books/projects/acl2-in-hol/lisp/axioms-essence.bash
M books/projects/acl2-in-hol/lisp/book-essence.bash
M books/projects/acl2-in-hol/tests/doit
M books/projects/acl2-in-hol/tests/inputs/Makefile
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/set-theory/cantor.lisp
M books/std/system/remove-dead-if-branches.lisp
M books/system/doc/acl2-doc.lisp
M books/workshops/2000/medina/polynomials/polynomial.lisp
M books/workshops/2000/medina/polynomials/term.lisp
M books/workshops/2000/ruiz/multiset/examples/ackermann/ackermann.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/confluence.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/newman.lisp
M books/workshops/2000/ruiz/multiset/multiset.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/dags.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/terms.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/anti-unification.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/matching.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/renamings.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/terms.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification-pattern.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp
M books/workshops/2004/ruiz-et-al/support/basic.lisp
M books/workshops/2004/ruiz-et-al/support/dag-unification-rules.lisp
M books/workshops/2004/ruiz-et-al/support/dags.lisp
M books/workshops/2004/ruiz-et-al/support/matching.lisp
M books/workshops/2004/ruiz-et-al/support/prefix-unification-rules.lisp
M books/workshops/2004/ruiz-et-al/support/q-dag-unification-rules.lisp
M books/workshops/2004/ruiz-et-al/support/q-dag-unification-st.lisp
M books/workshops/2004/ruiz-et-al/support/q-dag-unification.lisp
M books/workshops/2004/ruiz-et-al/support/subsumption-subst.lisp
M books/workshops/2004/ruiz-et-al/support/subsumption.lisp
M books/workshops/2004/ruiz-et-al/support/terms-as-dag.lisp
M books/workshops/2004/ruiz-et-al/support/terms.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/coe-fld.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-producto.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-suma.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuforma-normal.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fumonomio.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuopuesto.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio-normalizado.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fusuma.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/futermino.lisp
M books/workshops/2007/cowles-et-al/support/greve/ack.lisp
M books/workshops/2007/cowles-et-al/support/greve/defminterm.lisp
M books/workshops/2007/cowles-et-al/support/greve/defxch.lisp
M books/workshops/2007/rubio/support/abstract-reductions/confluence.lisp
M books/workshops/2007/rubio/support/abstract-reductions/convergent.lisp
M books/workshops/2007/rubio/support/abstract-reductions/newman.lisp
M books/workshops/2007/rubio/support/multisets/multiset.lisp
M books/workshops/2007/rubio/support/simplicial-topology/generate-degenerate.lisp
M books/xdoc/save-classic.lisp
M books/xdoc/save-fancy.lisp
M books/xdoc/save-rendered.lisp
M books/xdoc/save.lisp
M books/xdoc/topics.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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


Commit: eb1f39a2e47571628fd38c329a76b443971a60c1
https://github.com/acl2/acl2/commit/eb1f39a2e47571628fd38c329a76b443971a60c1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-binary-strict-pure-gen.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-cast.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-unary.lisp
M books/kestrel/c/atc/symbolic-execution-rules/syntaxp.lisp
M books/kestrel/c/atc/symbolic-execution-rules/test-value.lisp
M books/kestrel/c/atc/tag-generation.lisp

Log Message:
-----------
[C] Make a function name more generic.


Commit: b38182aae3c98314c67e0cb91607f510ed963b18
https://github.com/acl2/acl2/commit/b38182aae3c98314c67e0cb91607f510ed963b18
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-binary-strict-pure-gen.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-cast.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-unary.lisp
M books/kestrel/c/atc/symbolic-execution-rules/syntaxp.lisp
M books/kestrel/c/atc/symbolic-execution-rules/test-value.lisp
M books/kestrel/c/atc/tag-generation.lisp

Log Message:
-----------
[C] Shorten function name.


Commit: b2ffb4593c09539e8797e4a3fde91adebbe81e63
https://github.com/acl2/acl2/commit/b2ffb4593c09539e8797e4a3fde91adebbe81e63
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-arrsub.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-binary-strict-pure-gen.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-cast.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-unary.lisp
R books/kestrel/c/atc/symbolic-execution-rules/syntaxp.lisp
M books/kestrel/c/atc/symbolic-execution-rules/test-value.lisp
M books/kestrel/c/atc/tag-generation.lisp
A books/kestrel/c/proof-support/syntaxp-for-expr-pure.lisp
M books/kestrel/c/proof-support/top.lisp

Log Message:
-----------
[C] Move some material to proof support.


Commit: 4c8ed828e3d6cedc0df22d2dc8fdd0cb019d966b
https://github.com/acl2/acl2/commit/4c8ed828e3d6cedc0df22d2dc8fdd0cb019d966b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/workshops/references/workshops.bib

Log Message:
-----------
[workhops] Improve bibtex for 2025 workshop.


Commit: b03196148e136d6dd612f20bf9965132f3b5e47f
https://github.com/acl2/acl2/commit/b03196148e136d6dd612f20bf9965132f3b5e47f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/proof-support/exec-stmt-openers.lisp

Log Message:
-----------
[C proof support] Tweak some doc.


Commit: 845849b52f49da5ff92d394be384e3d1d4212c8e
https://github.com/acl2/acl2/commit/845849b52f49da5ff92d394be384e3d1d4212c8e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
A books/kestrel/c/proof-support/exec-expr-pure-openers.lisp
M books/kestrel/c/proof-support/top.lisp

Log Message:
-----------
[C proof support] Start material on pure expression execution.

Start moving material from ATC to here.


Commit: 7e9b4f4b60feac70e3330a013d1be913e5901887
https://github.com/acl2/acl2/commit/7e9b4f4b60feac70e3330a013d1be913e5901887
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/proof-support/exec-expr-pure-openers.lisp

Log Message:
-----------
[C proof support] Move and document better a function.


Commit: 9fae97094ec15c9c161aa3699a762e9ea9a75678
https://github.com/acl2/acl2/commit/9fae97094ec15c9c161aa3699a762e9ea9a75678
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/proof-support/exec-expr-pure-openers.lisp

Log Message:
-----------
[C proof support] Move and document another function.


Commit: 88ed89030303dc665307fd757ac8de05e0f3ca53
https://github.com/acl2/acl2/commit/88ed89030303dc665307fd757ac8de05e0f3ca53
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/proof-support/exec-stmt-openers.lisp

Log Message:
-----------
[C proof support] Improve file layout.


Commit: 576b74a07f288798a50d23b4c3570d6ce86daab1
https://github.com/acl2/acl2/commit/576b74a07f288798a50d23b4c3570d6ce86daab1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/proof-support/exec-expr-pure-openers.lisp

Log Message:
-----------
[C proof support] Move rules about pure expression execution.


Commit: ac720462d5493b233b30547b5851615566f48a23
https://github.com/acl2/acl2/commit/ac720462d5493b233b30547b5851615566f48a23
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/doc/publications.lisp
M books/kestrel/bibtex/xdoc-generation.lisp
M books/workshops/references/workshops.bib

Log Message:
-----------
[doc] Improve doc for the Workshop publications.

Add headers to separate each group.


Commit: 25518dd3883b80604f5457e74cea36cfa7520ac4
https://github.com/acl2/acl2/commit/25518dd3883b80604f5457e74cea36cfa7520ac4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

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/ascii-identifiers.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/printer.lisp
M books/kestrel/c/syntax/standard.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/copy-fn.lisp
M books/kestrel/c/transformation/rename.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
[C$] Extend ASTs for translation items.

Include preprocessing conditionals. These are for the ones preserved by our
preprocessor.


Commit: dd2618ea29932e815cdd7200945f8a3cdc286669
https://github.com/acl2/acl2/commit/dd2618ea29932e815cdd7200945f8a3cdc286669
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/doc/relnotes.lisp
A books/kestrel/axe/arm/doc.acl2
A books/kestrel/axe/arm/doc.lisp
M books/kestrel/axe/doc.lisp
M books/projects/pfcs/convenience-constructors.lisp
M books/projects/pfcs/package.lsp
M books/projects/pfcs/proof-support.lisp
M books/std/basic/top.lisp
A books/std/basic/yyyjoin.lisp

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


Commit: 7647b8d695d1cc479c1210ce7139f834824f75b0
https://github.com/acl2/acl2/commit/7647b8d695d1cc479c1210ce7139f834824f75b0
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/workshops/references/workshops.bib

Log Message:
-----------
[workshops] Improve bibtex.

Format author names like previous years.


Commit: d0337451a2fc76b39f25d1b81dced82469b4a16b
https://github.com/acl2/acl2/commit/d0337451a2fc76b39f25d1b81dced82469b4a16b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/doc/publications.lisp

Log Message:
-----------
[doc] Add xdoc parent.


Commit: 9dbffa503d54f4a9e0df384479b2a7cccd96a7b6
https://github.com/acl2/acl2/commit/9dbffa503d54f4a9e0df384479b2a7cccd96a7b6
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/doc/publications.lisp
M books/kestrel/bibtex/xdoc-generation.lisp
M books/workshops/references/workshops.bib

Log Message:
-----------
Merge commit 'd0337451a2fc76b39f25d1b81dced82469b4a16b' into HEAD


Commit: 1b187f32e3ffae3fd05f085d13253c26be532fd8
https://github.com/acl2/acl2/commit/1b187f32e3ffae3fd05f085d13253c26be532fd8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/fty/deffold-reduce.lisp

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


Commit: c1a8414b6c50542fb1f2212c537d5e8bfc3bafb6
https://github.com/acl2/acl2/commit/c1a8414b6c50542fb1f2212c537d5e8bfc3bafb6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/proof-support/exec-stmt-openers.lisp

Log Message:
-----------
[C proof support] Delete redundant parents.


Commit: 2f2fbf90620989a2223b014a7136b07948a1d17d
https://github.com/acl2/acl2/commit/2f2fbf90620989a2223b014a7136b07948a1d17d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/proof-support/exec-stmt-openers.lisp

Log Message:
-----------
[C proof support] Tweak some doc.


Commit: 860f4903180b878f4c803e886f473af226f3f943
https://github.com/acl2/acl2/commit/860f4903180b878f4c803e886f473af226f3f943
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp

Log Message:
-----------
[C$] [C2C] Reduce book inclusions.

After improving the proofs generated by `fty::deffold-reduce`.


Commit: 9e6fcdedcb1508f5bf3f0e0d6463bfa65143a743
https://github.com/acl2/acl2/commit/9e6fcdedcb1508f5bf3f0e0d6463bfa65143a743
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/proof-support/exec-expr-pure-openers.lisp

Log Message:
-----------
[C proof support] Add rule lists and rulesets.

Also reorder some theorems.


Commit: f4e19ec0c3aa2d05c6c28dd0280f5e29a29e5b4d
https://github.com/acl2/acl2/commit/f4e19ec0c3aa2d05c6c28dd0280f5e29a29e5b4d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp

Log Message:
-----------
[ATC] Use rule list from proof support sub-library.


Commit: dcd4250b22e55e74fafb395f2b2bed6d5bf9459e
https://github.com/acl2/acl2/commit/dcd4250b22e55e74fafb395f2b2bed6d5bf9459e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-arrsub.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-binary-strict-pure-gen.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-cast.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-unary.lisp
R books/kestrel/c/atc/symbolic-execution-rules/syntaxp.lisp
M books/kestrel/c/atc/symbolic-execution-rules/test-value.lisp
M books/kestrel/c/atc/tag-generation.lisp
M books/kestrel/c/proof-support/const-ast-accessors.lisp
A books/kestrel/c/proof-support/exec-expr-pure-openers.lisp
M books/kestrel/c/proof-support/exec-stmt-openers.lisp
M books/kestrel/c/proof-support/exec-stmt-while-openers.lisp
A books/kestrel/c/proof-support/syntaxp-for-expr-pure.lisp
M books/kestrel/c/proof-support/top.lisp

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


Commit: cc283622a1a3b68e00662e6e06dd995841487753
https://github.com/acl2/acl2/commit/cc283622a1a3b68e00662e6e06dd995841487753
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Synched doc.lisp etc.


Commit: d8a170136e1471e48ea1788ee63f351a13183695
https://github.com/acl2/acl2/commit/d8a170136e1471e48ea1788ee63f351a13183695
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/doc/publications.lisp
M books/kestrel/bibtex/xdoc-generation.lisp
M books/workshops/references/workshops.bib

Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/master'


Commit: f0cc782001dc4cf890cad77228f6b34a3664ef69
https://github.com/acl2/acl2/commit/f0cc782001dc4cf890cad77228f6b34a3664ef69
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/doc/publications.lisp
M books/kestrel/bibtex/xdoc-generation.lisp
M books/workshops/references/workshops.bib

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


Commit: ab76c4140c595c98ff63c9ecb3453b17d050de2e
https://github.com/acl2/acl2/commit/ab76c4140c595c98ff63c9ecb3453b17d050de2e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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


Compare: https://github.com/acl2/acl2/compare/906477f5de3c...ab76c4140c59

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

[Alessandro Coglio]

Branch: refs/heads/master

Commit: f0cc782001dc4cf890cad77228f6b34a3664ef69
https://github.com/acl2/acl2/commit/f0cc782001dc4cf890cad77228f6b34a3664ef69
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/doc/publications.lisp
M books/kestrel/bibtex/xdoc-generation.lisp
M books/workshops/references/workshops.bib

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


Commit: ab76c4140c595c98ff63c9ecb3453b17d050de2e
https://github.com/acl2/acl2/commit/ab76c4140c595c98ff63c9ecb3453b17d050de2e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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

Commit: 7bab5d1cbb1684c85f9fee5f691becf871456b87
https://github.com/acl2/acl2/commit/7bab5d1cbb1684c85f9fee5f691becf871456b87
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-18 (Wed, 18 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Fix XDOC.


Commit: 07c0959aece490ced6ff00a13cc9d4425cffb805
https://github.com/acl2/acl2/commit/07c0959aece490ced6ff00a13cc9d4425cffb805
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-22 (Sun, 22 Mar 2026)

Changed paths:
M acl2.lisp
M books/GNUmakefile
M books/doc/relnotes.lisp
M books/kestrel/bibtex/xdoc-generation.lisp
M books/kestrel/fty/deffold-map.lisp

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


Commit: ae717e8f83805b4d619d4ad98ee92af45dcad32b
https://github.com/acl2/acl2/commit/ae717e8f83805b4d619d4ad98ee92af45dcad32b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-22 (Sun, 22 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Fix XDOC link.


Compare: https://github.com/acl2/acl2/compare/36851786c69a...ae717e8f8380

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

Commit: cc283622a1a3b68e00662e6e06dd995841487753
https://github.com/acl2/acl2/commit/cc283622a1a3b68e00662e6e06dd995841487753
Author: Matt Kaufmann <kauf...@cs.utexas.edu>

Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------

Synched doc.lisp etc.


Commit: d8a170136e1471e48ea1788ee63f351a13183695
https://github.com/acl2/acl2/commit/d8a170136e1471e48ea1788ee63f351a13183695
Author: Matt Kaufmann <kauf...@cs.utexas.edu>

Date: 2026-03-17 (Tue, 17 Mar 2026)

Changed paths:
M books/doc/publications.lisp
M books/kestrel/bibtex/xdoc-generation.lisp
M books/workshops/references/workshops.bib

Log Message:
-----------

Merge remote-tracking branch 'remotes/origin/master'

Commit: f55950d3abe4e2273d1e96fb663bf18d19457808
https://github.com/acl2/acl2/commit/f55950d3abe4e2273d1e96fb663bf18d19457808

Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-03-18 (Wed, 18 Mar 2026)

Changed paths:

M books/kestrel/fty/deffold-map.lisp

Log Message:
-----------
Merge commit '4618d9ecfbd85f757e4b7cdeec87c0d1eb107b4f' into HEAD


Commit: 701acd698099b047e012cb9ce03afec2990e56a8
https://github.com/acl2/acl2/commit/701acd698099b047e012cb9ce03afec2990e56a8

Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-03-19 (Thu, 19 Mar 2026)

Changed paths:

M books/GNUmakefile
M books/doc/relnotes.lisp
M books/kestrel/bibtex/xdoc-generation.lisp

Log Message:
-----------
Merge commit 'b3e0ef9bc0e3adfce2fa20d976bf8ee738094a16' into HEAD


Commit: 36851786c69a1b36d7c5bec8ee59b1eb4d550eac
https://github.com/acl2/acl2/commit/36851786c69a1b36d7c5bec8ee59b1eb4d550eac
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-03-19 (Thu, 19 Mar 2026)

Changed paths:
M acl2.lisp

Log Message:
-----------
This is a dummy commit, to mark the starting point for releasing the next version (ACL2 8.7).

Commit: 07c0959aece490ced6ff00a13cc9d4425cffb805
https://github.com/acl2/acl2/commit/07c0959aece490ced6ff00a13cc9d4425cffb805
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-22 (Sun, 22 Mar 2026)

Changed paths:
M acl2.lisp
M books/GNUmakefile
M books/doc/relnotes.lisp
M books/kestrel/bibtex/xdoc-generation.lisp
M books/kestrel/fty/deffold-map.lisp

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


Commit: ae717e8f83805b4d619d4ad98ee92af45dcad32b
https://github.com/acl2/acl2/commit/ae717e8f83805b4d619d4ad98ee92af45dcad32b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-22 (Sun, 22 Mar 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Fix XDOC link.

Compare: https://github.com/acl2/acl2/compare/b3e0ef9bc0e3...ae717e8f8380