[acl2/acl2] 9f87b3: [C$] Refactor some predicates for the formalized s...

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 9f87b3faf495d2708e3b429cd6f9904a1916d188
https://github.com/acl2/acl2/commit/9f87b3faf495d2708e3b429cd6f9904a1916d188
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-06 (Tue, 06 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C$] Refactor some predicates for the formalized subset.

Add and use explicit predicates for lists of initializer declarators (of various
kinds).

Adapt a proof in the proof-generating transformations.


Commit: b66cddc071fd1e5ac40c1011e0226e98bf31e52e
https://github.com/acl2/acl2/commit/b66cddc071fd1e5ac40c1011e0226e98bf31e52e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-06 (Tue, 06 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C2C] Improve some checks and add a theorem.


Commit: e66b6ec223f4370e553bf70197b074f465a033cc
https://github.com/acl2/acl2/commit/e66b6ec223f4370e553bf70197b074f465a033cc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-06 (Tue, 06 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C2C] Add a theorem.


Commit: d73ec9734c5c8457eecc78816ea5cb58d35b9dfd
https://github.com/acl2/acl2/commit/d73ec9734c5c8457eecc78816ea5cb58d35b9dfd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/builtin.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp

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


Commit: c3d813d50dd76a68c8720c11419a48a3bcb31dcc
https://github.com/acl2/acl2/commit/c3d813d50dd76a68c8720c11419a48a3bcb31dcc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C2C] Add a theorem.


Commit: 207c86fbdf04e4fea1f8bc06f919f4ef563ea2ea
https://github.com/acl2/acl2/commit/207c86fbdf04e4fea1f8bc06f919f4ef563ea2ea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

Changed paths:
M books/demos/attach-stobj/demo-book.acl2
M books/doc/relnotes.lisp
A books/kestrel/abstract-domains/intervals/acl2-customization.lsp
A books/kestrel/abstract-domains/intervals/arithmetic.lisp
A books/kestrel/abstract-domains/intervals/cert.acl2
A books/kestrel/abstract-domains/intervals/core.lisp
A books/kestrel/abstract-domains/intervals/exact.lisp
A books/kestrel/abstract-domains/intervals/inp.lisp
A books/kestrel/abstract-domains/intervals/min-max-support.lisp
A books/kestrel/abstract-domains/intervals/noninterval-arith-support.lisp
A books/kestrel/abstract-domains/intervals/package.lsp
A books/kestrel/abstract-domains/intervals/portcullis.acl2
A books/kestrel/abstract-domains/intervals/portcullis.lisp
A books/kestrel/abstract-domains/intervals/subintervalp.lisp
A books/kestrel/abstract-domains/intervals/top.lisp
A books/kestrel/abstract-domains/many-valued-logics/3vl.lisp
A books/kestrel/abstract-domains/many-valued-logics/top.lisp
A books/kestrel/abstract-domains/top.lisp
M books/kestrel/arm/README.md
R books/kestrel/arm/arm32.lisp
M books/kestrel/arm/decoder.lisp
A books/kestrel/arm/def-inst.lisp
A books/kestrel/arm/encodings.lisp
A books/kestrel/arm/instructions.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/state.lisp
A books/kestrel/arm/step.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp
A books/kestrel/utilities/arith-fix-and-equiv-defs.lisp
A books/kestrel/utilities/arith-fix-and-equiv.lisp
M books/kestrel/utilities/top.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M simplify.lisp

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


Commit: debf4d4c546dddc8a2f07cdc75e51f6a2d6dd04c
https://github.com/acl2/acl2/commit/debf4d4c546dddc8a2f07cdc75e51f6a2d6dd04c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C2C] Add a theorem.


Commit: 8e152d9bd350162cd75cb0f85039aefac8b309a6
https://github.com/acl2/acl2/commit/8e152d9bd350162cd75cb0f85039aefac8b309a6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp

Log Message:
-----------
[C$] Revise the resizing of a preprocessor stobj array.


Commit: 2f3b642ca855a5caac9ba5c337be9c756bc5d1e6
https://github.com/acl2/acl2/commit/2f3b642ca855a5caac9ba5c337be9c756bc5d1e6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

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

Log Message:
-----------
[C$] Improve some layout.


Commit: 459f768f10e3765406b09a081bc61ef433f4d704
https://github.com/acl2/acl2/commit/459f768f10e3765406b09a081bc61ef433f4d704
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp

Log Message:
-----------
[C$] Add operation on preprocessing states.

This adds bytes to the current input.


