[acl2/acl2] 8c0b24: [C$] Relax check in disambiguator.

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 8c0b24c432d342b67c16740128ef955c5fee1a82
https://github.com/acl2/acl2/commit/8c0b24c432d342b67c16740128ef955c5fee1a82
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-13 (Mon, 13 Apr 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
A books/kestrel/c/syntax/translation-unit-comparison.lisp

Log Message:
-----------
[C$] Relax check in disambiguator.

This is for deciding whether a `#include` can be preserved or not by the
disambigautor. We disambiguate the included translation unit both in the context
of the including translation unit and in a fresh context, and we preserve the
`#include` if we obtain the same result, where 'same result' means that the two
translation units compare equal taking the macros, and the preprocessing
conditions, into account, similarly to the preprocessor.

The code for this comparison of translation units is more general than the
disambiguator, and in fact it is in its own file and topic. It will be also used
by the validator, and possibly by transformations, when we extend them to
preserve `#include` directives when possible.


Commit: d4f4e2ffe3c544ec2df7623e4bfb3008c94eca40
https://github.com/acl2/acl2/commit/d4f4e2ffe3c544ec2df7623e4bfb3008c94eca40
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-13 (Mon, 13 Apr 2026)

Changed paths:
M books/kestrel/c/syntax/concrete-syntax.lisp
M books/kestrel/c/syntax/top.lisp

Log Message:
-----------
[C$] Put Unicode characters under concrete syntax.

This is mainly XDOC organization.


Commit: 162a0fc2aa9b377efaf76dd8424f15e990509f85
https://github.com/acl2/acl2/commit/162a0fc2aa9b377efaf76dd8424f15e990509f85
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-13 (Mon, 13 Apr 2026)

Changed paths:
M books/kestrel/c/syntax/tests/disambiguator-trans-ensembles.lisp

Log Message:
-----------
[C$] Rename some names in a test.


Commit: 72b25521056c28e3e0ebd2e008edc348d59cba0b
https://github.com/acl2/acl2/commit/72b25521056c28e3e0ebd2e008edc348d59cba0b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-13 (Mon, 13 Apr 2026)

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

Log Message:
-----------
[C$] Fix bug in disambiguator.

When we recursively disambiguate an included file, we need to change, in the
disambiguator state, the current file, so we can properly resolve `#include`s;
and then we need to restore that to the including file.


Commit: b9d2cca2c9a9b84472d5f5d860083691e7384a7f
https://github.com/acl2/acl2/commit/b9d2cca2c9a9b84472d5f5d860083691e7384a7f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-13 (Mon, 13 Apr 2026)

Changed paths:
M books/kestrel/c/syntax/tests/disambiguator-trans-ensembles.lisp

Log Message:
-----------
[C$] Add a disambiguator test.

This shows the preservation of `#include`s with header guards.


Commit: ac76a414278e7f28018022dedef9b1af3d1170f6
https://github.com/acl2/acl2/commit/ac76a414278e7f28018022dedef9b1af3d1170f6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-13 (Mon, 13 Apr 2026)

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

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


Commit: b1560a836611e06c450a6ffb5f71d418da654255
https://github.com/acl2/acl2/commit/b1560a836611e06c450a6ffb5f71d418da654255
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-13 (Mon, 13 Apr 2026)

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

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


Compare: https://github.com/acl2/acl2/compare/7bb80013b8d3...b1560a836611

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

[Alessandro Coglio]

Branch: refs/heads/master

Commit: 9c99457b5f7f34553bc1efcc4ab71144b7feedda
https://github.com/acl2/acl2/commit/9c99457b5f7f34553bc1efcc4ab71144b7feedda

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-13 (Mon, 13 Apr 2026)

Changed paths:

A books/kestrel/c/syntax/tests/disamb-example2/guarded-included.h
A books/kestrel/c/syntax/tests/disamb-example2/including.c
A books/kestrel/c/syntax/tests/disamb-example2/including1.c
A books/kestrel/c/syntax/tests/disamb-example2/including2.c

Log Message:
-----------
[C$] Add forgotten test files.


Compare: https://github.com/acl2/acl2/compare/7bb80013b8d3...9c99457b5f7f

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel