[acl2/acl2] 2acfa7: [C$] Add fixtype for type validation information.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 2acfa75b050ce8499047d7ffb41b96a0fb5632d3
https://github.com/acl2/acl2/commit/2acfa75b050ce8499047d7ffb41b96a0fb5632d3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

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

Log Message:
-----------
[C$] Add fixtype for type validation information.

This will replace all the validation information fixtypes that are isomorphic to
this one.


Commit: 2f9f13e162e12e079c289f1140f19784d19d2d53
https://github.com/acl2/acl2/commit/2f9f13e162e12e079c289f1140f19784d19d2d53
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C$] Replace some specific validation information.


Commit: 4969c7aac415c38f46eb4a74d6006db2ccf90bbc
https://github.com/acl2/acl2/commit/4969c7aac415c38f46eb4a74d6006db2ccf90bbc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Replace some specific validation information.


Commit: 70f07dc04fe06ebf24184b42730c17f08fc5ec1a
https://github.com/acl2/acl2/commit/70f07dc04fe06ebf24184b42730c17f08fc5ec1a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Replace some specific validation information.


Commit: 6a04798c02585d00838598632744c9c04904297d
https://github.com/acl2/acl2/commit/6a04798c02585d00838598632744c9c04904297d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Replace some specific validation information.


Commit: 90f6e470fadd3660110b67b5894bfca7cf1e43e4
https://github.com/acl2/acl2/commit/90f6e470fadd3660110b67b5894bfca7cf1e43e4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C$] Replace some specific validation information.


Commit: 8c4386eb1951761d6acfcb0fa4b4add832589a0b
https://github.com/acl2/acl2/commit/8c4386eb1951761d6acfcb0fa4b4add832589a0b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp

Log Message:
-----------
[C$] Replace some specific validation information.


Commit: a3d7d0ffa599173748eee8073eb3c40ea333aab6
https://github.com/acl2/acl2/commit/a3d7d0ffa599173748eee8073eb3c40ea333aab6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split.lisp

Log Message:
-----------
[C$] Replace some specific validation information.


Commit: fc233b2258ddbabb4c96f96fe6f60f7a104d63f5
https://github.com/acl2/acl2/commit/fc233b2258ddbabb4c96f96fe6f60f7a104d63f5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

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

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


Commit: 8ce70c9a858aaa0a7144ebf3ba86231e66517370
https://github.com/acl2/acl2/commit/8ce70c9a858aaa0a7144ebf3ba86231e66517370
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

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

Log Message:
-----------
[C$] Add a fixtype for validation information.


Commit: 0be2dbecffb77b2a0647e09829643410b611e93e
https://github.com/acl2/acl2/commit/0be2dbecffb77b2a0647e09829643410b611e93e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

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

Log Message:
-----------
[C$] Move some code within file.


Commit: eeb7253a2b3ed92fdd0342ae5e6e33eb7339da61
https://github.com/acl2/acl2/commit/eeb7253a2b3ed92fdd0342ae5e6e33eb7339da61
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/package.lsp

Log Message:
-----------
[C] Import two symbols.


Commit: 98bff015cf2b8234c8df0a926e1bee40612d4021
https://github.com/acl2/acl2/commit/98bff015cf2b8234c8df0a926e1bee40612d4021
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split.lisp

Log Message:
-----------
[C$] Replace some specific validation information.


Commit: 9d4cb6df94caf62408fd3725a3332bc229fc6ca2
https://github.com/acl2/acl2/commit/9d4cb6df94caf62408fd3725a3332bc229fc6ca2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/struct-type-split.lisp

Log Message:
-----------
[C$] Replace some specific validation information.


Commit: 17743952975c04550a3a3d74f09e8b0e4f2ba847
https://github.com/acl2/acl2/commit/17743952975c04550a3a3d74f09e8b0e4f2ba847
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
[C$] Replace some specific validation information.


Commit: 4257bbff8806b20b8fc0510c4741d26dcba1e92b
https://github.com/acl2/acl2/commit/4257bbff8806b20b8fc0510c4741d26dcba1e92b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/examples/strcpy-safe-induction.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/proof-generation.lisp

Log Message:
-----------
[C$] Rename a fixtype.


Commit: 449fc81b52e30e018c5b1e4b2e3b3e9209438aa2
https://github.com/acl2/acl2/commit/449fc81b52e30e018c5b1e4b2e3b3e9209438aa2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp

Log Message:
-----------
[C$] Improve some names.


Commit: 35168d586e5cc350c1e653a72b3e20253a8b2a0a
https://github.com/acl2/acl2/commit/35168d586e5cc350c1e653a72b3e20253a8b2a0a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/package.lsp

Log Message:
-----------
[C] Import a symbol.


Commit: b3bde209de13765f53f6c77f70d0c95ebfd94d1f
https://github.com/acl2/acl2/commit/b3bde209de13765f53f6c77f70d0c95ebfd94d1f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/fty/top.lisp
A books/kestrel/fty/true-list-set.lisp

Log Message:
-----------
[FTY] Add a fixtype of sets of true lists.


Commit: 1e4ca5c435923ee81d805de57272044db2b527e7
https://github.com/acl2/acl2/commit/1e4ca5c435923ee81d805de57272044db2b527e7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

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

Log Message:
-----------
[C$] Improve some names.


Commit: 93d0f999e162e3401c44031b3b9dbc8ad4f68e1a
https://github.com/acl2/acl2/commit/93d0f999e162e3401c44031b3b9dbc8ad4f68e1a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
[C$] Improve some names.


Commit: 89a95aa5232447db1cc278228c040b8814cd6df7
https://github.com/acl2/acl2/commit/89a95aa5232447db1cc278228c040b8814cd6df7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-21 (Sun, 21 Jun 2026)

Changed paths:
M books/kestrel/c/package.lsp
M books/kestrel/fty/top.lisp
A books/kestrel/fty/true-list-set.lisp

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


Compare: https://github.com/acl2/acl2/compare/cc591f7be808...89a95aa52324

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

[Alessandro Coglio]

Branch: refs/heads/master

[Alessandro Coglio]

Branch: refs/heads/testing