Commit: a74deec9363c245534f133688f4c4557d35f6ac9
https://github.com/acl2/acl2/commit/a74deec9363c245534f133688f4c4557d35f6ac9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C2C] Improve some checks and add a theorem.


Commit: da38e51d138f5b1cefb63d127ddfd39aee37d25b
https://github.com/acl2/acl2/commit/da38e51d138f5b1cefb63d127ddfd39aee37d25b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Handle `#include`s that expand in place.

We had to add a function to put any unread character back into the input bytes:
see documentation.


Commit: 71b2bd7a999908c31b0f2afb3302367d329e349f
https://github.com/acl2/acl2/commit/71b2bd7a999908c31b0f2afb3302367d329e349f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-reader.lisp

Log Message:
-----------
[C$] Expand some doc.


Commit: 64d79af1620a54a26ac3e84328e02266249d0209
https://github.com/acl2/acl2/commit/64d79af1620a54a26ac3e84328e02266249d0209
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/transformation/proof-generation.lisp

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


Commit: 6ed575ca1c360d69a152eb5e1b426579051991f9
https://github.com/acl2/acl2/commit/6ed575ca1c360d69a152eb5e1b426579051991f9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

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

Log Message:
-----------
[C$] Expand some doc.


Compare: https://github.com/acl2/acl2/compare/0067f34bddf5...6ed575ca1c36

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

[Alessandro Coglio]

Branch: refs/heads/master

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

[MattKaufmann]

Branch: refs/heads/testing-acl2s

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

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-07 (Wed, 07 Jan 2026)

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

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

[C$] Improve handling of `#include`s.

When the included file is self-contained, preserve all the white space and
comments of the directive itself.


Commit: bea3e3de6509a5611d05119dd72578ed23eda22e
https://github.com/acl2/acl2/commit/bea3e3de6509a5611d05119dd72578ed23eda22e
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:

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

M other-events.lisp

Log Message:
-----------
Fixed type declaration bug showing up at safety 3 with SBCL in books/misc/hidden-defpkg-checks/.

We fixed a low-level bug in [include-book], which we have only
observed using ACL2 built on host Lisp SBCL with safety 3 (an
optimization setting that causes more runtime checks at the cost of
longer run times). (Technical note: The bug was in bogus type
declarations in the definition of ACL2 source macro
with-hcomp-bindings.) Thanks to Jim White for reporting the bug.

This fix seems to permit Issue #1889 to be closed.


Commit: 66830d3524f48d387eb87def75f9f751742fd85f
https://github.com/acl2/acl2/commit/66830d3524f48d387eb87def75f9f751742fd85f
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/projects/hol-in-acl2/acl2/hol.lisp
A books/projects/hol-in-acl2/acl2/type-match.lisp
M books/projects/hol-in-acl2/examples/eval-poly-acl2.lisp

Log Message:
-----------
Tweaks to hol-in-acl2


Commit: ccc44d49459510dbc2212e29168eadcc6cd6a671
https://github.com/acl2/acl2/commit/ccc44d49459510dbc2212e29168eadcc6cd6a671
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/projects/set-theory/logic.txt

Log Message:
-----------
Tweaked note on logical foundations of ACL2(zfc) to make it slightly more accessible


Commit: 64a722a31581d5336ef7ed46615d8ab6926a5df9
https://github.com/acl2/acl2/commit/64a722a31581d5336ef7ed46615d8ab6926a5df9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/projects/hol-in-acl2/acl2/hol.lisp
A books/projects/hol-in-acl2/acl2/type-match.lisp
M books/projects/hol-in-acl2/examples/eval-poly-acl2.lisp
M books/projects/set-theory/logic.txt

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

M other-events.lisp

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


Commit: 80dd0901b42fa76f5f1b64c4a8e7ab3a8cad4168
https://github.com/acl2/acl2/commit/80dd0901b42fa76f5f1b64c4a8e7ab3a8cad4168
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp

Log Message:
-----------
[C$] Remove outdated doc..


Commit: 4839122ead0a91179128d94a188d3346907b6bbd
https://github.com/acl2/acl2/commit/4839122ead0a91179128d94a188d3346907b6bbd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp

Log Message:
-----------
[C$] Tweak book inclusion order.

Rationale: first include books from current or sibling library via relative
paths, then from other libraries via `:dir :system` paths, then local
inclusions, finally set the controlled configuraion.


Commit: bd385e04fd9328a18d4883e597767cd014a7f212
https://github.com/acl2/acl2/commit/bd385e04fd9328a18d4883e597767cd014a7f212
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp

