[acl2/acl2] 4862b4: [doc] Add new doc topic on Emacs workflow.

0 views

Skip to first unread message

Eric W. Smith

unread,

Mar 17, 2026, 4:38:26 AM (11 days ago) Mar 17

to acl2-...@googlegroups.com

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 4862b4949e7e688a303b664bd1bb4804b788520c
https://github.com/acl2/acl2/commit/4862b4949e7e688a303b664bd1bb4804b788520c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-02 (Mon, 02 Feb 2026)

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
[doc] Add new doc topic on Emacs workflow.

Thanks to Matt Kaufmann for helpful feedback.

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

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
[doc] Improve links.

Commit: 616435b2eb4600466c5f0dec693a7a71fa8d3842
https://github.com/acl2/acl2/commit/616435b2eb4600466c5f0dec693a7a71fa8d3842
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-03 (Tue, 03 Feb 2026)

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
[doc] Improve emacs-workflow doc.

Thanks to Grant Jurgensen for feedback I incorporated in this commit.

Commit: 5b1a4f08750506e8a527e3eedace4a2e7272278b
https://github.com/acl2/acl2/commit/5b1a4f08750506e8a527e3eedace4a2e7272278b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-03 (Tue, 03 Feb 2026)

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

Log Message:
-----------
[doc] Improve :doc emacs.

Thanks to Matt Kaufmann and Grant Jurgensen for helpful discussions/suggestions.

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

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

Log Message:
-----------
[doc] Apply suggestion from Grant Jurgensen.

Commit: 6574c9184466951edfacc0dbe41c3b122993bbd0
https://github.com/acl2/acl2/commit/6574c9184466951edfacc0dbe41c3b122993bbd0
Author: Eric W. Smith <48038799+eri...@users.noreply.github.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 pull request #1903 from acl2/emacs-workflow

[doc] Add new doc topic on Emacs workflow.

Compare: https://github.com/acl2/acl2/compare/e993a2c0ba91...6574c9184466

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

acl2buildserver

unread,

Mar 17, 2026, 5:23:50 AM (11 days ago) Mar 17

to acl2-...@googlegroups.com

Branch: refs/heads/master

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

Compare: https://github.com/acl2/acl2/compare/3295a0ee8eec...606e8538d902

acl2buildserver

unread,

Mar 17, 2026, 5:24:44 AM (11 days ago) Mar 17

to acl2-...@googlegroups.com

Branch: refs/heads/testing

Alessandro Coglio

unread,

Mar 17, 2026, 6:33:39 AM (11 days ago) Mar 17

to acl2-...@googlegroups.com

Branch: refs/heads/testing-user-01

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: 6d44c857042ceb58ffc71181bb1a9659cb237b27
https://github.com/acl2/acl2/commit/6d44c857042ceb58ffc71181bb1a9659cb237b27
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-03-12 (Thu, 12 Mar 2026)

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
[doc] Improve best-practices

Refine advice around non-ASCII characters and file licensing.

Commit: 21d30000000d65ab01658a20f6b7a8eb7f90d01b
https://github.com/acl2/acl2/commit/21d30000000d65ab01658a20f6b7a8eb7f90d01b
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-03-12 (Thu, 12 Mar 2026)

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
[doc] Edit character encoding advice

Thanks to Eric McCarthy for suggesting this change.

Co-authored-by: Eric McCarthy <7607035+...@users.noreply.github.com>

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

Changed paths:
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:
-----------
[xdoc] Allow missing parents to cause an error.

The new :error-on-missing-parents option to xdoc::save is nil by default but is set to t for the main manual build.

Commit: 67118b2ed3d2179d684663da4550321eff31acad
https://github.com/acl2/acl2/commit/67118b2ed3d2179d684663da4550321eff31acad
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-03-13 (Fri, 13 Mar 2026)

Changed paths:
A books/misc/character-encoding-test.acl2
M books/misc/character-encoding-test.lisp

Log Message:
-----------
[misc] Add character-encoding-test.acl2

This adds a test described in comments in character-encoding-test.lisp.
The limitation of older SBCL versions no longer seems to apply. The
comments were updated accordingly.

This also removes an outdated comment about the distributes
emacs-acl2.el file.

Commit: 923ccc19c2d438e2a7a13d6fcc842b48d7d8815a
https://github.com/acl2/acl2/commit/923ccc19c2d438e2a7a13d6fcc842b48d7d8815a
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-03-13 (Fri, 13 Mar 2026)

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

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

[doc] Edit character-encoding and add using-utf-8 topic

This removes the suggestion to configure Emacs to save files with a
Latin-1 encoding. It also adds a new topic, using-utf-8, which is
mentioned from character-encodings and which describes the potentially
surprising behavior when using UTF-8-encoded characters in ACL2.

Commit: 7cd2eabc48db6e8ca9ef457dd63d219a9ad18a81
https://github.com/acl2/acl2/commit/7cd2eabc48db6e8ca9ef457dd63d219a9ad18a81
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-03-13 (Fri, 13 Mar 2026)

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

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

[doc] Edit :doc using-utf-8

Thanks to Matt Kaufmann for suggesting this change to the wording.

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: 362638f9d8d80947aa19d70398df7cb2b846788e
https://github.com/acl2/acl2/commit/362638f9d8d80947aa19d70398df7cb2b846788e
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-03-15 (Sun, 15 Mar 2026)

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

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

[doc] Update :doc using-utf-8

Incorporated Eric Smith's advice to add further background on the
logical picture of ACL2 characters and strings.

