[acl2/acl2] 85c81d: [C$] Improve handling of self-contained files.

[Alessandro Coglio]

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

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

Log Message:
-----------
[C$] Improve handling of self-contained files.

Also store the header guard (if any) in the data structure for self-contained
files.


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

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

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

If we are including an already preprocessed self-contained file with a header
guard that is currently defined, it is safe to preserve the `#include`, without
the need to re-preprocess the included file.

Adjust test expectation and remove TODO, since now the test works the way we
want it to.


Commit: 56c23bc16dc9b6bce2fa15ba27281823d46f49dc
https://github.com/acl2/acl2/commit/56c23bc16dc9b6bce2fa15ba27281823d46f49dc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-08 (Sun, 08 Feb 2026)

Changed paths:
R books/kestrel/c/syntax/tests/gincluder.c
A books/kestrel/c/syntax/tests/gincluder1.c
A books/kestrel/c/syntax/tests/gincluder2.c
M books/kestrel/c/syntax/tests/preprocessor.lisp

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

This show that a more complex collection of files still preserves `#include`s.


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

Changed paths:
M books/kestrel/c/syntax/tests/gincluder1.h
M books/kestrel/c/syntax/tests/gincluder2.h
M books/kestrel/c/syntax/tests/guarded.h
M books/kestrel/c/syntax/tests/preprocessor.lisp

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


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

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

Log Message:
-----------
[C$] Factor some code.


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

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

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

Do not output the `#ifndef` and `#endif` when the file has header guards but is
expanded in place; only output the `#define` in this case, to preserve the
semantics. (This situation may be rare, but definitely possible.)


Commit: 5c77a0937d215fd8d096c2db49a36339cfbc5675
https://github.com/acl2/acl2/commit/5c77a0937d215fd8d096c2db49a36339cfbc5675
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-08 (Sun, 08 Feb 2026)

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

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

This shows some more elaborate handling of `#include`s with a header guard.


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

Changed paths:
M books/kestrel/c/atc/expression-generation.lisp
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/function-tables.lisp
M books/kestrel/c/atc/generation-contexts.lisp
M books/kestrel/c/atc/generation.lisp
M books/kestrel/c/atc/limits.lisp
M books/kestrel/c/atc/pretty-printing-options.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/term-checkers-atc.lisp
M books/kestrel/c/atc/theorem-generation.lisp
M books/kestrel/c/package.lsp

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


Compare: https://github.com/acl2/acl2/compare/fa371426dc7b...de23e2d6a421

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