Log Message:
-----------
[C$] Improve handling of the null directive.

Preserve all white space and comments in it, and wrap the hash into a small
block comment inline. Perhaps the preprocessor should support options for the
exact treatment of this and other situations.


Commit: d59e7483c8fda0b868e524c9f6c1d94a6eb3a81d
https://github.com/acl2/acl2/commit/d59e7483c8fda0b868e524c9f6c1d94a6eb3a81d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

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

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

[C$] Improve handling of unexpanded `#include`s.

Forgot to preserve the final line comment, if any.


Commit: 01bf67de11b5a06d008049fa9e815e8cfe64bf47
https://github.com/acl2/acl2/commit/01bf67de11b5a06d008049fa9e815e8cfe64bf47
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/tests/including.c
M books/kestrel/c/syntax/tests/preprocessor.lisp

Log Message:
-----------
[C$] Add some preprocessor tests.

Test the preservation of white space and comments in unexpanded `#include`
directives.


Commit: d9dee1a1b36befa0d5a1e18eb7f8f45675424302
https://github.com/acl2/acl2/commit/d9dee1a1b36befa0d5a1e18eb7f8f45675424302
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
A books/std/omaps/from-alist.lisp
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp

Log Message:
-----------
[OMAP] Add from-alist and from-lists


Commit: a2683ab3150b87df607d5d874d1a1e8a01ea7854
https://github.com/acl2/acl2/commit/a2683ab3150b87df607d5d874d1a1e8a01ea7854
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
A books/std/omaps/from-alist.lisp
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp

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


Commit: 4a97222418b3043b09e492a70568f601c37015ad
https://github.com/acl2/acl2/commit/4a97222418b3043b09e492a70568f601c37015ad
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/build/jenkins/Makefile
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh

Log Message:
-----------
[build] Add MAKEACL2OPTS option to Jenkins scripts.

Unlike MAKEOPTS, which only applies to books, MAKEACL2OPTS applies to building ACL2 itself.


Commit: f4be7f84b31222b67c4dddd52dcbecf8de5497c8
https://github.com/acl2/acl2/commit/f4be7f84b31222b67c4dddd52dcbecf8de5497c8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/build/jenkins/Makefile

Log Message:
-----------
[build] Try to fix syntax.


Commit: 4de378350400f7c7487feaf747168458f3846771
https://github.com/acl2/acl2/commit/4de378350400f7c7487feaf747168458f3846771
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/build/jenkins/Makefile

Log Message:
-----------
[build] Fix tabs in Jenkins Makefile.


Commit: 7d791aa11c28256665c140249f9d70417e01c212
https://github.com/acl2/acl2/commit/7d791aa11c28256665c140249f9d70417e01c212
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/build/jenkins/Makefile

Log Message:
-----------
[build] Fix printing in Jenkins Makefile.


Commit: d1dd38b6f3503d5045faa127f192086fa327b241
https://github.com/acl2/acl2/commit/d1dd38b6f3503d5045faa127f192086fa327b241
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
A books/std/omaps/from-alist.lisp
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp

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


Commit: dd62b342b8ac6c3f85c3fe4fd56236e3fa694dce
https://github.com/acl2/acl2/commit/dd62b342b8ac6c3f85c3fe4fd56236e3fa694dce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/parser.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/simpadd0.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Add support for GCC statement attributes.


Commit: 6cbfd2a333e97938c5d04792cbf06bcfed08d447
https://github.com/acl2/acl2/commit/6cbfd2a333e97938c5d04792cbf06bcfed08d447
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/text.c

Log Message:
-----------
[C$] Extend preprocessor.

Add initial handling of text lines.

Add a test for that.


Commit: 761ed1a5c96dc6be103beedb499d282be5f9d9bf
https://github.com/acl2/acl2/commit/761ed1a5c96dc6be103beedb499d282be5f9d9bf
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/doc/publications.lisp

Log Message:
-----------
Updated URL for book by Russinoff, as he requested


Commit: db1d5d66264ad0cab20610f1c9cfb55d8099cf99
https://github.com/acl2/acl2/commit/db1d5d66264ad0cab20610f1c9cfb55d8099cf99
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh

Log Message:
-----------
[build] Add some documentation.

This was suggested by a comment in Matt Kaufmann's review of the PR.


Commit: 89078791d2e9aad30f76fb85b7244a303c36b5f2
https://github.com/acl2/acl2/commit/89078791d2e9aad30f76fb85b7244a303c36b5f2
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/build/jenkins/Makefile
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh

