[acl2/acl2] 7baf78: [C$] Refine ensemble annotation

[Grant Jurgensen]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 7baf788b17e37812c9f287e2420e8c1c6dd9f0b7
https://github.com/acl2/acl2/commit/7baf788b17e37812c9f287e2420e8c1c6dd9f0b7
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-07 (Thu, 07 May 2026)

Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp

Log Message:
-----------
[C$] Refine ensemble annotation

Previously, we added the entire validation table to the annotation. Now,
we just add the particular fields which are persistent and accumulated
across translation units.


Commit: fd292f3c3dc18ede25255c3bc0a15f5e859cc58d
https://github.com/acl2/acl2/commit/fd292f3c3dc18ede25255c3bc0a15f5e859cc58d
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-07 (Thu, 07 May 2026)

Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Move fields from valid-table to vstate.

This move the fields which are not specific to the current translation
unit into the vstate.


Commit: 536a9dd32eb7858a81f9981556f05a8edabcabc8
https://github.com/acl2/acl2/commit/536a9dd32eb7858a81f9981556f05a8edabcabc8
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-07 (Thu, 07 May 2026)

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

Log Message:
-----------
[C$] Update stale doc in valid-trans-ensemble.

Update the documentation to reflect that cross-translation-unit
information is now accumulated and stored in the ensemble annotation.

Co-Authored-By: Claude Sonnet 4.6 <nor...@anthropic.com>


Commit: 2312c261eec86d0e2849f04e0dcb4863c89f0356
https://github.com/acl2/acl2/commit/2312c261eec86d0e2849f04e0dcb4863c89f0356
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-07 (Thu, 07 May 2026)

Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Move macro table from vstate to valid-table.

The macro table is specific to a single translation unit, so it belongs
in the validation table rather than the validator state.

Co-Authored-By: Claude Sonnet 4.6 <nor...@anthropic.com>


Commit: 12210e44988cde79ed114ff44e505eca58fbfcd1
https://github.com/acl2/acl2/commit/12210e44988cde79ed114ff44e505eca58fbfcd1
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-07 (Thu, 07 May 2026)

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

Log Message:
-----------
[C$] Fix XDOC errors.


Compare: https://github.com/acl2/acl2/compare/dcc78ee08319...12210e44988c

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

[Grant Jurgensen]

Branch: refs/heads/master

[Grant Jurgensen]

Branch: refs/heads/testing