Commit: 1313a031f94b83e5ff4d9e5875788dd9ebe835e3
https://github.com/acl2/acl2/commit/1313a031f94b83e5ff4d9e5875788dd9ebe835e3
Author: Grant Jurgensen <gr...@kestrel.edu>
Date: 2026-03-15 (Sun, 15 Mar 2026)

Changed paths:
A books/misc/character-encoding-test.acl2
M books/misc/character-encoding-test.lisp

M books/system/doc/acl2-doc.lisp

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

Merge pull request #1918 from gjurgensen/gj-char-encoding

[doc] Edit `character-encoding` and add `using-utf-8` topic

Commit: 7c907ebed533d767896e9c76729d4eccb2e7bc3d
https://github.com/acl2/acl2/commit/7c907ebed533d767896e9c76729d4eccb2e7bc3d

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

Date: 2026-03-15 (Sun, 15 Mar 2026)

Changed paths:
A books/misc/character-encoding-test.acl2
M books/misc/character-encoding-test.lisp

M books/system/doc/acl2-doc.lisp

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

Merge commit '1313a031f94b83e5ff4d9e5875788dd9ebe835e3' into HEAD

Commit: b91ae3c5efea5cc515d1ce71aa183035beb74a5c
https://github.com/acl2/acl2/commit/b91ae3c5efea5cc515d1ce71aa183035beb74a5c
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-03-15 (Sun, 15 Mar 2026)

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
[doc] Update best-practices with reference to :doc using-utf-8

Commit: a0876656d5a6369239072d39615a619f3a90d8a1
https://github.com/acl2/acl2/commit/a0876656d5a6369239072d39615a619f3a90d8a1
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-03-15 (Sun, 15 Mar 2026)

Changed paths:
M books/doc/relnotes.lisp
M books/kestrel/air/model-0/air/pfcs-lifting.lisp
M books/kestrel/apt/isodata-doc.lisp
M books/kestrel/c/proof-support/const-folding.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.lisp
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/validator.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/error-checking/def-error-checker.lisp
M books/kestrel/risc-v/executable/decoding-executable.lisp
A books/misc/character-encoding-test.acl2
M books/misc/character-encoding-test.lisp
M books/projects/aleo/leo/early-version/definition/expressions.lisp
M books/projects/aleo/leo/early-version/definition/lexer.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/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Merge branch 'testing-kestrel'

Commit: 3d6d434ee51e3d45ad7bdc463f5a3dcefd0c1f23
https://github.com/acl2/acl2/commit/3d6d434ee51e3d45ad7bdc463f5a3dcefd0c1f23
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:
M bin/purity-acl2.sh

Log Message:
-----------
Update purity script date

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

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
Merge pull request #1915 from gjurgensen/gj-doc

Improve `best-practices` and remove wiki page

Commit: 67d942d600c58ef0a450d1f6cca0db33a0b34d71
https://github.com/acl2/acl2/commit/67d942d600c58ef0a450d1f6cca0db33a0b34d71
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:
M books/doc/relnotes.lisp

Log Message:
-----------
[doc] Replace tab with spaces

Commit: f22acf09298696e8100913fd29135d29b483edb3
https://github.com/acl2/acl2/commit/f22acf09298696e8100913fd29135d29b483edb3
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:
M books/doc/relnotes.lisp

Log Message:
-----------
[doc] Add character-encoding topic changes to relnotes

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: 25d10c770ec80248e371bde248e65ce39f5e9d29
https://github.com/acl2/acl2/commit/25d10c770ec80248e371bde248e65ce39f5e9d29
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:
M books/doc/relnotes.lisp

Log Message:
-----------
[doc] Fix XDOC typo

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: 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.

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

Changed paths:
M books/kestrel/bitcoin/bech32.lisp

Log Message:
-----------
[bech32] Fix xdoc issue.

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: b70da5edd24a06912166c1baa61858c153388ab5
https://github.com/acl2/acl2/commit/b70da5edd24a06912166c1baa61858c153388ab5
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:
M books/std/system/remove-dead-if-branches.lisp

Log Message:
-----------
[Std/system] Fix typo in xdoc.

Commit: 1addd09ff2c9f55919c3d8111d5ab06b35c6151b
https://github.com/acl2/acl2/commit/1addd09ff2c9f55919c3d8111d5ab06b35c6151b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:
M books/kestrel/x86/assumptions-new.lisp

Log Message:
-----------
[x86] Fix comment typo.

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
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.

Commit: 7be1ef07f91b9aa518882973e6fe3619d8472f86
https://github.com/acl2/acl2/commit/7be1ef07f91b9aa518882973e6fe3619d8472f86

Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>

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

Changed paths:
M books/xdoc/save-rendered.lisp

Log Message:
-----------
Update books/xdoc/save-rendered.lisp

Accept suggestion by Eric M.

Co-authored-by: Eric McCarthy <7607035+...@users.noreply.github.com>

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

Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>

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

Changed paths:
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 pull request #1917 from acl2/xdoc-missing-parents-error

Allow missing parents to cause an error.

Commit: 10d564d8e5edd4510dc2cea10000dc3c5825ff21
https://github.com/acl2/acl2/commit/10d564d8e5edd4510dc2cea10000dc3c5825ff21
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-16 (Mon, 16 Mar 2026)

Changed paths:
M books/doc/relnotes.lisp

Log Message:
-----------
[xdoc] Small edits to release notes.

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

Changed paths:
M books/doc/relnotes.lisp

Log Message:
-----------
[xdoc] Move 2 release note items.

These seem to belong under Documentation.

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

Changed paths:
M books/doc/relnotes.lisp

Log Message:
-----------
[xdoc] Fix broken link.

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

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

Log Message:
-----------
[doc] Apply suggestion from Grant Jurgensen.

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