Log Message:
-----------
Merge pull request #1892 from acl2/jenkins-makeacl2opts

Add option in Jenkins scripts to pass make options for ACL2 itself


Commit: b4df8fad9fe1baa75bc692334b13517c9e4b9558
https://github.com/acl2/acl2/commit/b4df8fad9fe1baa75bc692334b13517c9e4b9558
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/projects/dpss/Base/events.lisp

Log Message:
-----------
Fixed typo.

This typo was found in an SBCL-based safety-3 run. Thanks to Eric
Smith for setting up leeroy to run tests with safety 3. The typo
was "delare" instead of "declare" here:

(def::und smallest-impending-dt-index (ens)
(delare (xargs :fty ((uav-list) uav-id)))
...)

Apparently the def::und macro could be improved by doing more checking.


Commit: d0bab51550952c3048df522936c05a2a5fb67b38
https://github.com/acl2/acl2/commit/d0bab51550952c3048df522936c05a2a5fb67b38
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/parser.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/simpadd0.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

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


Commit: 4cb4286e7a80b3ce17a53d7af1265a1aab447c40
https://github.com/acl2/acl2/commit/4cb4286e7a80b3ce17a53d7af1265a1aab447c40
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

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

Log Message:
-----------
[C$] Add some doc comments.


Commit: 9ad4ad3e610225d6bff8401520e955c5da4288c1
https://github.com/acl2/acl2/commit/9ad4ad3e610225d6bff8401520e955c5da4288c1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp

M books/kestrel/c/syntax/preprocessor-states.lisp

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

[C$] Improve preprocessor lexer.

Have it handle read and unread lexemes in the preprocessor state.


Commit: 31b67ed805bc3f0150a364fc333403c30e2c8932
https://github.com/acl2/acl2/commit/31b67ed805bc3f0150a364fc333403c30e2c8932
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

Changed paths:
M books/build/jenkins/Makefile
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh
M books/doc/publications.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/parser.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/simpadd0.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/projects/dpss/Base/events.lisp
A books/std/omaps/from-alist.lisp
A books/std/omaps/from-lists.lisp
M books/std/omaps/top.lisp

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


Commit: 3fe93932303e65a239112a7b06af3f35fc5095da
https://github.com/acl2/acl2/commit/3fe93932303e65a239112a7b06af3f35fc5095da
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

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

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

[C$] Simplify some preprocessor code.


Commit: f3d79c3d48c418bfd65b532ba316588e2bc08fca
https://github.com/acl2/acl2/commit/f3d79c3d48c418bfd65b532ba316588e2bc08fca
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

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

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

[C$] Improve a function name.


Commit: 4bbef68be50da1f72319eea09d7f06f74a778ef6
https://github.com/acl2/acl2/commit/4bbef68be50da1f72319eea09d7f06f74a778ef6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)

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

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

[C$] Simplify some preprocessor code.

Handle empty and non-empty text lines uniformly.


Commit: af47c9e42b336fb0ef3cf6eb158344e40aa1df22
https://github.com/acl2/acl2/commit/af47c9e42b336fb0ef3cf6eb158344e40aa1df22
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-09 (Fri, 09 Jan 2026)

Changed paths:
M acl2-init.lisp

Log Message:
-----------
Disable xref recording in SBCL.

This didn't noticeably affect "make regression-everything" time (using -j 20 on Linux):

;;; Previous (Jan. 7):
97642.058u 6791.411s 1:52:23.62 1548.6% 0+0k 4056816+11973888io 30pf+0w

;;; New:
97399.966u 6992.549s 1:51:44.33 1557.0% 0+0k 3353848+12250952io 31pf+0w

I added the following comment in acl2-init.lisp to explain the change,
which was contributed by Jim White (thanks!).

; The following was contributed by Jim White, who used Copilot on 1/8/2026 to
; suggest the following addition to prevent raw Lisp errors when certifying the
; following with SBCL 2.9.11 on ARM64 (Ubuntu 24.04.3 LTS running in Docker
; container): demos/congruent-stobjs-book, demos/brr-test-book,
; demos/refinement-failure-test-book, demos/brr-free-variables-book, and
; workshops/2023/kaufmann-moore/brr-book. If SBCL bug #2137765 is fixed
; (https://bugs.launchpad.net/sbcl/+bug/2137765), then we might remove this
; change sometime later.


Compare: https://github.com/acl2/acl2/compare/0067f34bddf5...af47c9e42b33