[acl2/acl2] b868c6: [PFCS] Shorten some code.

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: b868c65aad684defd0a44d8a2bf4b2f520dc546c
https://github.com/acl2/acl2/commit/b868c65aad684defd0a44d8a2bf4b2f520dc546c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-27 (Fri, 27 Feb 2026)

Changed paths:
M books/projects/pfcs/well-formedness.lisp

Log Message:
-----------
[PFCS] Shorten some code.


Commit: 7133e1de4fe36747d24a6c92896b15fa85f87190
https://github.com/acl2/acl2/commit/7133e1de4fe36747d24a6c92896b15fa85f87190
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M books/kestrel/fty/defmake-self.lisp

Log Message:
-----------
[FTY] Fix XDOC parents in generate defmake-self forms


Commit: a0bb21d6cc2fd6a242f0415cf50ec9efe4a8468c
https://github.com/acl2/acl2/commit/a0bb21d6cc2fd6a242f0415cf50ec9efe4a8468c
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M books/kestrel/c/transformation/utilities/rename-fn.lisp

Log Message:
-----------
[C2C] Fix non-existent parent in rename-fn


Commit: a9e61486fc6fe7818c1f1246971cb3f0b83ef47c
https://github.com/acl2/acl2/commit/a9e61486fc6fe7818c1f1246971cb3f0b83ef47c
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/fty/defmake-self.lisp

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


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

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

Log Message:
-----------
Updated *acl2-broken-links-alist* in books/system/doc/acl2-doc.lisp.


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

Changed paths:
M README.md
M all-files.txt
M books/doc/more-topics.lisp
M books/doc/publications.acl2
M books/doc/relnotes.lisp
M books/kestrel/air/model-0/top.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/concrete-syntax.lisp
M books/kestrel/c/syntax/printing.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/crypto/primes/koala-bear.lisp
M books/kestrel/ethereum/rlp/top.lisp
M books/kestrel/fty/defmake-self.lisp
M books/kestrel/utilities/defstobj-plus-tests.lisp
M books/misc/check-acl2-exports.lisp
M books/projects/aleo/leo/early-version/definition/concrete-syntax.lisp
M books/projects/aleo/leo/early-version/definition/format-strings.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-and.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-all.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-true.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-if.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-nand.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-nor.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-not.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-or.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-xor.lisp
M books/projects/aleo/vm/circuits/pfcs/field-add.lisp
M books/projects/aleo/vm/circuits/pfcs/field-assert-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-assert-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-checked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-flagged.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-unchecked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-double.lisp
M books/projects/aleo/vm/circuits/pfcs/field-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-if.lisp
M books/projects/aleo/vm/circuits/pfcs/field-inv-checked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-inv-flagged.lisp
M books/projects/aleo/vm/circuits/pfcs/field-mul.lisp
M books/projects/aleo/vm/circuits/pfcs/field-neg.lisp
M books/projects/aleo/vm/circuits/pfcs/field-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-square.lisp
M books/projects/aleo/vm/circuits/pfcs/field-sub.lisp
M books/projects/aleo/vm/circuits/top.lisp
M books/projects/aleo/vm/language/grammar.lisp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
A books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
A books/projects/x86isa/machine/instructions/pmadd.lisp
A books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/system/apply/apply-prim.lisp
M books/system/doc/acl2-doc.lisp
M books/system/to-do.txt
M books/workshops/2025/kwan/rv-state.lisp
M defpkgs.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp

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


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

Changed paths:
M books/kestrel/ethereum/rlp/top.lisp

Log Message:
-----------
[Ethereum] Fix XDOC reference.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Rename an AST tag.

To avoid an unwanted side effect in XDOC.


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

Changed paths:
M books/doc/relnotes.lisp
M books/kestrel/air/model-0/top.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/concrete-syntax.lisp
M books/kestrel/c/syntax/printing.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/crypto/primes/koala-bear.lisp
M books/kestrel/ethereum/rlp/top.lisp
M books/kestrel/fty/defmake-self.lisp
M books/projects/aleo/leo/early-version/definition/concrete-syntax.lisp
M books/projects/aleo/leo/early-version/definition/format-strings.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-and.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-all.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-true.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-if.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-nand.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-nor.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-not.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-or.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-xor.lisp
M books/projects/aleo/vm/circuits/pfcs/field-add.lisp
M books/projects/aleo/vm/circuits/pfcs/field-assert-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-assert-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-checked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-flagged.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-unchecked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-double.lisp
M books/projects/aleo/vm/circuits/pfcs/field-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-if.lisp
M books/projects/aleo/vm/circuits/pfcs/field-inv-checked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-inv-flagged.lisp
M books/projects/aleo/vm/circuits/pfcs/field-mul.lisp
M books/projects/aleo/vm/circuits/pfcs/field-neg.lisp
M books/projects/aleo/vm/circuits/pfcs/field-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-square.lisp
M books/projects/aleo/vm/circuits/pfcs/field-sub.lisp
M books/projects/aleo/vm/circuits/top.lisp
M books/projects/aleo/vm/language/grammar.lisp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
A books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/top.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: 3caeffe6b910aebeb21395d3f3dd5b830ddb03db
https://github.com/acl2/acl2/commit/3caeffe6b910aebeb21395d3f3dd5b830ddb03db
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-03-01 (Sun, 01 Mar 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/move.lisp

Log Message:
-----------
[X86ISA] Add missing XDOC parent.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


Compare: https://github.com/acl2/acl2/compare/28c6f29436a6...95fed79a868b

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

[Alessandro Coglio]

Branch: refs/heads/master

Home: https://github.com/acl2/acl2
Commit: b868c65aad684defd0a44d8a2bf4b2f520dc546c
https://github.com/acl2/acl2/commit/b868c65aad684defd0a44d8a2bf4b2f520dc546c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-27 (Fri, 27 Feb 2026)

Changed paths:
M books/projects/pfcs/well-formedness.lisp

Log Message:
-----------
[PFCS] Shorten some code.

Compare: https://github.com/acl2/acl2/compare/c9b599761b0d...95fed79a868b

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

[MattKaufmann]

Branch: refs/heads/testing-acl2s

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

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

Changed paths:

M books/kestrel/risc-v/executable/execution-executable.lisp
M books/projects/python/embedding/types.lisp
M books/workshops/2025/manjrekar/examples/imul64/imul64-proof.lisp
M books/workshops/2025/manjrekar/examples/imul8/imul8-proof.lisp

Log Message:
-----------
Avoid errors from ACL2(p) run that used waterfall-parallelism.


Compare: https://github.com/acl2/acl2/compare/c9b599761b0d...83d184694c7e