[acl2/acl2] 4d8e88: [C$] Improve preprocessor implementation.

0 views
Skip to first unread message

Alessandro Coglio

unread,
Feb 8, 2026, 2:37:22 PM (2 days ago) Feb 8
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 4d8e886d5429c845772acb31343190d0dd8916b9
https://github.com/acl2/acl2/commit/4d8e886d5429c845772acb31343190d0dd8916b9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-06 (Fri, 06 Feb 2026)

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

Log Message:
-----------
[C$] Improve preprocessor implementation.

Make the maximum macro reach part of the stobj.


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

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

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


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

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

Log Message:
-----------
[C$] Add file dependencies to preprocessor tests.


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

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

Log Message:
-----------
[C$] Extend preprocessor to track header guard state.

This is used to recognize whether a file has the header guard form.

We still need to make use of this information.


Commit: 139a07a6b96f4631118c6aab917a2439d8e00703
https://github.com/acl2/acl2/commit/139a07a6b96f4631118c6aab917a2439d8e00703
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-07 (Sat, 07 Feb 2026)

Changed paths:
M books/acl2s/cgen/callback.lisp
M books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/u...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/validation-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/vali...@useless-runes.lsp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
A books/kestrel/c/syntax/tests/types.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/types.lisp
A books/kestrel/c/syntax/uid.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
M books/kestrel/c/transformation/tests/add-section-attr/test3.c
M books/kestrel/c/transformation/tests/split-all-gso/extern-struct.c
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-all-gso/static-struct1.c
M books/kestrel/c/transformation/tests/split-all-gso/static-struct2.c
M books/kestrel/c/transformation/tests/split-gso/extern-struct.c
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-alt.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval_poly.defhol
M books/projects/hol-in-acl2/examples/eval_polyScript.sml

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


Commit: d3690e62efa47d116a4d6321e8a7061c336fd5c0
https://github.com/acl2/acl2/commit/d3690e62efa47d116a4d6321e8a7061c336fd5c0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-07 (Sat, 07 Feb 2026)

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

Log Message:
-----------
[C$] Accumulate output lexemes in preprocessor states.

This simplifies some code, and also enabled an upcoming more elaborate
collection of output lexemes.


Commit: e8022dad27584f564acb631c309a71e5eb6702d7
https://github.com/acl2/acl2/commit/e8022dad27584f564acb631c309a71e5eb6702d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-07 (Sat, 07 Feb 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.lisp

Log Message:
-----------
[C$] Extend treatment of header guards.

Reorganize the collected output lexemes into chunks related to the header guard
structure. When the file has the header guard structure, also output the
directives in question.

Adjust some test expectations.


Compare: https://github.com/acl2/acl2/compare/837f6f84bd07...e8022dad2758

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

Alessandro Coglio

unread,
Feb 8, 2026, 2:37:39 PM (2 days ago) Feb 8
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Reply all
Reply to author
Forward
0 new messages