[acl2/acl2] 11348e: [C$] Add two structural operations on ASTs.
0 views
Skip to first unread message
Alessandro Coglio
Feb 9, 2026, 11:46:01 PM (19 hours ago) Feb 9
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 11348e465412b6b9d5b4c0f29f5f9ce620e55189
https://github.com/acl2/acl2/commit/11348e465412b6b9d5b4c0f29f5f9ce620e55189
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Add two structural operations on ASTs.
Commit: 25ee8372c2922bd074c4ce24bfbd37fbef5d5d9c
https://github.com/acl2/acl2/commit/25ee8372c2922bd074c4ce24bfbd37fbef5d5d9c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Improve preprocessor.
Generate line comments to indicate where `#include` directives have expanded
files in place.
Commit: 49ebb9817707193168bff5fb3075425b551caf9b
https://github.com/acl2/acl2/commit/49ebb9817707193168bff5fb3075425b551caf9b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/gincluder1.c
M books/kestrel/c/syntax/tests/gincluder1.h
M books/kestrel/c/syntax/tests/gincluder2.c
M books/kestrel/c/syntax/tests/gincluder2.h
M books/kestrel/c/syntax/tests/gincludermod1.c
M books/kestrel/c/syntax/tests/gincludermod2.c
M books/kestrel/c/syntax/tests/guarded.h
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Tweak some tests for readability.
Commit: 42bb05e47e5dfbef84d085ae9eaac0c388ed2750
https://github.com/acl2/acl2/commit/42bb05e47e5dfbef84d085ae9eaac0c388ed2750
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/utilities/defmacrodoc.lisp
Log Message:
-----------
[utilities] Improve defmacrodoc.
Fix handling of default arguments that are not atoms.
Commit: b3d5be3561d045fb3e603d6aa11dbd31ade21ec8
https://github.com/acl2/acl2/commit/b3d5be3561d045fb3e603d6aa11dbd31ade21ec8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/projects/pfcs/abstract-syntax-trees.lisp
Log Message:
-----------
Merge.
Commit: 309cb47d323db4a69e0f6039c6fa8ba4a7d510da
https://github.com/acl2/acl2/commit/309cb47d323db4a69e0f6039c6fa8ba4a7d510da
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.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/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/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.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/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Add a form of `#include` directives to ASTs.
For now, we just allow them at the beginning of a file, after the optional
comment line (see fixtype for translation units).
This commit modifies tools that operate on AST (e.g. validator, and most
transformations) to return or throw an error if `#include` directives are
encountered, since we need to design and implement an appropriate treatment.
The printer has already been extended to handle the directives.
The `simpadd0` transformation accepts these directives because the
transformation that it operates is entirely local.
Commit: df283a417786ed2ce6abf27c78b24ea8ee1bd425
https://github.com/acl2/acl2/commit/df283a417786ed2ce6abf27c78b24ea8ee1bd425
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/top.lisp
Log Message:
-----------
[C$] Update and improve some doc.
Commit: fa88ea652b56e5017f458fdf19dcf87186ddbc51
https://github.com/acl2/acl2/commit/fa88ea652b56e5017f458fdf19dcf87186ddbc51
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser-messages.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
Log Message:
-----------
[C$] Improve some names.
Commit: 5f15fdb577368a0ecaf9c2a75ffa2547bd6c49ce
https://github.com/acl2/acl2/commit/5f15fdb577368a0ecaf9c2a75ffa2547bd6c49ce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/parser-messages.lisp
M books/kestrel/c/syntax/parser-states.lisp
Log Message:
-----------
[C$] Extend tokens with header names.
This is part of handling both preprocessing and non-preprocessing constructs in
our syntax and tools.
Commit: 0247aaba4d8f7b07894602bd90bb54a3e0e7f3bf
https://github.com/acl2/acl2/commit/0247aaba4d8f7b07894602bd90bb54a3e0e7f3bf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
A books/kestrel/c/transformation/command-line/tests/add-section-attr-mac.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2-mac.json
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
Log Message:
-----------
[C2C] Adapt command-line tests to work on the Mac.
On the Mac, the add-section-attr transformation needs to be given section names appropriate for Mach-O executables. Thanks to Alessandro Coglio for reporting this issue.
Commit: 9db02a9ed995dd0ebda44fe51126eca96a5691a2
https://github.com/acl2/acl2/commit/9db02a9ed995dd0ebda44fe51126eca96a5691a2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/lexer.lisp
Log Message:
-----------
[C$] Improve some names.
Commit: 3cf76d25ddff1fc6bd2a3d47fa01bb79b3e13a6c
https://github.com/acl2/acl2/commit/3cf76d25ddff1fc6bd2a3d47fa01bb79b3e13a6c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
A books/kestrel/c/transformation/command-line/tests/add-section-attr-mac.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2-mac.json
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
M books/kestrel/utilities/defmacrodoc.lisp
Log Message:
-----------
Merge.
Commit: 6e6f943b148fc267eedfd29d6126e93525266462
https://github.com/acl2/acl2/commit/6e6f943b148fc267eedfd29d6126e93525266462
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/lexer.lisp
Log Message:
-----------
[C$] Improve a name and add some doc.
Compare: https://github.com/acl2/acl2/compare/c7cd4cc72819...6e6f943b148f
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 11348e465412b6b9d5b4c0f29f5f9ce620e55189
https://github.com/acl2/acl2/commit/11348e465412b6b9d5b4c0f29f5f9ce620e55189
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Add two structural operations on ASTs.
Commit: 25ee8372c2922bd074c4ce24bfbd37fbef5d5d9c
https://github.com/acl2/acl2/commit/25ee8372c2922bd074c4ce24bfbd37fbef5d5d9c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Improve preprocessor.
Generate line comments to indicate where `#include` directives have expanded
files in place.
Commit: 49ebb9817707193168bff5fb3075425b551caf9b
https://github.com/acl2/acl2/commit/49ebb9817707193168bff5fb3075425b551caf9b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/gincluder1.c
M books/kestrel/c/syntax/tests/gincluder1.h
M books/kestrel/c/syntax/tests/gincluder2.c
M books/kestrel/c/syntax/tests/gincluder2.h
M books/kestrel/c/syntax/tests/gincludermod1.c
M books/kestrel/c/syntax/tests/gincludermod2.c
M books/kestrel/c/syntax/tests/guarded.h
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Tweak some tests for readability.
Commit: 42bb05e47e5dfbef84d085ae9eaac0c388ed2750
https://github.com/acl2/acl2/commit/42bb05e47e5dfbef84d085ae9eaac0c388ed2750
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/utilities/defmacrodoc.lisp
Log Message:
-----------
[utilities] Improve defmacrodoc.
Fix handling of default arguments that are not atoms.
Commit: b3d5be3561d045fb3e603d6aa11dbd31ade21ec8
https://github.com/acl2/acl2/commit/b3d5be3561d045fb3e603d6aa11dbd31ade21ec8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/projects/pfcs/abstract-syntax-trees.lisp
Log Message:
-----------
Merge.
Commit: 309cb47d323db4a69e0f6039c6fa8ba4a7d510da
https://github.com/acl2/acl2/commit/309cb47d323db4a69e0f6039c6fa8ba4a7d510da
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.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/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/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.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/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Add a form of `#include` directives to ASTs.
For now, we just allow them at the beginning of a file, after the optional
comment line (see fixtype for translation units).
This commit modifies tools that operate on AST (e.g. validator, and most
transformations) to return or throw an error if `#include` directives are
encountered, since we need to design and implement an appropriate treatment.
The printer has already been extended to handle the directives.
The `simpadd0` transformation accepts these directives because the
transformation that it operates is entirely local.
Commit: df283a417786ed2ce6abf27c78b24ea8ee1bd425
https://github.com/acl2/acl2/commit/df283a417786ed2ce6abf27c78b24ea8ee1bd425
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/top.lisp
Log Message:
-----------
[C$] Update and improve some doc.
Commit: fa88ea652b56e5017f458fdf19dcf87186ddbc51
https://github.com/acl2/acl2/commit/fa88ea652b56e5017f458fdf19dcf87186ddbc51
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser-messages.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
Log Message:
-----------
[C$] Improve some names.
Commit: 5f15fdb577368a0ecaf9c2a75ffa2547bd6c49ce
https://github.com/acl2/acl2/commit/5f15fdb577368a0ecaf9c2a75ffa2547bd6c49ce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/parser-messages.lisp
M books/kestrel/c/syntax/parser-states.lisp
Log Message:
-----------
[C$] Extend tokens with header names.
This is part of handling both preprocessing and non-preprocessing constructs in
our syntax and tools.
Commit: 0247aaba4d8f7b07894602bd90bb54a3e0e7f3bf
https://github.com/acl2/acl2/commit/0247aaba4d8f7b07894602bd90bb54a3e0e7f3bf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
A books/kestrel/c/transformation/command-line/tests/add-section-attr-mac.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2-mac.json
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
Log Message:
-----------
[C2C] Adapt command-line tests to work on the Mac.
On the Mac, the add-section-attr transformation needs to be given section names appropriate for Mach-O executables. Thanks to Alessandro Coglio for reporting this issue.
Commit: 9db02a9ed995dd0ebda44fe51126eca96a5691a2
https://github.com/acl2/acl2/commit/9db02a9ed995dd0ebda44fe51126eca96a5691a2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/lexer.lisp
Log Message:
-----------
[C$] Improve some names.
Commit: 3cf76d25ddff1fc6bd2a3d47fa01bb79b3e13a6c
https://github.com/acl2/acl2/commit/3cf76d25ddff1fc6bd2a3d47fa01bb79b3e13a6c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
A books/kestrel/c/transformation/command-line/tests/add-section-attr-mac.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2-mac.json
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
M books/kestrel/utilities/defmacrodoc.lisp
Log Message:
-----------
Merge.
Commit: 6e6f943b148fc267eedfd29d6126e93525266462
https://github.com/acl2/acl2/commit/6e6f943b148fc267eedfd29d6126e93525266462
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-09 (Mon, 09 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/lexer.lisp
Log Message:
-----------
[C$] Improve a name and add some doc.
Compare: https://github.com/acl2/acl2/compare/c7cd4cc72819...6e6f943b148f
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
acl2buildserver
3:41 AM (15 hours ago) 3:41 AM
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: beb4ea17dfe064d024193855cfd55fd1b1afd86f
https://github.com/acl2/acl2/commit/beb4ea17dfe064d024193855cfd55fd1b1afd86f
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-10 (Tue, 10 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.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/langdef-mapping.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
Compare: https://github.com/acl2/acl2/compare/1054c590f67a...beb4ea17dfe0
https://github.com/acl2/acl2/commit/beb4ea17dfe064d024193855cfd55fd1b1afd86f
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-10 (Tue, 10 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.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/langdef-mapping.lisp
M books/kestrel/c/syntax/lexer.lisp
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/preprocessor.lisp
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/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/gincluder1.c
M books/kestrel/c/syntax/tests/gincluder1.h
M books/kestrel/c/syntax/tests/gincluder2.c
M books/kestrel/c/syntax/tests/gincluder2.h
M books/kestrel/c/syntax/tests/gincludermod1.c
M books/kestrel/c/syntax/tests/gincludermod2.c
M books/kestrel/c/syntax/tests/guarded.h
M books/kestrel/c/syntax/tests/preprocessor.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/tests/gincluder1.h
M books/kestrel/c/syntax/tests/gincluder2.c
M books/kestrel/c/syntax/tests/gincluder2.h
M books/kestrel/c/syntax/tests/gincludermod1.c
M books/kestrel/c/syntax/tests/gincludermod2.c
M books/kestrel/c/syntax/tests/guarded.h
M books/kestrel/c/syntax/tests/preprocessor.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/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.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/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
Merge commit '6e6f943b148fc267eedfd29d6126e93525266462' into HEAD
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.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/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
Compare: https://github.com/acl2/acl2/compare/1054c590f67a...beb4ea17dfe0
acl2buildserver
3:42 AM (15 hours ago) 3:42 AM
to acl2-...@googlegroups.com
Branch: refs/heads/testing
acl2buildserver
12:14 PM (7 hours ago) 12:14 PM
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Reply all
Reply to author
Forward
0 new messages