[acl2/acl2] 4f3050: [C$] Extend struct and union types
0 views
Skip to first unread message
Grant Jurgensen
Feb 6, 2026, 5:14:21 PM (4 days ago) Feb 6
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 4f305020e5e4a26fe729169550070dab53a01c30
https://github.com/acl2/acl2/commit/4f305020e5e4a26fe729169550070dab53a01c30
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.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
Log Message:
-----------
[C$] Extend struct and union types
Struct and union types now include their UID, translation unit name,
optional tag, and members if untagged. We also introduce a "completions"
map to associate tagged struct/union types to their members.
Validation was updated accordingly. Tests were added to the validator.
Commit: 27a169a8dad9e7592d836e66d21813ba4e0673e0
https://github.com/acl2/acl2/commit/27a169a8dad9e7592d836e66d21813ba4e0673e0
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
A books/kestrel/c/syntax/tests/types.lisp
Log Message:
-----------
[C$] Add type compatibility/composite tests
Commit: e3edd4d633bdde690277b0787d21a753ad6a57dc
https://github.com/acl2/acl2/commit/e3edd4d633bdde690277b0787d21a753ad6a57dc
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/validation-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/vali...@useless-runes.lsp
Log Message:
-----------
[C$] Update useless runes
Commit: 275baa82009a053f14f4e7256eced650e40ec05a
https://github.com/acl2/acl2/commit/275baa82009a053f14f4e7256eced650e40ec05a
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Add GCC extension to assignment typing
Allow function pointers to be used with void pointers in simple
assignment expresssion.
Commit: 2715c7988513fd532a4c7a0f7e1052295a4416dc
https://github.com/acl2/acl2/commit/2715c7988513fd532a4c7a0f7e1052295a4416dc
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/uid.lisp
Log Message:
-----------
[C$] Add XDOC parents to UID topics
Commit: c5a0e1eff8b1f72a82e210bee6bd6c9f030f07fd
https://github.com/acl2/acl2/commit/c5a0e1eff8b1f72a82e210bee6bd6c9f030f07fd
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/types.lisp
Log Message:
-----------
[C$] Add type helper functions
Commit: 6a1db295d54b7030c00d816a3bf1da8e51860abe
https://github.com/acl2/acl2/commit/6a1db295d54b7030c00d816a3bf1da8e51860abe
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/transformation/split-gso.lisp
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
Log Message:
-----------
[C2C] Update split-gso and tests
This adapts to the new C type fixtype. It also fixes some tests, which
were not actually valid C.
Commit: 1d9b193f9fd4bd40ced8846bf697718c4db5eb6e
https://github.com/acl2/acl2/commit/1d9b193f9fd4bd40ced8846bf697718c4db5eb6e
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
Log Message:
-----------
[C$] Fix xdoc typo
Commit: 70eec9b2de2b47c0ad69ec0392ae29534f5a520c
https://github.com/acl2/acl2/commit/70eec9b2de2b47c0ad69ec0392ae29534f5a520c
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/types.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Use a fast-alist for type completions map
This map can get quite large; using omaps became impractical.
Commit: 79217c11575900ef3019834a8779070fbd38b841
https://github.com/acl2/acl2/commit/79217c11575900ef3019834a8779070fbd38b841
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Fix xdoc typo
Commit: 6415232c6a4e4479342e6d7de077a2726b9f8053
https://github.com/acl2/acl2/commit/6415232c6a4e4479342e6d7de077a2726b9f8053
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/u...@useless-runes.lsp
Log Message:
-----------
[C$] Update useless runes
Commit: e04fbc783e9ee2db13a9aca00dfa04cc2d72c23d
https://github.com/acl2/acl2/commit/e04fbc783e9ee2db13a9aca00dfa04cc2d72c23d
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-information.lisp
Log Message:
-----------
[C$] Update XDOC
Commit: a5d7e5ae37d1c5851bf9d22dc07df64d5c38ef4b
https://github.com/acl2/acl2/commit/a5d7e5ae37d1c5851bf9d22dc07df64d5c38ef4b
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/uid.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
Log Message:
-----------
Update copyright years
Commit: ab3865a9fd4414b4235905d46c2be000349d40a9
https://github.com/acl2/acl2/commit/ab3865a9fd4414b4235905d46c2be000349d40a9
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Improve documentation
Thanks to Alessandro Coglio for suggesting these changes.
Commit: f5b961ee3e2c1c4601d361070df8969e6dae761b
https://github.com/acl2/acl2/commit/f5b961ee3e2c1c4601d361070df8969e6dae761b
Author: Grant Jurgensen <gr...@kestrel.edu>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
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/split-gso.lisp
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
Log Message:
-----------
Merge pull request #1904 from gjurgensen/gj-c$
[C$] Extend struct and union types
Compare: https://github.com/acl2/acl2/compare/f1215b5012c6...f5b961ee3e2c
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 4f305020e5e4a26fe729169550070dab53a01c30
https://github.com/acl2/acl2/commit/4f305020e5e4a26fe729169550070dab53a01c30
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.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
Log Message:
-----------
[C$] Extend struct and union types
Struct and union types now include their UID, translation unit name,
optional tag, and members if untagged. We also introduce a "completions"
map to associate tagged struct/union types to their members.
Validation was updated accordingly. Tests were added to the validator.
Commit: 27a169a8dad9e7592d836e66d21813ba4e0673e0
https://github.com/acl2/acl2/commit/27a169a8dad9e7592d836e66d21813ba4e0673e0
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
A books/kestrel/c/syntax/tests/types.lisp
Log Message:
-----------
[C$] Add type compatibility/composite tests
Commit: e3edd4d633bdde690277b0787d21a753ad6a57dc
https://github.com/acl2/acl2/commit/e3edd4d633bdde690277b0787d21a753ad6a57dc
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/validation-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/vali...@useless-runes.lsp
Log Message:
-----------
[C$] Update useless runes
Commit: 275baa82009a053f14f4e7256eced650e40ec05a
https://github.com/acl2/acl2/commit/275baa82009a053f14f4e7256eced650e40ec05a
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Add GCC extension to assignment typing
Allow function pointers to be used with void pointers in simple
assignment expresssion.
Commit: 2715c7988513fd532a4c7a0f7e1052295a4416dc
https://github.com/acl2/acl2/commit/2715c7988513fd532a4c7a0f7e1052295a4416dc
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/uid.lisp
Log Message:
-----------
[C$] Add XDOC parents to UID topics
Commit: c5a0e1eff8b1f72a82e210bee6bd6c9f030f07fd
https://github.com/acl2/acl2/commit/c5a0e1eff8b1f72a82e210bee6bd6c9f030f07fd
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/types.lisp
Log Message:
-----------
[C$] Add type helper functions
Commit: 6a1db295d54b7030c00d816a3bf1da8e51860abe
https://github.com/acl2/acl2/commit/6a1db295d54b7030c00d816a3bf1da8e51860abe
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/transformation/split-gso.lisp
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
Log Message:
-----------
[C2C] Update split-gso and tests
This adapts to the new C type fixtype. It also fixes some tests, which
were not actually valid C.
Commit: 1d9b193f9fd4bd40ced8846bf697718c4db5eb6e
https://github.com/acl2/acl2/commit/1d9b193f9fd4bd40ced8846bf697718c4db5eb6e
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
Log Message:
-----------
[C$] Fix xdoc typo
Commit: 70eec9b2de2b47c0ad69ec0392ae29534f5a520c
https://github.com/acl2/acl2/commit/70eec9b2de2b47c0ad69ec0392ae29534f5a520c
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/types.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Use a fast-alist for type completions map
This map can get quite large; using omaps became impractical.
Commit: 79217c11575900ef3019834a8779070fbd38b841
https://github.com/acl2/acl2/commit/79217c11575900ef3019834a8779070fbd38b841
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Fix xdoc typo
Commit: 6415232c6a4e4479342e6d7de077a2726b9f8053
https://github.com/acl2/acl2/commit/6415232c6a4e4479342e6d7de077a2726b9f8053
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/u...@useless-runes.lsp
Log Message:
-----------
[C$] Update useless runes
Commit: e04fbc783e9ee2db13a9aca00dfa04cc2d72c23d
https://github.com/acl2/acl2/commit/e04fbc783e9ee2db13a9aca00dfa04cc2d72c23d
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-information.lisp
Log Message:
-----------
[C$] Update XDOC
Commit: a5d7e5ae37d1c5851bf9d22dc07df64d5c38ef4b
https://github.com/acl2/acl2/commit/a5d7e5ae37d1c5851bf9d22dc07df64d5c38ef4b
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/uid.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
Log Message:
-----------
Update copyright years
Commit: ab3865a9fd4414b4235905d46c2be000349d40a9
https://github.com/acl2/acl2/commit/ab3865a9fd4414b4235905d46c2be000349d40a9
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Improve documentation
Thanks to Alessandro Coglio for suggesting these changes.
Commit: f5b961ee3e2c1c4601d361070df8969e6dae761b
https://github.com/acl2/acl2/commit/f5b961ee3e2c1c4601d361070df8969e6dae761b
Author: Grant Jurgensen <gr...@kestrel.edu>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
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/split-gso.lisp
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
Log Message:
-----------
Merge pull request #1904 from gjurgensen/gj-c$
[C$] Extend struct and union types
Compare: https://github.com/acl2/acl2/compare/f1215b5012c6...f5b961ee3e2c
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
acl2buildserver
Feb 6, 2026, 9:59:38 PM (4 days ago) Feb 6
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: 52676d42c9249f18bcd451f8c0f2f4fa415711d5
https://github.com/acl2/acl2/commit/52676d42c9249f18bcd451f8c0f2f4fa415711d5
Author: Eric Smith <ews...@gmail.com>
Log Message:
-----------
[C2C] Improve command-line tool.
Allow the new-dir and old-dir to be the same when overwrite-ok is true.
Commit: f837cd4a60a48c40ff73c03461b857ce306953da
https://github.com/acl2/acl2/commit/f837cd4a60a48c40ff73c03461b857ce306953da
Author: Eric Smith <ews...@gmail.com>
Commit: 837f6f84bd078f649a0bca1bd411eed507db75d5
https://github.com/acl2/acl2/commit/837f6f84bd078f649a0bca1bd411eed507db75d5
Author: ACL2 Build Server <acl2bui...@gmail.com>
Compare: https://github.com/acl2/acl2/compare/9983ebdf1a55...837f6f84bd07
https://github.com/acl2/acl2/commit/52676d42c9249f18bcd451f8c0f2f4fa415711d5
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/transformation/command-line/wrappers.lisp
Changed paths:
Log Message:
-----------
[C2C] Improve command-line tool.
Allow the new-dir and old-dir to be the same when overwrite-ok is true.
https://github.com/acl2/acl2/commit/f837cd4a60a48c40ff73c03461b857ce306953da
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
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/split-gso.lisp
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
Log Message:
-----------
Merge.
Changed paths:
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/split-gso.lisp
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
Log Message:
-----------
Commit: 837f6f84bd078f649a0bca1bd411eed507db75d5
https://github.com/acl2/acl2/commit/837f6f84bd078f649a0bca1bd411eed507db75d5
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
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
Changed paths:
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/split-gso.lisp
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
Log Message:
-----------
Merge commit 'f837cd4a60a48c40ff73c03461b857ce306953da' into HEAD
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
Log Message:
-----------
Compare: https://github.com/acl2/acl2/compare/9983ebdf1a55...837f6f84bd07
acl2buildserver
Feb 6, 2026, 10:00:36 PM (4 days ago) Feb 6
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Feb 8, 2026, 12:29:53 PM (2 days ago) Feb 8
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: 19d99a9dc7815eba4c2d9d981e42bf022ddb8147
https://github.com/acl2/acl2/commit/19d99a9dc7815eba4c2d9d981e42bf022ddb8147
Author: Andrew Walter <m...@atwalter.com>
Log Message:
-----------
[acl2s] Fix a type error in cgen's callback (#1899)
cgen's callback did not properly account for the fact that the ctx
argument may be a string and thus under certain circumstances it
would try to take the car of a string, causing a type error when ACL2
is built with `(safety 3)`.
This was fixed by adding a `consp` check before the offending `car`
form.
Commit: dd729c988c9d36f55c0c6dee79af958d0331a266
https://github.com/acl2/acl2/commit/dd729c988c9d36f55c0c6dee79af958d0331a266
Author: Pete Manolios <pman...@gmail.com>
M axioms.lisp
M books/GNUmakefile
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh
M books/doc/relnotes.lisp
M books/kestrel/acl2data/gather/patch-defthm.lsp
M books/kestrel/apt/solve-method-axe-rewriter.lisp
M books/kestrel/arithmetic-light/max.lisp
M books/kestrel/arithmetic-light/min.lisp
M books/kestrel/arm/def-inst.lisp
A books/kestrel/arm/doc.lisp
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/memory.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/arm/step.lisp
A books/kestrel/arm/tests/acl2-customization.lsp
A books/kestrel/arm/tests/simple.lisp
A books/kestrel/arm/top.lisp
M books/kestrel/auto-termination/td-cands.acl2
M books/kestrel/auto-termination/td-cands.lisp
M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/equivalence-checker.lisp
A books/kestrel/axe/evaluator-support.lisp
M books/kestrel/axe/evaluator-tests.acl2
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/evaluator.acl2
M books/kestrel/axe/evaluator.lisp
M books/kestrel/axe/hit-counts.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/prune-term.lisp
M books/kestrel/axe/rewriter-basic-smt-tests.lisp
M books/kestrel/axe/rewriter-basic-tests.lisp
M books/kestrel/axe/rewriter-basic.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/support-non-axe.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-limits.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/step-increments.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
R books/kestrel/axe/x86/evaluator-x86.acl2
M books/kestrel/axe/x86/evaluator-x86.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-32-proof.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-64-proof.lisp
A books/kestrel/axe/x86/lifter-support.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rewriter-x86-tests.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester-code-only.lisp
M books/kestrel/axe/x86/tester-rules.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/top.lisp
M books/kestrel/axe/x86/unroller-code-only.lisp
M books/kestrel/axe/x86/unroller.acl2
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/c/atc/generation.lisp
A books/kestrel/c/atc/limits.lisp
M books/kestrel/c/language/implementation-environments/versions.lisp
M books/kestrel/c/language/integer-operations.lisp
M books/kestrel/c/language/keywords.lisp
A books/kestrel/c/language/punctuators.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/builtin.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/lexer.lisp
A books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/output-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
A books/kestrel/c/syntax/preprocessor-evaluator.lisp
A books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
A books/kestrel/c/syntax/stringization.lisp
A books/kestrel/c/syntax/tests/c17-std-example-6.10.3.3.c
A books/kestrel/c/syntax/tests/c17-std-example-6.10.3.4.c
A books/kestrel/c/syntax/tests/c17-std-example1-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example2-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example3-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example4-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example5-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example6-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example7-6.10.3.5.c
A books/kestrel/c/syntax/tests/concatenate.c
A books/kestrel/c/syntax/tests/conditional.c
A books/kestrel/c/syntax/tests/gincluder.c
A books/kestrel/c/syntax/tests/gincluder1.h
A books/kestrel/c/syntax/tests/gincluder2.h
A books/kestrel/c/syntax/tests/guarded.h
M books/kestrel/c/syntax/tests/input-files.lisp
A books/kestrel/c/syntax/tests/macros.c
M books/kestrel/c/syntax/tests/output-files.lisp
M books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
A books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/stringize.c
M books/kestrel/c/syntax/tests/validator.lisp
A books/kestrel/c/syntax/token-concatenation.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/top.lisp
A books/kestrel/c/transformation/add-section-attr-doc.lisp
A books/kestrel/c/transformation/add-section-attr.lisp
A books/kestrel/c/transformation/command-line/tests/add-section-attr.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2.json
A books/kestrel/c/transformation/command-line/tests/input-files/file10.c
A books/kestrel/c/transformation/command-line/tests/input-files/file11.c
A books/kestrel/c/transformation/command-line/tests/input-files/file9.c
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
A books/kestrel/c/transformation/command-line/tests/split-gso-no-extensions.json
M books/kestrel/c/transformation/command-line/transform-c.lisp
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso.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
A books/kestrel/c/transformation/tests/add-section-attr/.gitignore
A books/kestrel/c/transformation/tests/add-section-attr/acl2-customization.lsp
A books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/cert.acl2
A books/kestrel/c/transformation/tests/add-section-attr/external-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/test1.c
A books/kestrel/c/transformation/tests/add-section-attr/test2.c
A books/kestrel/c/transformation/tests/add-section-attr/test3.c
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp
M books/kestrel/c/transformation/top.lisp
A books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
A books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/utilities/top.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
A books/kestrel/data/.sys/portc...@useless-runes.lsp
A books/kestrel/data/.sys/t...@useless-runes.lsp
A books/kestrel/data/acl2-customization.lsp
A books/kestrel/data/cert.acl2
A books/kestrel/data/doc.lisp
A books/kestrel/data/hash/.sys/jenkin...@useless-runes.lsp
A books/kestrel/data/hash/.sys/jen...@useless-runes.lsp
A books/kestrel/data/hash/.sys/portc...@useless-runes.lsp
A books/kestrel/data/hash/.sys/t...@useless-runes.lsp
A books/kestrel/data/hash/acl2-customization.lsp
A books/kestrel/data/hash/cert.acl2
A books/kestrel/data/hash/jenkins-defs.lisp
A books/kestrel/data/hash/jenkins.lisp
A books/kestrel/data/hash/package.lsp
A books/kestrel/data/hash/portcullis.acl2
A books/kestrel/data/hash/portcullis.lisp
A books/kestrel/data/hash/top.lisp
A books/kestrel/data/package.lsp
A books/kestrel/data/portcullis.acl2
A books/kestrel/data/portcullis.lisp
A books/kestrel/data/top.lisp
A books/kestrel/data/treeset/.sys/cardinal...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/cardi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/de...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/delet...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/del...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/diff...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/extensi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/f...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/generic-t...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/generi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/hash...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/ha...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/in-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/i...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/indu...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/inser...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/ins...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/interse...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/inte...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/iter...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/it...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/min-ma...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/min...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/portc...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/set-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/s...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/subse...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/to-ose...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/to-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/t...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/union...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/un...@useless-runes.lsp
A books/kestrel/data/treeset/acl2-customization.lsp
A books/kestrel/data/treeset/benchmark/acl2-customization.lsp
A books/kestrel/data/treeset/benchmark/benchmark.lsp
A books/kestrel/data/treeset/benchmark/cert.acl2
A books/kestrel/data/treeset/benchmark/random.lisp
A books/kestrel/data/treeset/cardinality-defs.lisp
A books/kestrel/data/treeset/cardinality.lisp
A books/kestrel/data/treeset/cert.acl2
A books/kestrel/data/treeset/defs.lisp
A books/kestrel/data/treeset/delete-defs.lisp
A books/kestrel/data/treeset/delete.lisp
A books/kestrel/data/treeset/diff-defs.lisp
A books/kestrel/data/treeset/diff.lisp
A books/kestrel/data/treeset/doc.lisp
A books/kestrel/data/treeset/extensionality.lisp
A books/kestrel/data/treeset/fty.lisp
A books/kestrel/data/treeset/generic-typed-defs.lisp
A books/kestrel/data/treeset/generic-typed.lisp
A books/kestrel/data/treeset/hash-defs.lisp
A books/kestrel/data/treeset/hash.lisp
A books/kestrel/data/treeset/in-defs.lisp
A books/kestrel/data/treeset/in.lisp
A books/kestrel/data/treeset/induction.lisp
A books/kestrel/data/treeset/insert-defs.lisp
A books/kestrel/data/treeset/insert.lisp
A books/kestrel/data/treeset/internal/.sys/antisy...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/bst-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/b...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/count...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/co...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/delet...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/del...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/diff...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap-or...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/he...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-ord...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-o...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/i...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/inser...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/ins...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/interse...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/inte...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/iter...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/it...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/join...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/jo...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/min-ma...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/min...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/rotat...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/rot...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/split...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/sp...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/subse...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/tree...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/tr...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/union...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/un...@useless-runes.lsp
A books/kestrel/data/treeset/internal/acl2-customization.lsp
A books/kestrel/data/treeset/internal/antisymmetry.lisp
A books/kestrel/data/treeset/internal/bst-defs.lisp
A books/kestrel/data/treeset/internal/bst.lisp
A books/kestrel/data/treeset/internal/cert.acl2
A books/kestrel/data/treeset/internal/count-defs.lisp
A books/kestrel/data/treeset/internal/count.lisp
A books/kestrel/data/treeset/internal/delete-defs.lisp
A books/kestrel/data/treeset/internal/delete.lisp
A books/kestrel/data/treeset/internal/diff-defs.lisp
A books/kestrel/data/treeset/internal/diff.lisp
A books/kestrel/data/treeset/internal/doc.lisp
A books/kestrel/data/treeset/internal/heap-defs.lisp
A books/kestrel/data/treeset/internal/heap-order-defs.lisp
A books/kestrel/data/treeset/internal/heap-order.lisp
A books/kestrel/data/treeset/internal/heap.lisp
A books/kestrel/data/treeset/internal/in-defs.lisp
A books/kestrel/data/treeset/internal/in-order-defs.lisp
A books/kestrel/data/treeset/internal/in-order.lisp
A books/kestrel/data/treeset/internal/in.lisp
A books/kestrel/data/treeset/internal/insert-defs.lisp
A books/kestrel/data/treeset/internal/insert.lisp
A books/kestrel/data/treeset/internal/intersect-defs.lisp
A books/kestrel/data/treeset/internal/intersect.lisp
A books/kestrel/data/treeset/internal/iter-defs.lisp
A books/kestrel/data/treeset/internal/iter.lisp
A books/kestrel/data/treeset/internal/join-defs.lisp
A books/kestrel/data/treeset/internal/join.lisp
A books/kestrel/data/treeset/internal/min-max-defs.lisp
A books/kestrel/data/treeset/internal/min-max.lisp
A books/kestrel/data/treeset/internal/rotate-defs.lisp
A books/kestrel/data/treeset/internal/rotate.lisp
A books/kestrel/data/treeset/internal/split-defs.lisp
A books/kestrel/data/treeset/internal/split.lisp
A books/kestrel/data/treeset/internal/subset-defs.lisp
A books/kestrel/data/treeset/internal/subset.lisp
A books/kestrel/data/treeset/internal/tree-defs.lisp
A books/kestrel/data/treeset/internal/tree.lisp
A books/kestrel/data/treeset/internal/union-defs.lisp
A books/kestrel/data/treeset/internal/union.lisp
A books/kestrel/data/treeset/intersect-defs.lisp
A books/kestrel/data/treeset/intersect.lisp
A books/kestrel/data/treeset/iter-defs.lisp
A books/kestrel/data/treeset/iter.lisp
A books/kestrel/data/treeset/min-max-defs.lisp
A books/kestrel/data/treeset/min-max.lisp
A books/kestrel/data/treeset/package.lsp
A books/kestrel/data/treeset/portcullis.acl2
A books/kestrel/data/treeset/portcullis.lisp
A books/kestrel/data/treeset/set-defs.lisp
A books/kestrel/data/treeset/set.lisp
A books/kestrel/data/treeset/subset-defs.lisp
A books/kestrel/data/treeset/subset.lisp
A books/kestrel/data/treeset/to-oset-defs.lisp
A books/kestrel/data/treeset/to-oset.lisp
A books/kestrel/data/treeset/top.lisp
A books/kestrel/data/treeset/union-defs.lisp
A books/kestrel/data/treeset/union.lisp
A books/kestrel/data/utilities/.sys/list...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/li...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/nat-...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/n...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/oset...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/os...@useless-runes.lsp
A books/kestrel/data/utilities/acl2-customization.lsp
A books/kestrel/data/utilities/bit-vectors/.sys/bitop...@useless-runes.lsp
A books/kestrel/data/utilities/bit-vectors/.sys/bit...@useless-runes.lsp
A books/kestrel/data/utilities/bit-vectors/acl2-customization.lsp
A books/kestrel/data/utilities/bit-vectors/bitops-defs.lisp
A books/kestrel/data/utilities/bit-vectors/bitops.lisp
A books/kestrel/data/utilities/bit-vectors/cert.acl2
A books/kestrel/data/utilities/cert.acl2
A books/kestrel/data/utilities/fixed-size-words/.sys/fix...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/.sys/u32-...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/.sys/u...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/acl2-customization.lsp
A books/kestrel/data/utilities/fixed-size-words/cert.acl2
A books/kestrel/data/utilities/fixed-size-words/fixnum.lisp
A books/kestrel/data/utilities/fixed-size-words/u32-defs.lisp
A books/kestrel/data/utilities/fixed-size-words/u32.lisp
A books/kestrel/data/utilities/list-defs.lisp
A books/kestrel/data/utilities/list.lisp
A books/kestrel/data/utilities/oset-defs.lisp
A books/kestrel/data/utilities/oset.lisp
A books/kestrel/data/utilities/top.lisp
A books/kestrel/data/utilities/total-order/.sys/max-...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/min-...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/total-or...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/total...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/acl2-customization.lsp
A books/kestrel/data/utilities/total-order/cert.acl2
A books/kestrel/data/utilities/total-order/max-defs.lisp
A books/kestrel/data/utilities/total-order/max.lisp
A books/kestrel/data/utilities/total-order/min-defs.lisp
A books/kestrel/data/utilities/total-order/min-max.lisp
A books/kestrel/data/utilities/total-order/min.lisp
A books/kestrel/data/utilities/total-order/total-order-defs.lisp
A books/kestrel/data/utilities/total-order/total-order.lisp
A books/kestrel/executable-parsers/.sys/elf-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/mach-o...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-e...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ex...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ma...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parsed-exec...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parser...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/pe-t...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/t...@useless-runes.lsp
A books/kestrel/executable-parsers/elf-tools.lisp
A books/kestrel/executable-parsers/mach-o-tools.lisp
A books/kestrel/executable-parsers/parse-elf-file.lisp
A books/kestrel/executable-parsers/parse-executable.lisp
A books/kestrel/executable-parsers/parse-mach-o-file.lisp
A books/kestrel/executable-parsers/parse-pe-file.lisp
A books/kestrel/executable-parsers/parsed-executable-tools.lisp
A books/kestrel/executable-parsers/parser-utils.lisp
A books/kestrel/executable-parsers/pe-tools.lisp
A books/kestrel/executable-parsers/top.lisp
M books/kestrel/fty/deffold-map-doc.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/helpers/advice-implementation.lisp
M books/kestrel/helpers/advice-tests.lisp
A books/kestrel/helpers/defrule-tests.lisp
M books/kestrel/helpers/package.lsp
M books/kestrel/helpers/speed-up-implementation.lisp
M books/kestrel/json-parser/parsed-json.lisp
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp
R books/kestrel/treeset/.sys/binary-t...@useless-runes.lsp
R books/kestrel/treeset/.sys/binar...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-ord...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-...@useless-runes.lsp
R books/kestrel/treeset/.sys/b...@useless-runes.lsp
R books/kestrel/treeset/.sys/cardinal...@useless-runes.lsp
R books/kestrel/treeset/.sys/cardi...@useless-runes.lsp
R books/kestrel/treeset/.sys/de...@useless-runes.lsp
R books/kestrel/treeset/.sys/delet...@useless-runes.lsp
R books/kestrel/treeset/.sys/del...@useless-runes.lsp
R books/kestrel/treeset/.sys/diff...@useless-runes.lsp
R books/kestrel/treeset/.sys/di...@useless-runes.lsp
R books/kestrel/treeset/.sys/double-co...@useless-runes.lsp
R books/kestrel/treeset/.sys/f...@useless-runes.lsp
R books/kestrel/treeset/.sys/ha...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap-or...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap-...@useless-runes.lsp
R books/kestrel/treeset/.sys/he...@useless-runes.lsp
R books/kestrel/treeset/.sys/in-...@useless-runes.lsp
R books/kestrel/treeset/.sys/i...@useless-runes.lsp
R books/kestrel/treeset/.sys/inser...@useless-runes.lsp
R books/kestrel/treeset/.sys/ins...@useless-runes.lsp
R books/kestrel/treeset/.sys/interse...@useless-runes.lsp
R books/kestrel/treeset/.sys/inte...@useless-runes.lsp
R books/kestrel/treeset/.sys/jenkin...@useless-runes.lsp
R books/kestrel/treeset/.sys/join...@useless-runes.lsp
R books/kestrel/treeset/.sys/jo...@useless-runes.lsp
R books/kestrel/treeset/.sys/pick-a...@useless-runes.lsp
R books/kestrel/treeset/.sys/portc...@useless-runes.lsp
R books/kestrel/treeset/.sys/rotat...@useless-runes.lsp
R books/kestrel/treeset/.sys/rot...@useless-runes.lsp
R books/kestrel/treeset/.sys/set-...@useless-runes.lsp
R books/kestrel/treeset/.sys/s...@useless-runes.lsp
R books/kestrel/treeset/.sys/split...@useless-runes.lsp
R books/kestrel/treeset/.sys/sp...@useless-runes.lsp
R books/kestrel/treeset/.sys/subse...@useless-runes.lsp
R books/kestrel/treeset/.sys/sub...@useless-runes.lsp
R books/kestrel/treeset/.sys/sum-acl2-...@useless-runes.lsp
R books/kestrel/treeset/.sys/sum-acl...@useless-runes.lsp
R books/kestrel/treeset/.sys/t...@useless-runes.lsp
R books/kestrel/treeset/.sys/total...@useless-runes.lsp
R books/kestrel/treeset/.sys/union...@useless-runes.lsp
R books/kestrel/treeset/.sys/un...@useless-runes.lsp
R books/kestrel/treeset/acl2-customization.lsp
R books/kestrel/treeset/binary-tree-defs.lisp
R books/kestrel/treeset/binary-tree.lisp
R books/kestrel/treeset/bst-defs.lisp
R books/kestrel/treeset/bst-order-defs.lisp
R books/kestrel/treeset/bst-order.lisp
R books/kestrel/treeset/bst.lisp
R books/kestrel/treeset/cardinality-defs.lisp
R books/kestrel/treeset/cardinality.lisp
R books/kestrel/treeset/cert.acl2
R books/kestrel/treeset/defs.lisp
R books/kestrel/treeset/delete-defs.lisp
R books/kestrel/treeset/delete.lisp
R books/kestrel/treeset/diff-defs.lisp
R books/kestrel/treeset/diff.lisp
R books/kestrel/treeset/double-containment.lisp
R books/kestrel/treeset/fty.lisp
R books/kestrel/treeset/hash.lisp
R books/kestrel/treeset/heap-defs.lisp
R books/kestrel/treeset/heap-order-defs.lisp
R books/kestrel/treeset/heap-order.lisp
R books/kestrel/treeset/heap.lisp
R books/kestrel/treeset/in-defs.lisp
R books/kestrel/treeset/in.lisp
R books/kestrel/treeset/insert-defs.lisp
R books/kestrel/treeset/insert.lisp
R books/kestrel/treeset/intersect-defs.lisp
R books/kestrel/treeset/intersect.lisp
R books/kestrel/treeset/jenkins-hash.lisp
R books/kestrel/treeset/join-defs.lisp
R books/kestrel/treeset/join.lisp
R books/kestrel/treeset/package.lsp
R books/kestrel/treeset/pick-a-point.lisp
R books/kestrel/treeset/portcullis.acl2
R books/kestrel/treeset/portcullis.lisp
R books/kestrel/treeset/rotate-defs.lisp
R books/kestrel/treeset/rotate.lisp
R books/kestrel/treeset/set-defs.lisp
R books/kestrel/treeset/set.lisp
R books/kestrel/treeset/split-defs.lisp
R books/kestrel/treeset/split.lisp
R books/kestrel/treeset/subset-defs.lisp
R books/kestrel/treeset/subset.lisp
R books/kestrel/treeset/sum-acl2-count-defs.lisp
R books/kestrel/treeset/sum-acl2-count.lisp
R books/kestrel/treeset/tests/.sys/mk-r...@useless-runes.lsp
R books/kestrel/treeset/tests/.sys/mk-...@useless-runes.lsp
R books/kestrel/treeset/tests/.sys/time...@useless-runes.lsp
R books/kestrel/treeset/tests/acl2-customization.lsp
R books/kestrel/treeset/tests/cert.acl2
R books/kestrel/treeset/tests/mk-random.lisp
R books/kestrel/treeset/tests/mk-set.lisp
R books/kestrel/treeset/tests/tests.lsp
R books/kestrel/treeset/tests/time-set.lisp
R books/kestrel/treeset/top.lisp
R books/kestrel/treeset/total-order.lisp
R books/kestrel/treeset/union-defs.lisp
R books/kestrel/treeset/union.lisp
M books/kestrel/utilities/ld-history.lisp
M books/kestrel/utilities/redundancy.lisp
M books/kestrel/utilities/run-json-command.lisp
M books/kestrel/utilities/verify-guards-program-tests.lisp
M books/kestrel/utilities/verify-guards-program.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/assumptions64.lisp
M books/kestrel/x86/package.lsp
R books/kestrel/x86/parsers/.sys/elf-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/mach-o...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-e...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ex...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ma...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parsed-exec...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parser...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/pe-t...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/t...@useless-runes.lsp
R books/kestrel/x86/parsers/elf-tools.lisp
R books/kestrel/x86/parsers/mach-o-tools.lisp
R books/kestrel/x86/parsers/parse-elf-file.lisp
R books/kestrel/x86/parsers/parse-executable.lisp
R books/kestrel/x86/parsers/parse-mach-o-file.lisp
R books/kestrel/x86/parsers/parse-pe-file.lisp
R books/kestrel/x86/parsers/parsed-executable-tools.lisp
R books/kestrel/x86/parsers/parser-utils.lisp
R books/kestrel/x86/parsers/pe-tools.lisp
R books/kestrel/x86/parsers/top.lisp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
M books/kestrel/x86/top.lisp
R books/kestrel/x86/x86-changes.acl2
M books/kestrel/x86/x86-changes.lisp
M books/projects/hol-in-acl2/README
A books/projects/hol-in-acl2/acl2/hpp-set.lisp
M books/projects/hol-in-acl2/acl2/package.lsp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
M books/projects/hol-in-acl2/acl2/theories.lisp
R books/projects/hol-in-acl2/examples/README
A books/projects/hol-in-acl2/examples/README.txt
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/eval_poly.defhol
A books/projects/hol-in-acl2/examples/eval_polyScript.sml
M books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
M books/projects/hol-in-acl2/examples/ex1-top.lisp
A books/projects/hol-in-acl2/examples/ex1.defhol
A books/projects/hol-in-acl2/examples/ex1Script.sml
R books/projects/hol-in-acl2/hol4/eval-poly.sml
R books/projects/hol-in-acl2/hol4/ex1.sml
R books/projects/hol-in-acl2/hol4/translator.sml
M books/projects/hol-in-acl2/to-do.txt
M books/projects/vescmul/int-vector-adders-meta.lisp
M books/projects/x86isa/machine/cert.acl2
M books/projects/x86isa/machine/environment-and-syscalls-raw.lsp
M books/projects/x86isa/machine/other-non-det-raw.lsp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/register-readers-and-writers-raw.lsp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/tools/execution/top.lisp
M books/std/strings/bin-digit-char-listp.lisp
M books/std/strings/dec-digit-char-listp.lisp
M books/std/strings/hex-digit-char-listp.lisp
M books/std/strings/oct-digit-char-listp.lisp
M books/std/util/defaggregate.lisp
M books/std/util/defprojection.lisp
M books/std/util/defrule.lisp
M books/std/util/tests/defaggregate.lisp
M books/system/doc/acl2-doc.lisp
A books/tools/eval-events-from-file-doc.lisp
A books/tools/eval-events-from-file-test-data.lsp
A books/tools/eval-events-from-file-test.lisp
A books/tools/eval-events-from-file.lisp
M books/tools/top.lisp
M books/tools/with-supporters-doc.lisp
M books/tools/with-supporters.lisp
M books/xdoc/display.lisp
M defthm.lisp
M defuns.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp
M other-events.lisp
M proof-builder-b.lisp
Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/master' into testing-acl2s
Commit: f1215b5012c66da463b258e2e2eb2b6e3427af68
https://github.com/acl2/acl2/commit/f1215b5012c66da463b258e2e2eb2b6e3427af68
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/utilities/add-attributes.lisp
Log Message:
-----------
[C2C] Fix add-section-attr bug
Declarations with empty initializer declarator lists were being
erroneously dropped. Extended a test case to test for the desired
behavior.
Commit: a5d7e5ae37d1c5851bf9d22dc07df64d5c38ef4b
https://github.com/acl2/acl2/commit/a5d7e5ae37d1c5851bf9d22dc07df64d5c38ef4b
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/uid.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
Log Message:
-----------
Update copyright years
Commit: 4d8e886d5429c845772acb31343190d0dd8916b9
https://github.com/acl2/acl2/commit/4d8e886d5429c845772acb31343190d0dd8916b9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve preprocessor implementation.
Make the maximum macro reach part of the stobj.
Commit: bc13f6577e0cebed432ea0ce8929603d2e542dde
https://github.com/acl2/acl2/commit/bc13f6577e0cebed432ea0ce8929603d2e542dde
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/utilities/add-attributes.lisp
Log Message:
-----------
Merge commit 'f1215b5012c66da463b258e2e2eb2b6e3427af68' into HEAD
Commit: 9983ebdf1a551b55f3b91a5234f31cdf51223ade
https://github.com/acl2/acl2/commit/9983ebdf1a551b55f3b91a5234f31cdf51223ade
Author: Matt Kaufmann <matthew.j...@gmail.com>
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:
-----------
Small updates to eval_poly example of hol-in-acl2 project
Commit: 57a866ed42bcbf2f363d132b906b297c16583feb
https://github.com/acl2/acl2/commit/57a866ed42bcbf2f363d132b906b297c16583feb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C$] Update some doc.
Commit: 7f0bb469e4404dfbbc830a0979682ea3d12fa882
https://github.com/acl2/acl2/commit/7f0bb469e4404dfbbc830a0979682ea3d12fa882
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C$] Add file dependencies to preprocessor tests.
Commit: 5705fc5abfb60ca3c9309c693290fed5977f6cfc
https://github.com/acl2/acl2/commit/5705fc5abfb60ca3c9309c693290fed5977f6cfc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
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/transformation/tests/add-section-attr/test3.c
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/41dd9ee939c5...e8022dad2758
https://github.com/acl2/acl2/commit/19d99a9dc7815eba4c2d9d981e42bf022ddb8147
Author: Andrew Walter <m...@atwalter.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/acl2s/cgen/callback.lisp
Changed paths:
Log Message:
-----------
[acl2s] Fix a type error in cgen's callback (#1899)
cgen's callback did not properly account for the fact that the ctx
argument may be a string and thus under certain circumstances it
would try to take the car of a string, causing a type error when ACL2
is built with `(safety 3)`.
This was fixed by adding a `consp` check before the offending `car`
form.
Commit: dd729c988c9d36f55c0c6dee79af958d0331a266
https://github.com/acl2/acl2/commit/dd729c988c9d36f55c0c6dee79af958d0331a266
Author: Pete Manolios <pman...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M acl2-init.lisp
Changed paths:
M axioms.lisp
M books/GNUmakefile
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh
M books/doc/relnotes.lisp
M books/kestrel/acl2data/gather/patch-defthm.lsp
M books/kestrel/apt/solve-method-axe-rewriter.lisp
M books/kestrel/arithmetic-light/max.lisp
M books/kestrel/arithmetic-light/min.lisp
M books/kestrel/arm/def-inst.lisp
A books/kestrel/arm/doc.lisp
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/memory.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/arm/step.lisp
A books/kestrel/arm/tests/acl2-customization.lsp
A books/kestrel/arm/tests/simple.lisp
A books/kestrel/arm/top.lisp
M books/kestrel/auto-termination/td-cands.acl2
M books/kestrel/auto-termination/td-cands.lisp
M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/equivalence-checker.lisp
A books/kestrel/axe/evaluator-support.lisp
M books/kestrel/axe/evaluator-tests.acl2
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/evaluator.acl2
M books/kestrel/axe/evaluator.lisp
M books/kestrel/axe/hit-counts.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/prune-term.lisp
M books/kestrel/axe/rewriter-basic-smt-tests.lisp
M books/kestrel/axe/rewriter-basic-tests.lisp
M books/kestrel/axe/rewriter-basic.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/support-non-axe.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-limits.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/step-increments.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
R books/kestrel/axe/x86/evaluator-x86.acl2
M books/kestrel/axe/x86/evaluator-x86.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-32-proof.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-64-proof.lisp
A books/kestrel/axe/x86/lifter-support.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rewriter-x86-tests.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester-code-only.lisp
M books/kestrel/axe/x86/tester-rules.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/top.lisp
M books/kestrel/axe/x86/unroller-code-only.lisp
M books/kestrel/axe/x86/unroller.acl2
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/c/atc/generation.lisp
A books/kestrel/c/atc/limits.lisp
M books/kestrel/c/language/implementation-environments/versions.lisp
M books/kestrel/c/language/integer-operations.lisp
M books/kestrel/c/language/keywords.lisp
A books/kestrel/c/language/punctuators.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/builtin.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/lexer.lisp
A books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/output-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
A books/kestrel/c/syntax/preprocessor-evaluator.lisp
A books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
A books/kestrel/c/syntax/stringization.lisp
A books/kestrel/c/syntax/tests/c17-std-example-6.10.3.3.c
A books/kestrel/c/syntax/tests/c17-std-example-6.10.3.4.c
A books/kestrel/c/syntax/tests/c17-std-example1-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example2-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example3-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example4-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example5-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example6-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example7-6.10.3.5.c
A books/kestrel/c/syntax/tests/concatenate.c
A books/kestrel/c/syntax/tests/conditional.c
A books/kestrel/c/syntax/tests/gincluder.c
A books/kestrel/c/syntax/tests/gincluder1.h
A books/kestrel/c/syntax/tests/gincluder2.h
A books/kestrel/c/syntax/tests/guarded.h
M books/kestrel/c/syntax/tests/input-files.lisp
A books/kestrel/c/syntax/tests/macros.c
M books/kestrel/c/syntax/tests/output-files.lisp
M books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
A books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/stringize.c
M books/kestrel/c/syntax/tests/validator.lisp
A books/kestrel/c/syntax/token-concatenation.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/top.lisp
A books/kestrel/c/transformation/add-section-attr-doc.lisp
A books/kestrel/c/transformation/add-section-attr.lisp
A books/kestrel/c/transformation/command-line/tests/add-section-attr.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2.json
A books/kestrel/c/transformation/command-line/tests/input-files/file10.c
A books/kestrel/c/transformation/command-line/tests/input-files/file11.c
A books/kestrel/c/transformation/command-line/tests/input-files/file9.c
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
A books/kestrel/c/transformation/command-line/tests/split-gso-no-extensions.json
M books/kestrel/c/transformation/command-line/transform-c.lisp
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso.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
A books/kestrel/c/transformation/tests/add-section-attr/.gitignore
A books/kestrel/c/transformation/tests/add-section-attr/acl2-customization.lsp
A books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/cert.acl2
A books/kestrel/c/transformation/tests/add-section-attr/external-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/test1.c
A books/kestrel/c/transformation/tests/add-section-attr/test2.c
A books/kestrel/c/transformation/tests/add-section-attr/test3.c
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp
M books/kestrel/c/transformation/top.lisp
A books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
A books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/utilities/top.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
A books/kestrel/data/.sys/portc...@useless-runes.lsp
A books/kestrel/data/.sys/t...@useless-runes.lsp
A books/kestrel/data/acl2-customization.lsp
A books/kestrel/data/cert.acl2
A books/kestrel/data/doc.lisp
A books/kestrel/data/hash/.sys/jenkin...@useless-runes.lsp
A books/kestrel/data/hash/.sys/jen...@useless-runes.lsp
A books/kestrel/data/hash/.sys/portc...@useless-runes.lsp
A books/kestrel/data/hash/.sys/t...@useless-runes.lsp
A books/kestrel/data/hash/acl2-customization.lsp
A books/kestrel/data/hash/cert.acl2
A books/kestrel/data/hash/jenkins-defs.lisp
A books/kestrel/data/hash/jenkins.lisp
A books/kestrel/data/hash/package.lsp
A books/kestrel/data/hash/portcullis.acl2
A books/kestrel/data/hash/portcullis.lisp
A books/kestrel/data/hash/top.lisp
A books/kestrel/data/package.lsp
A books/kestrel/data/portcullis.acl2
A books/kestrel/data/portcullis.lisp
A books/kestrel/data/top.lisp
A books/kestrel/data/treeset/.sys/cardinal...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/cardi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/de...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/delet...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/del...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/diff...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/extensi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/f...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/generic-t...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/generi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/hash...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/ha...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/in-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/i...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/indu...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/inser...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/ins...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/interse...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/inte...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/iter...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/it...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/min-ma...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/min...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/portc...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/set-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/s...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/subse...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/to-ose...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/to-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/t...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/union...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/un...@useless-runes.lsp
A books/kestrel/data/treeset/acl2-customization.lsp
A books/kestrel/data/treeset/benchmark/acl2-customization.lsp
A books/kestrel/data/treeset/benchmark/benchmark.lsp
A books/kestrel/data/treeset/benchmark/cert.acl2
A books/kestrel/data/treeset/benchmark/random.lisp
A books/kestrel/data/treeset/cardinality-defs.lisp
A books/kestrel/data/treeset/cardinality.lisp
A books/kestrel/data/treeset/cert.acl2
A books/kestrel/data/treeset/defs.lisp
A books/kestrel/data/treeset/delete-defs.lisp
A books/kestrel/data/treeset/delete.lisp
A books/kestrel/data/treeset/diff-defs.lisp
A books/kestrel/data/treeset/diff.lisp
A books/kestrel/data/treeset/doc.lisp
A books/kestrel/data/treeset/extensionality.lisp
A books/kestrel/data/treeset/fty.lisp
A books/kestrel/data/treeset/generic-typed-defs.lisp
A books/kestrel/data/treeset/generic-typed.lisp
A books/kestrel/data/treeset/hash-defs.lisp
A books/kestrel/data/treeset/hash.lisp
A books/kestrel/data/treeset/in-defs.lisp
A books/kestrel/data/treeset/in.lisp
A books/kestrel/data/treeset/induction.lisp
A books/kestrel/data/treeset/insert-defs.lisp
A books/kestrel/data/treeset/insert.lisp
A books/kestrel/data/treeset/internal/.sys/antisy...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/bst-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/b...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/count...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/co...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/delet...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/del...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/diff...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap-or...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/he...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-ord...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-o...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/i...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/inser...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/ins...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/interse...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/inte...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/iter...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/it...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/join...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/jo...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/min-ma...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/min...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/rotat...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/rot...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/split...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/sp...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/subse...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/tree...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/tr...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/union...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/un...@useless-runes.lsp
A books/kestrel/data/treeset/internal/acl2-customization.lsp
A books/kestrel/data/treeset/internal/antisymmetry.lisp
A books/kestrel/data/treeset/internal/bst-defs.lisp
A books/kestrel/data/treeset/internal/bst.lisp
A books/kestrel/data/treeset/internal/cert.acl2
A books/kestrel/data/treeset/internal/count-defs.lisp
A books/kestrel/data/treeset/internal/count.lisp
A books/kestrel/data/treeset/internal/delete-defs.lisp
A books/kestrel/data/treeset/internal/delete.lisp
A books/kestrel/data/treeset/internal/diff-defs.lisp
A books/kestrel/data/treeset/internal/diff.lisp
A books/kestrel/data/treeset/internal/doc.lisp
A books/kestrel/data/treeset/internal/heap-defs.lisp
A books/kestrel/data/treeset/internal/heap-order-defs.lisp
A books/kestrel/data/treeset/internal/heap-order.lisp
A books/kestrel/data/treeset/internal/heap.lisp
A books/kestrel/data/treeset/internal/in-defs.lisp
A books/kestrel/data/treeset/internal/in-order-defs.lisp
A books/kestrel/data/treeset/internal/in-order.lisp
A books/kestrel/data/treeset/internal/in.lisp
A books/kestrel/data/treeset/internal/insert-defs.lisp
A books/kestrel/data/treeset/internal/insert.lisp
A books/kestrel/data/treeset/internal/intersect-defs.lisp
A books/kestrel/data/treeset/internal/intersect.lisp
A books/kestrel/data/treeset/internal/iter-defs.lisp
A books/kestrel/data/treeset/internal/iter.lisp
A books/kestrel/data/treeset/internal/join-defs.lisp
A books/kestrel/data/treeset/internal/join.lisp
A books/kestrel/data/treeset/internal/min-max-defs.lisp
A books/kestrel/data/treeset/internal/min-max.lisp
A books/kestrel/data/treeset/internal/rotate-defs.lisp
A books/kestrel/data/treeset/internal/rotate.lisp
A books/kestrel/data/treeset/internal/split-defs.lisp
A books/kestrel/data/treeset/internal/split.lisp
A books/kestrel/data/treeset/internal/subset-defs.lisp
A books/kestrel/data/treeset/internal/subset.lisp
A books/kestrel/data/treeset/internal/tree-defs.lisp
A books/kestrel/data/treeset/internal/tree.lisp
A books/kestrel/data/treeset/internal/union-defs.lisp
A books/kestrel/data/treeset/internal/union.lisp
A books/kestrel/data/treeset/intersect-defs.lisp
A books/kestrel/data/treeset/intersect.lisp
A books/kestrel/data/treeset/iter-defs.lisp
A books/kestrel/data/treeset/iter.lisp
A books/kestrel/data/treeset/min-max-defs.lisp
A books/kestrel/data/treeset/min-max.lisp
A books/kestrel/data/treeset/package.lsp
A books/kestrel/data/treeset/portcullis.acl2
A books/kestrel/data/treeset/portcullis.lisp
A books/kestrel/data/treeset/set-defs.lisp
A books/kestrel/data/treeset/set.lisp
A books/kestrel/data/treeset/subset-defs.lisp
A books/kestrel/data/treeset/subset.lisp
A books/kestrel/data/treeset/to-oset-defs.lisp
A books/kestrel/data/treeset/to-oset.lisp
A books/kestrel/data/treeset/top.lisp
A books/kestrel/data/treeset/union-defs.lisp
A books/kestrel/data/treeset/union.lisp
A books/kestrel/data/utilities/.sys/list...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/li...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/nat-...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/n...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/oset...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/os...@useless-runes.lsp
A books/kestrel/data/utilities/acl2-customization.lsp
A books/kestrel/data/utilities/bit-vectors/.sys/bitop...@useless-runes.lsp
A books/kestrel/data/utilities/bit-vectors/.sys/bit...@useless-runes.lsp
A books/kestrel/data/utilities/bit-vectors/acl2-customization.lsp
A books/kestrel/data/utilities/bit-vectors/bitops-defs.lisp
A books/kestrel/data/utilities/bit-vectors/bitops.lisp
A books/kestrel/data/utilities/bit-vectors/cert.acl2
A books/kestrel/data/utilities/cert.acl2
A books/kestrel/data/utilities/fixed-size-words/.sys/fix...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/.sys/u32-...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/.sys/u...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/acl2-customization.lsp
A books/kestrel/data/utilities/fixed-size-words/cert.acl2
A books/kestrel/data/utilities/fixed-size-words/fixnum.lisp
A books/kestrel/data/utilities/fixed-size-words/u32-defs.lisp
A books/kestrel/data/utilities/fixed-size-words/u32.lisp
A books/kestrel/data/utilities/list-defs.lisp
A books/kestrel/data/utilities/list.lisp
A books/kestrel/data/utilities/oset-defs.lisp
A books/kestrel/data/utilities/oset.lisp
A books/kestrel/data/utilities/top.lisp
A books/kestrel/data/utilities/total-order/.sys/max-...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/min-...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/total-or...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/total...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/acl2-customization.lsp
A books/kestrel/data/utilities/total-order/cert.acl2
A books/kestrel/data/utilities/total-order/max-defs.lisp
A books/kestrel/data/utilities/total-order/max.lisp
A books/kestrel/data/utilities/total-order/min-defs.lisp
A books/kestrel/data/utilities/total-order/min-max.lisp
A books/kestrel/data/utilities/total-order/min.lisp
A books/kestrel/data/utilities/total-order/total-order-defs.lisp
A books/kestrel/data/utilities/total-order/total-order.lisp
A books/kestrel/executable-parsers/.sys/elf-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/mach-o...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-e...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ex...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ma...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parsed-exec...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parser...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/pe-t...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/t...@useless-runes.lsp
A books/kestrel/executable-parsers/elf-tools.lisp
A books/kestrel/executable-parsers/mach-o-tools.lisp
A books/kestrel/executable-parsers/parse-elf-file.lisp
A books/kestrel/executable-parsers/parse-executable.lisp
A books/kestrel/executable-parsers/parse-mach-o-file.lisp
A books/kestrel/executable-parsers/parse-pe-file.lisp
A books/kestrel/executable-parsers/parsed-executable-tools.lisp
A books/kestrel/executable-parsers/parser-utils.lisp
A books/kestrel/executable-parsers/pe-tools.lisp
A books/kestrel/executable-parsers/top.lisp
M books/kestrel/fty/deffold-map-doc.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/helpers/advice-implementation.lisp
M books/kestrel/helpers/advice-tests.lisp
A books/kestrel/helpers/defrule-tests.lisp
M books/kestrel/helpers/package.lsp
M books/kestrel/helpers/speed-up-implementation.lisp
M books/kestrel/json-parser/parsed-json.lisp
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp
R books/kestrel/treeset/.sys/binary-t...@useless-runes.lsp
R books/kestrel/treeset/.sys/binar...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-ord...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-...@useless-runes.lsp
R books/kestrel/treeset/.sys/b...@useless-runes.lsp
R books/kestrel/treeset/.sys/cardinal...@useless-runes.lsp
R books/kestrel/treeset/.sys/cardi...@useless-runes.lsp
R books/kestrel/treeset/.sys/de...@useless-runes.lsp
R books/kestrel/treeset/.sys/delet...@useless-runes.lsp
R books/kestrel/treeset/.sys/del...@useless-runes.lsp
R books/kestrel/treeset/.sys/diff...@useless-runes.lsp
R books/kestrel/treeset/.sys/di...@useless-runes.lsp
R books/kestrel/treeset/.sys/double-co...@useless-runes.lsp
R books/kestrel/treeset/.sys/f...@useless-runes.lsp
R books/kestrel/treeset/.sys/ha...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap-or...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap-...@useless-runes.lsp
R books/kestrel/treeset/.sys/he...@useless-runes.lsp
R books/kestrel/treeset/.sys/in-...@useless-runes.lsp
R books/kestrel/treeset/.sys/i...@useless-runes.lsp
R books/kestrel/treeset/.sys/inser...@useless-runes.lsp
R books/kestrel/treeset/.sys/ins...@useless-runes.lsp
R books/kestrel/treeset/.sys/interse...@useless-runes.lsp
R books/kestrel/treeset/.sys/inte...@useless-runes.lsp
R books/kestrel/treeset/.sys/jenkin...@useless-runes.lsp
R books/kestrel/treeset/.sys/join...@useless-runes.lsp
R books/kestrel/treeset/.sys/jo...@useless-runes.lsp
R books/kestrel/treeset/.sys/pick-a...@useless-runes.lsp
R books/kestrel/treeset/.sys/portc...@useless-runes.lsp
R books/kestrel/treeset/.sys/rotat...@useless-runes.lsp
R books/kestrel/treeset/.sys/rot...@useless-runes.lsp
R books/kestrel/treeset/.sys/set-...@useless-runes.lsp
R books/kestrel/treeset/.sys/s...@useless-runes.lsp
R books/kestrel/treeset/.sys/split...@useless-runes.lsp
R books/kestrel/treeset/.sys/sp...@useless-runes.lsp
R books/kestrel/treeset/.sys/subse...@useless-runes.lsp
R books/kestrel/treeset/.sys/sub...@useless-runes.lsp
R books/kestrel/treeset/.sys/sum-acl2-...@useless-runes.lsp
R books/kestrel/treeset/.sys/sum-acl...@useless-runes.lsp
R books/kestrel/treeset/.sys/t...@useless-runes.lsp
R books/kestrel/treeset/.sys/total...@useless-runes.lsp
R books/kestrel/treeset/.sys/union...@useless-runes.lsp
R books/kestrel/treeset/.sys/un...@useless-runes.lsp
R books/kestrel/treeset/acl2-customization.lsp
R books/kestrel/treeset/binary-tree-defs.lisp
R books/kestrel/treeset/binary-tree.lisp
R books/kestrel/treeset/bst-defs.lisp
R books/kestrel/treeset/bst-order-defs.lisp
R books/kestrel/treeset/bst-order.lisp
R books/kestrel/treeset/bst.lisp
R books/kestrel/treeset/cardinality-defs.lisp
R books/kestrel/treeset/cardinality.lisp
R books/kestrel/treeset/cert.acl2
R books/kestrel/treeset/defs.lisp
R books/kestrel/treeset/delete-defs.lisp
R books/kestrel/treeset/delete.lisp
R books/kestrel/treeset/diff-defs.lisp
R books/kestrel/treeset/diff.lisp
R books/kestrel/treeset/double-containment.lisp
R books/kestrel/treeset/fty.lisp
R books/kestrel/treeset/hash.lisp
R books/kestrel/treeset/heap-defs.lisp
R books/kestrel/treeset/heap-order-defs.lisp
R books/kestrel/treeset/heap-order.lisp
R books/kestrel/treeset/heap.lisp
R books/kestrel/treeset/in-defs.lisp
R books/kestrel/treeset/in.lisp
R books/kestrel/treeset/insert-defs.lisp
R books/kestrel/treeset/insert.lisp
R books/kestrel/treeset/intersect-defs.lisp
R books/kestrel/treeset/intersect.lisp
R books/kestrel/treeset/jenkins-hash.lisp
R books/kestrel/treeset/join-defs.lisp
R books/kestrel/treeset/join.lisp
R books/kestrel/treeset/package.lsp
R books/kestrel/treeset/pick-a-point.lisp
R books/kestrel/treeset/portcullis.acl2
R books/kestrel/treeset/portcullis.lisp
R books/kestrel/treeset/rotate-defs.lisp
R books/kestrel/treeset/rotate.lisp
R books/kestrel/treeset/set-defs.lisp
R books/kestrel/treeset/set.lisp
R books/kestrel/treeset/split-defs.lisp
R books/kestrel/treeset/split.lisp
R books/kestrel/treeset/subset-defs.lisp
R books/kestrel/treeset/subset.lisp
R books/kestrel/treeset/sum-acl2-count-defs.lisp
R books/kestrel/treeset/sum-acl2-count.lisp
R books/kestrel/treeset/tests/.sys/mk-r...@useless-runes.lsp
R books/kestrel/treeset/tests/.sys/mk-...@useless-runes.lsp
R books/kestrel/treeset/tests/.sys/time...@useless-runes.lsp
R books/kestrel/treeset/tests/acl2-customization.lsp
R books/kestrel/treeset/tests/cert.acl2
R books/kestrel/treeset/tests/mk-random.lisp
R books/kestrel/treeset/tests/mk-set.lisp
R books/kestrel/treeset/tests/tests.lsp
R books/kestrel/treeset/tests/time-set.lisp
R books/kestrel/treeset/top.lisp
R books/kestrel/treeset/total-order.lisp
R books/kestrel/treeset/union-defs.lisp
R books/kestrel/treeset/union.lisp
M books/kestrel/utilities/ld-history.lisp
M books/kestrel/utilities/redundancy.lisp
M books/kestrel/utilities/run-json-command.lisp
M books/kestrel/utilities/verify-guards-program-tests.lisp
M books/kestrel/utilities/verify-guards-program.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/assumptions64.lisp
M books/kestrel/x86/package.lsp
R books/kestrel/x86/parsers/.sys/elf-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/mach-o...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-e...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ex...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ma...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parsed-exec...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parser...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/pe-t...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/t...@useless-runes.lsp
R books/kestrel/x86/parsers/elf-tools.lisp
R books/kestrel/x86/parsers/mach-o-tools.lisp
R books/kestrel/x86/parsers/parse-elf-file.lisp
R books/kestrel/x86/parsers/parse-executable.lisp
R books/kestrel/x86/parsers/parse-mach-o-file.lisp
R books/kestrel/x86/parsers/parse-pe-file.lisp
R books/kestrel/x86/parsers/parsed-executable-tools.lisp
R books/kestrel/x86/parsers/parser-utils.lisp
R books/kestrel/x86/parsers/pe-tools.lisp
R books/kestrel/x86/parsers/top.lisp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
M books/kestrel/x86/top.lisp
R books/kestrel/x86/x86-changes.acl2
M books/kestrel/x86/x86-changes.lisp
M books/projects/hol-in-acl2/README
A books/projects/hol-in-acl2/acl2/hpp-set.lisp
M books/projects/hol-in-acl2/acl2/package.lsp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
M books/projects/hol-in-acl2/acl2/theories.lisp
R books/projects/hol-in-acl2/examples/README
A books/projects/hol-in-acl2/examples/README.txt
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/eval_poly.defhol
A books/projects/hol-in-acl2/examples/eval_polyScript.sml
M books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
M books/projects/hol-in-acl2/examples/ex1-top.lisp
A books/projects/hol-in-acl2/examples/ex1.defhol
A books/projects/hol-in-acl2/examples/ex1Script.sml
R books/projects/hol-in-acl2/hol4/eval-poly.sml
R books/projects/hol-in-acl2/hol4/ex1.sml
R books/projects/hol-in-acl2/hol4/translator.sml
M books/projects/hol-in-acl2/to-do.txt
M books/projects/vescmul/int-vector-adders-meta.lisp
M books/projects/x86isa/machine/cert.acl2
M books/projects/x86isa/machine/environment-and-syscalls-raw.lsp
M books/projects/x86isa/machine/other-non-det-raw.lsp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/register-readers-and-writers-raw.lsp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/tools/execution/top.lisp
M books/std/strings/bin-digit-char-listp.lisp
M books/std/strings/dec-digit-char-listp.lisp
M books/std/strings/hex-digit-char-listp.lisp
M books/std/strings/oct-digit-char-listp.lisp
M books/std/util/defaggregate.lisp
M books/std/util/defprojection.lisp
M books/std/util/defrule.lisp
M books/std/util/tests/defaggregate.lisp
M books/system/doc/acl2-doc.lisp
A books/tools/eval-events-from-file-doc.lisp
A books/tools/eval-events-from-file-test-data.lsp
A books/tools/eval-events-from-file-test.lisp
A books/tools/eval-events-from-file.lisp
M books/tools/top.lisp
M books/tools/with-supporters-doc.lisp
M books/tools/with-supporters.lisp
M books/xdoc/display.lisp
M defthm.lisp
M defuns.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp
M other-events.lisp
M proof-builder-b.lisp
Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/master' into testing-acl2s
Commit: f1215b5012c66da463b258e2e2eb2b6e3427af68
https://github.com/acl2/acl2/commit/f1215b5012c66da463b258e2e2eb2b6e3427af68
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/utilities/add-attributes.lisp
Log Message:
-----------
[C2C] Fix add-section-attr bug
Declarations with empty initializer declarator lists were being
erroneously dropped. Extended a test case to test for the desired
behavior.
Commit: a5d7e5ae37d1c5851bf9d22dc07df64d5c38ef4b
https://github.com/acl2/acl2/commit/a5d7e5ae37d1c5851bf9d22dc07df64d5c38ef4b
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/uid.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
Log Message:
-----------
Update copyright years
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
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve preprocessor implementation.
Make the maximum macro reach part of the stobj.
Commit: bc13f6577e0cebed432ea0ce8929603d2e542dde
https://github.com/acl2/acl2/commit/bc13f6577e0cebed432ea0ce8929603d2e542dde
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/utilities/add-attributes.lisp
Log Message:
-----------
Merge commit 'f1215b5012c66da463b258e2e2eb2b6e3427af68' into HEAD
https://github.com/acl2/acl2/commit/9983ebdf1a551b55f3b91a5234f31cdf51223ade
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-thy-alt.lisp
Changed paths:
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:
-----------
Small updates to eval_poly example of hol-in-acl2 project
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
Changed paths:
Log Message:
-----------
[C$] Update some doc.
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
Changed paths:
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
Changed paths:
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
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/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/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/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/41dd9ee939c5...e8022dad2758
Reply all
Reply to author
Forward
0 new messages