[acl2/acl2] f9338d: [C$] Improve handling of `#include`s.

0 views
Skip to first unread message

Alessandro Coglio

unread,
Jan 9, 2026, 12:23:26 AM (12 days ago) Jan 9
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
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: 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: 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: 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: 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.


Compare: https://github.com/acl2/acl2/compare/dd62b342b8ac...4bbef68be50d

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

Alessandro Coglio

unread,
Jan 9, 2026, 1:32:50 AM (12 days ago) Jan 9
to acl2-...@googlegroups.com
Branch: refs/heads/master
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.


Compare: https://github.com/acl2/acl2/compare/d0bab5155095...4bbef68be50d

Alessandro Coglio

unread,
Jan 9, 2026, 1:33:32 AM (12 days ago) Jan 9
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Jan 9, 2026, 2:05:10 AM (12 days ago) Jan 9
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Reply all
Reply to author
Forward
0 new messages