[acl2/acl2] b311b8: Convert ISO-8859-1 non-ASCII bytes in books/ comme...

[Grant Jurgensen]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
Commit: b311b86e339aef0c33a6a6a5b2323259a8f4610c
https://github.com/acl2/acl2/commit/b311b86e339aef0c33a6a6a5b2323259a8f4610c
Author: Jim White <j...@fovi.com>
Date: 2026-02-13 (Fri, 13 Feb 2026)

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

Log Message:
-----------
Convert ISO-8859-1 non-ASCII bytes in books/ comments to UTF-8

Convert non-ASCII bytes in line comments (;) and block comments (#|...|#)
from ISO-8859-1 encoding to their UTF-8 equivalents in the books/ directory.

Changes:
- 60 files modified, 24,599 bytes converted
- All non-ASCII bytes were in comments, none in code
- Files already valid UTF-8 (quicklisp, test data) were skipped

Content types converted:
- Spanish accented characters (a/e/i/o/u-acute, ntilde) in workshop
papers by Ruiz, Rubio, Cowles-Gamboa-Euclid, Medina, and others
- Middle dot (U+00B7) section separators in multiset/unification proofs
- Guillemets and copyright symbols


Commit: 233ada8ce85fdd73d24f9d48a82c79357f246e23
https://github.com/acl2/acl2/commit/233ada8ce85fdd73d24f9d48a82c79357f246e23
Author: Grant Jurgensen <gr...@kestrel.edu>
Date: 2026-03-16 (Mon, 16 Mar 2026)

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

Log Message:
-----------
Merge pull request #1908 from jimwhite/utf8-books

Convert ISO-8859-1 non-ASCII bytes in books/ comments to UTF-8

Note that we will encourage UTF-8 in the future, but authors may still use ISO-8859-1 if that is their preference.


Compare: https://github.com/acl2/acl2/compare/f27136d4ef8e...233ada8ce85f

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

[Grant Jurgensen]

Branch: refs/heads/master

[acl2buildserver]

Branch: refs/heads/testing-kestrel

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

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

Log Message:
-----------
[FTY] Add missing dash in `deffold-reduce`-generated theorems.


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

Changed paths:
M books/kestrel/c/syntax/unambiguity.lisp

Log Message:
-----------
[C$] Remove handwritten theorems now redundant.

This became apparent after fixing some names of theorems generated by
`deffold-reduce`.


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

Changed paths:
M books/projects/pfcs/proof-support.lisp

Log Message:
-----------
[PFCS] Improve some variable names for consistency.


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

Changed paths:
M books/projects/pfcs/proof-support.lisp

Log Message:
-----------
[PFCS] Improve a variable name for consistency.


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

Changed paths:
M books/std/basic/top.lisp
A books/std/basic/yyyjoin.lisp

Log Message:
-----------
[Std/basic] Add `yyyjoin`.


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

Changed paths:
M books/projects/pfcs/convenience-constructors.lisp
M books/projects/pfcs/package.lsp

Log Message:
-----------
[PFCS] Use the newly added `yyyjoin` from Std/basic.


Commit: 13144e9cdf86e6fefb9a736ba8f5cb740f91f974
https://github.com/acl2/acl2/commit/13144e9cdf86e6fefb9a736ba8f5cb740f91f974
Author: Matt Kaufmann <matthew.j...@gmail.com>

Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:

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/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 doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Tweaks to hol-in-acl2 library. Fixes made to acl2-in-hol scripts. Synched doc.lisp etc.

Thanks to Alessandro Coglio for pointing out the script issue.


Commit: aa221be789d2af8d08ab5ead54052daa08b60699
https://github.com/acl2/acl2/commit/aa221be789d2af8d08ab5ead54052daa08b60699
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:

M books/doc/relnotes.lisp

Log Message:
-----------
Merge commit '25d10c770ec80248e371bde248e65ce39f5e9d29' into HEAD


Commit: 73d22f44eb68479ed344f5803c208f0135391b02
https://github.com/acl2/acl2/commit/73d22f44eb68479ed344f5803c208f0135391b02
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:

M bin/purity-acl2.sh
M books/doc/practices.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
A books/misc/character-encoding-test.acl2
M books/misc/character-encoding-test.lisp
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/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/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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


Commit: 73212ecd7eaf85d2667e7e0b0b91d8a1cfc27354
https://github.com/acl2/acl2/commit/73212ecd7eaf85d2667e7e0b0b91d8a1cfc27354
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:

M books/doc/relnotes.lisp

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


Commit: f27136d4ef8e71ac896de9618d022ad769c196bb
https://github.com/acl2/acl2/commit/f27136d4ef8e71ac896de9618d022ad769c196bb
Author: Matt Kaufmann <matthew.j...@gmail.com>

Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:

M books/projects/acl2-in-hol/lisp/a2ml.bash
M books/projects/acl2-in-hol/tests/inputs/Makefile

Log Message:
-----------
More fixes made to acl2-in-hol scripts.

Thanks to Alessandro Coglio for pointing out more issues with those
scripts.

Commit: 2b3340f83ec955cea3a0e6ab19773bf9eb610a65
https://github.com/acl2/acl2/commit/2b3340f83ec955cea3a0e6ab19773bf9eb610a65
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:

M books/kestrel/bitcoin/bech32.lisp

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


Commit: e19234e696354e01bf5048d93ecd23fe1fe5841f
https://github.com/acl2/acl2/commit/e19234e696354e01bf5048d93ecd23fe1fe5841f
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:
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/projects/acl2-in-hol/lisp/a2ml.bash
M books/projects/acl2-in-hol/tests/inputs/Makefile

Merge.


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

Changed paths:
M books/kestrel/x86/assumptions-new.lisp
M books/std/system/remove-dead-if-branches.lisp

Log Message:
-----------
Merge commit '1addd09ff2c9f55919c3d8111d5ab06b35c6151b' into HEAD


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

Changed paths:
M books/doc/relnotes.lisp
M books/doc/top.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

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


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

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

Log Message:
-----------
Merge commit '6574c9184466951edfacc0dbe41c3b122993bbd0' into HEAD


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

Log Message:
-----------
Merge commit '0503f60d27ee577256dc98fd86db3c0b3f70efe8' into HEAD


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

Changed paths:
M books/doc/practices.lisp
M books/doc/relnotes.lisp
M books/doc/top.lisp
M books/kestrel/bitcoin/bech32.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/std/system/remove-dead-if-branches.lisp
M books/system/doc/acl2-doc.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

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


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

Changed paths:
M bin/purity-acl2.sh
M books/GNUmakefile

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/air/model-0/air/pfcs-lifting.lisp
M books/kestrel/apt/doc.lisp
M books/kestrel/apt/isodata-doc.lisp
A books/kestrel/apt/simplify-conjunctions-tests.lisp
A books/kestrel/apt/simplify-conjunctions.lisp
M books/kestrel/apt/top.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/pseudocode.lisp
A books/kestrel/arm/rules.lisp
M books/kestrel/arm/top.lisp
M books/kestrel/axe/arm/examples/add/add-with-stop-pcs.lisp
M books/kestrel/axe/arm/examples/add/add.lisp
M books/kestrel/axe/arm/package.lsp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/bv-list-rules-axe.lisp
M books/kestrel/axe/dag-conjuncts.lisp
M books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags2.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter-utilities3.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/tester.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/prune-term.lisp
M books/kestrel/axe/prune-with-contexts-tests.lisp
M books/kestrel/axe/result-array-stobj.lisp
M books/kestrel/axe/rewriter-basic-tests.lisp
M books/kestrel/axe/rewriter-basic.lisp
M books/kestrel/axe/rewriter-tests.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/specialize.lisp
M books/kestrel/axe/strengthen-facts.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bitcoin/bech32.lisp
M books/kestrel/bv-lists/all-unsigned-byte-p2.lisp
M books/kestrel/bv-lists/append-arrays.lisp
M books/kestrel/bv-lists/bv-array-clear-range.lisp
M books/kestrel/bv-lists/bv-array-clear.lisp
M books/kestrel/bv-lists/bv-list-read-chunk-little.lisp
M books/kestrel/bv-lists/bvchop-list.lisp
M books/kestrel/bv-lists/bvchop-list2.lisp
M books/kestrel/bv-lists/bvnot-list.lisp
M books/kestrel/bv-lists/logext-list.lisp
M books/kestrel/bv/.sys/in...@useless-runes.lsp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bvcat-rules.lisp
M books/kestrel/bv/bvlt-def.lisp
M books/kestrel/bv/bvsx-rules.lisp
M books/kestrel/bv/intro.lisp
M books/kestrel/bv/logand-b.lisp
M books/kestrel/bv/single-bit.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-binary-strict-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
A books/kestrel/c/examples/README.md
A books/kestrel/c/examples/add-uints.lisp
A books/kestrel/c/examples/add_uints.c
A books/kestrel/c/examples/cert.acl2
A books/kestrel/c/examples/strcpy-safe-support.lisp
A books/kestrel/c/examples/strcpy-safe.lisp
A books/kestrel/c/examples/strcpy_safe.c
M books/kestrel/c/language/keywords.lisp
A books/kestrel/c/proof-support/const-folding.lisp
M books/kestrel/c/proof-support/exec-stmt-openers.lisp
M books/kestrel/c/proof-support/top.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
A books/kestrel/c/syntax/abstract-syntax-structurals.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/abstract-syntax.lisp
M books/kestrel/c/syntax/concrete-syntax.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/parser-messages.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/positions.lisp
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-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/reader.lisp
A books/kestrel/c/syntax/spans.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
M books/kestrel/c/syntax/tests/reader.lisp
M books/kestrel/c/syntax/token-concatenation.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/top.lisp
M books/kestrel/c/transformation/copy-fn.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/crypto/salsa/salsa20.lisp
M books/kestrel/error-checking/def-error-checker.lisp
M books/kestrel/risc-v/executable/decoding-executable.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/rflags-spec-sub.lisp
M books/kestrel/zcash/gadgets/a-3-3-1-alt-proof.lisp
M books/kestrel/zcash/gadgets/a-3-3-1-proof.lisp
M books/kestrel/zcash/gadgets/a-3-3-4-proof.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/aleo/leo/early-version/definition/expressions.lisp
M books/projects/aleo/leo/early-version/definition/lexer.lisp
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/pfcs/.sys/parser-i...@useless-runes.lsp
M books/projects/pfcs/lifting.lisp
M books/projects/pfcs/parser-interface.lisp
M books/projects/pfcs/proof-support.lisp
M books/projects/pfcs/r1cs-bridge.lisp
M books/projects/pfcs/r1cs-subset.lisp
M books/projects/pfcs/semantics.lisp
M books/projects/pfcs/syntax-abstraction.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/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: 45086dd9a5f90db0004937922647bedf4bca1b75
https://github.com/acl2/acl2/commit/45086dd9a5f90db0004937922647bedf4bca1b75
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

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


Commit: 6b2177722615264e303b9597b77fc74092c31eb1
https://github.com/acl2/acl2/commit/6b2177722615264e303b9597b77fc74092c31eb1
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

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


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

Changed paths:
M books/std/basic/yyyjoin.lisp

Log Message:
-----------
[Std/basic] Add XDOC parent.


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

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

Log Message:
-----------
[FTY] Improve proofs generated by `deffold-reduce`.

Generate some enabled hints for the termination proofs.


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

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


Compare: https://github.com/acl2/acl2/compare/d0337451a2fc...9dbffa503d54