[acl2/acl2] b255f5: [C$] Add file and topic for validation.

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: b255f51d927d23ccf48c554da2d058132daf8e30
https://github.com/acl2/acl2/commit/b255f51d927d23ccf48c554da2d058132daf8e30
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

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

Log Message:
-----------
[C$] Add file and topic for validation.

Put validator and validation information under this new topic.


Commit: 1ef881d9b7c928255889255210e5752905de8ff9
https://github.com/acl2/acl2/commit/1ef881d9b7c928255889255210e5752905de8ff9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
A books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp

Log Message:
-----------
[C$] Refactor parser code.

Put parser states into a separate file.


Commit: cf42df6b7fc4dab6b42bcc398bd0abe21b744335
https://github.com/acl2/acl2/commit/cf42df6b7fc4dab6b42bcc398bd0abe21b744335
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/parser-states.lisp

Log Message:
-----------
[C$] Move a macro to a file.


Commit: f42a037842615aeba11d70a0811260ba643f245f
https://github.com/acl2/acl2/commit/f42a037842615aeba11d70a0811260ba643f245f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/parser.lisp
A books/kestrel/c/syntax/reader.lisp

Log Message:
-----------
[C$] Put reader into separate new file.


Commit: fce5b2d4242329ed32afa547e0c25b8fd9d3ce6d
https://github.com/acl2/acl2/commit/fce5b2d4242329ed32afa547e0c25b8fd9d3ce6d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
A books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser.lisp

Log Message:
-----------
[C$] Move lexer into new separate file.


Commit: 7c81c86f34cb2f48d119d098e642ed100719d7b3
https://github.com/acl2/acl2/commit/7c81c86f34cb2f48d119d098e642ed100719d7b3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

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

Log Message:
-----------
[C$] Remove local theorems no longer needed.


Commit: 6de3fc272ab1da709930e118be0ff91ae509ed5b
https://github.com/acl2/acl2/commit/6de3fc272ab1da709930e118be0ff91ae509ed5b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

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

Log Message:
-----------
[C$] Remove redundant book inclusion.


Commit: 01d062622a06f0900b644e8790f19c9ee22c5d98
https://github.com/acl2/acl2/commit/01d062622a06f0900b644e8790f19c9ee22c5d98
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/parser-states.lisp

Log Message:
-----------
[C$] Simplify some book inclusions.


Commit: ccb22adf3e683dff28671df2ad80223919da5f7f
https://github.com/acl2/acl2/commit/ccb22adf3e683dff28671df2ad80223919da5f7f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

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

Log Message:
-----------
[C$] Simplify book inclusions.


Commit: 36e2aaeced7e189968636fec351dc1b16a5fc5e3
https://github.com/acl2/acl2/commit/36e2aaeced7e189968636fec351dc1b16a5fc5e3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

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

Log Message:
-----------
[C$] Simplify some book inclusions.


Commit: 6dbffcc639484e23706f40f27eea91e3a1a7dcfd
https://github.com/acl2/acl2/commit/6dbffcc639484e23706f40f27eea91e3a1a7dcfd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

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

Log Message:
-----------
[C$] Eliminate local theorem.


Commit: 18a8f901e63fdec79a8a93a4add1ff475ee29800
https://github.com/acl2/acl2/commit/18a8f901e63fdec79a8a93a4add1ff475ee29800
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

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

Log Message:
-----------
[C$] Use library and avoid local theorem.


Commit: 3960e6fd59abab4d5fc7408cabec53b46955d2c6
https://github.com/acl2/acl2/commit/3960e6fd59abab4d5fc7408cabec53b46955d2c6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

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

Log Message:
-----------
[C$] Use library to avoid local theorem.


Commit: 9db30f04121c56d1af3e711b3aa1574ae4b3aeb9
https://github.com/acl2/acl2/commit/9db30f04121c56d1af3e711b3aa1574ae4b3aeb9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/package.lsp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/simpadd0.lisp
A books/kestrel/c/transformation/tests/simpadd0/old/while.c
A books/kestrel/c/transformation/tests/simpadd0/while.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

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


Commit: 6ee695d0f4e89d1114125923256d509084d46d4a
https://github.com/acl2/acl2/commit/6ee695d0f4e89d1114125923256d509084d46d4a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
A books/kestrel/c/syntax/tests/lexer.lisp
A books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/parser.lisp
A books/kestrel/c/syntax/tests/reader.lisp

Log Message:
-----------
[C$] Split parser tests into files.


Compare: https://github.com/acl2/acl2/compare/ae8c229bb5d9...6ee695d0f4e8

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

[Alessandro Coglio]

Branch: refs/heads/master

[Alessandro Coglio]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel