[acl2/acl2] fb37f8: [C$] Reorder a `ppstate` stobj component.
0 views
Skip to first unread message
Alessandro Coglio
Jan 14, 2026, 12:23:09 AM (7 days ago) Jan 14
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: fb37f87d245e23fb3c7db5db3ba4d1e827dbf1f0
https://github.com/acl2/acl2/commit/fb37f87d245e23fb3c7db5db3ba4d1e827dbf1f0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Reorder a `ppstate` stobj component.
Commit: fc1159fa79edfa00dd3c4b1ce00508f08db4f70b
https://github.com/acl2/acl2/commit/fc1159fa79edfa00dd3c4b1ce00508f08db4f70b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Avoid calling a fixer.
Commit: 1d36416cd2710d2047cf73226a5deb0f62157923
https://github.com/acl2/acl2/commit/1d36416cd2710d2047cf73226a5deb0f62157923
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add and start using group endings.
Commit: dccdbd2fbac3e64786a418f972a46ee8d0656dbf
https://github.com/acl2/acl2/commit/dccdbd2fbac3e64786a418f972a46ee8d0656dbf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Handle top-level groups not ending with EOF.
Commit: 8cd6310feaa67d2684117f52fec015f05cc89691
https://github.com/acl2/acl2/commit/8cd6310feaa67d2684117f52fec015f05cc89691
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve handling of preprocessing groups.
Commit: 1f2288663371a7327ff9b86848ae9cd08ad18eaa
https://github.com/acl2/acl2/commit/1f2288663371a7327ff9b86848ae9cd08ad18eaa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add and explain macro replacement modes.
Commit: c6d873928ba1dfd1985a1bb6d8b9422f0cf2ee03
https://github.com/acl2/acl2/commit/c6d873928ba1dfd1985a1bb6d8b9422f0cf2ee03
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Tweaks.
Commit: 8dd83d3fb86b9ee8b52c703b9a4e446366a5c195
https://github.com/acl2/acl2/commit/8dd83d3fb86b9ee8b52c703b9a4e446366a5c195
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Fold `pproc-directive` into `pproc-?-group-part`, also because directives are
actually lines, while the code in `pproc-directive` may proceess more or less
than a directive in some cases.
Handle end of groups with `#elif`, `#else`, and `#endif`.
Commit: ab0dfa46e8ac8bc9f6aecac448b4795cf8a98b51
https://github.com/acl2/acl2/commit/ab0dfa46e8ac8bc9f6aecac448b4795cf8a98b51
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Expand some doc.
Commit: 9696875e9927a3ea15c82906904614d0df6e1371
https://github.com/acl2/acl2/commit/9696875e9927a3ea15c82906904614d0df6e1371
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Abbreviate a function name.
Commit: ff0cbbcca6c123565b1fa5abfe05e8a9ab2c1455
https://github.com/acl2/acl2/commit/ff0cbbcca6c123565b1fa5abfe05e8a9ab2c1455
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Streamline some code.
The functions dispatched to by `pproc-?-group-part` would always return `nil` as
group ending, so they should not return it explicitly.
Commit: c1659e946a5d6d5d4add092a802a711b6d0c2520
https://github.com/acl2/acl2/commit/c1659e946a5d6d5d4add092a802a711b6d0c2520
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
Log Message:
-----------
[C$] Improve some function names.
Commit: 3c1c03207282d6fb030fe607d8c2afc4d6a4d790
https://github.com/acl2/acl2/commit/3c1c03207282d6fb030fe607d8c2afc4d6a4d790
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Reorder code within a file.
Commit: ecd685902b0397989286219490a6e839f0351491
https://github.com/acl2/acl2/commit/ecd685902b0397989286219490a6e839f0351491
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Reorder a function within a file.
Commit: a6e5a1ffc73bc661a073c8869366c73b732c6610
https://github.com/acl2/acl2/commit/a6e5a1ffc73bc661a073c8869366c73b732c6610
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add stub for handling `#define` directives.
Commit: 554436401b4a4483fe1c46db91b0a114b360f45c
https://github.com/acl2/acl2/commit/554436401b4a4483fe1c46db91b0a114b360f45c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Rename a function.
Commit: 9ef763f4c0fc1b6633530c924460d766c2380326
https://github.com/acl2/acl2/commit/9ef763f4c0fc1b6633530c924460d766c2380326
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Update some doc.
Commit: 80a061429e028e6061865f5eea3aee3e4a9930dd
https://github.com/acl2/acl2/commit/80a061429e028e6061865f5eea3aee3e4a9930dd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Expand some doc.
Commit: 7a65fcf1910e34bd717bfe59200527c98e1c4a68
https://github.com/acl2/acl2/commit/7a65fcf1910e34bd717bfe59200527c98e1c4a68
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Remove function most likely not needed.
Commit: b39876b3c098003e7c1473d6f854b6e9cc48380e
https://github.com/acl2/acl2/commit/b39876b3c098003e7c1473d6f854b6e9cc48380e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Split a function into two variants.
This avoids passing the `headerp` flag, which is `nil` most of the time. For the
one case in which it is `t`, we have a more clearly named function.
Commit: fe85f6b33067ecfbe0b66004125056af6df31217
https://github.com/acl2/acl2/commit/fe85f6b33067ecfbe0b66004125056af6df31217
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Inline some preprocessor stobj functions.
Commit: 38fd1eff372914d380ae01b26c6741e5eed491ed
https://github.com/acl2/acl2/commit/38fd1eff372914d380ae01b26c6741e5eed491ed
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Make some return theorems unconditional.
Add some fixing theorems.
Commit: 65e2097b66ae7fa230e26c60f10142ce61b59b82
https://github.com/acl2/acl2/commit/65e2097b66ae7fa230e26c60f10142ce61b59b82
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Add a theorem.
Commit: 868ac45363e2620a6a2ce8ab345d107c47743542
https://github.com/acl2/acl2/commit/868ac45363e2620a6a2ce8ab345d107c47743542
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Extend a theorem.
Commit: 5dde43bbb4eb3c921634a909f3851726bea7a6ad
https://github.com/acl2/acl2/commit/5dde43bbb4eb3c921634a909f3851726bea7a6ad
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C$] Disable a theorem.
Commit: e3d6f158d68db295805c90cd906878f44ce60589
https://github.com/acl2/acl2/commit/e3d6f158d68db295805c90cd906878f44ce60589
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/b16e9d458228...e3d6f158d68d
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: fb37f87d245e23fb3c7db5db3ba4d1e827dbf1f0
https://github.com/acl2/acl2/commit/fb37f87d245e23fb3c7db5db3ba4d1e827dbf1f0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Reorder a `ppstate` stobj component.
Commit: fc1159fa79edfa00dd3c4b1ce00508f08db4f70b
https://github.com/acl2/acl2/commit/fc1159fa79edfa00dd3c4b1ce00508f08db4f70b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Avoid calling a fixer.
Commit: 1d36416cd2710d2047cf73226a5deb0f62157923
https://github.com/acl2/acl2/commit/1d36416cd2710d2047cf73226a5deb0f62157923
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add and start using group endings.
Commit: dccdbd2fbac3e64786a418f972a46ee8d0656dbf
https://github.com/acl2/acl2/commit/dccdbd2fbac3e64786a418f972a46ee8d0656dbf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Handle top-level groups not ending with EOF.
Commit: 8cd6310feaa67d2684117f52fec015f05cc89691
https://github.com/acl2/acl2/commit/8cd6310feaa67d2684117f52fec015f05cc89691
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve handling of preprocessing groups.
Commit: 1f2288663371a7327ff9b86848ae9cd08ad18eaa
https://github.com/acl2/acl2/commit/1f2288663371a7327ff9b86848ae9cd08ad18eaa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add and explain macro replacement modes.
Commit: c6d873928ba1dfd1985a1bb6d8b9422f0cf2ee03
https://github.com/acl2/acl2/commit/c6d873928ba1dfd1985a1bb6d8b9422f0cf2ee03
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Tweaks.
Commit: 8dd83d3fb86b9ee8b52c703b9a4e446366a5c195
https://github.com/acl2/acl2/commit/8dd83d3fb86b9ee8b52c703b9a4e446366a5c195
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Fold `pproc-directive` into `pproc-?-group-part`, also because directives are
actually lines, while the code in `pproc-directive` may proceess more or less
than a directive in some cases.
Handle end of groups with `#elif`, `#else`, and `#endif`.
Commit: ab0dfa46e8ac8bc9f6aecac448b4795cf8a98b51
https://github.com/acl2/acl2/commit/ab0dfa46e8ac8bc9f6aecac448b4795cf8a98b51
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Expand some doc.
Commit: 9696875e9927a3ea15c82906904614d0df6e1371
https://github.com/acl2/acl2/commit/9696875e9927a3ea15c82906904614d0df6e1371
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Abbreviate a function name.
Commit: ff0cbbcca6c123565b1fa5abfe05e8a9ab2c1455
https://github.com/acl2/acl2/commit/ff0cbbcca6c123565b1fa5abfe05e8a9ab2c1455
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Streamline some code.
The functions dispatched to by `pproc-?-group-part` would always return `nil` as
group ending, so they should not return it explicitly.
Commit: c1659e946a5d6d5d4add092a802a711b6d0c2520
https://github.com/acl2/acl2/commit/c1659e946a5d6d5d4add092a802a711b6d0c2520
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
Log Message:
-----------
[C$] Improve some function names.
Commit: 3c1c03207282d6fb030fe607d8c2afc4d6a4d790
https://github.com/acl2/acl2/commit/3c1c03207282d6fb030fe607d8c2afc4d6a4d790
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Reorder code within a file.
Commit: ecd685902b0397989286219490a6e839f0351491
https://github.com/acl2/acl2/commit/ecd685902b0397989286219490a6e839f0351491
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Reorder a function within a file.
Commit: a6e5a1ffc73bc661a073c8869366c73b732c6610
https://github.com/acl2/acl2/commit/a6e5a1ffc73bc661a073c8869366c73b732c6610
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add stub for handling `#define` directives.
Commit: 554436401b4a4483fe1c46db91b0a114b360f45c
https://github.com/acl2/acl2/commit/554436401b4a4483fe1c46db91b0a114b360f45c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Rename a function.
Commit: 9ef763f4c0fc1b6633530c924460d766c2380326
https://github.com/acl2/acl2/commit/9ef763f4c0fc1b6633530c924460d766c2380326
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Update some doc.
Commit: 80a061429e028e6061865f5eea3aee3e4a9930dd
https://github.com/acl2/acl2/commit/80a061429e028e6061865f5eea3aee3e4a9930dd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Expand some doc.
Commit: 7a65fcf1910e34bd717bfe59200527c98e1c4a68
https://github.com/acl2/acl2/commit/7a65fcf1910e34bd717bfe59200527c98e1c4a68
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Remove function most likely not needed.
Commit: b39876b3c098003e7c1473d6f854b6e9cc48380e
https://github.com/acl2/acl2/commit/b39876b3c098003e7c1473d6f854b6e9cc48380e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Split a function into two variants.
This avoids passing the `headerp` flag, which is `nil` most of the time. For the
one case in which it is `t`, we have a more clearly named function.
Commit: fe85f6b33067ecfbe0b66004125056af6df31217
https://github.com/acl2/acl2/commit/fe85f6b33067ecfbe0b66004125056af6df31217
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Inline some preprocessor stobj functions.
Commit: 38fd1eff372914d380ae01b26c6741e5eed491ed
https://github.com/acl2/acl2/commit/38fd1eff372914d380ae01b26c6741e5eed491ed
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Make some return theorems unconditional.
Add some fixing theorems.
Commit: 65e2097b66ae7fa230e26c60f10142ce61b59b82
https://github.com/acl2/acl2/commit/65e2097b66ae7fa230e26c60f10142ce61b59b82
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Add a theorem.
Commit: 868ac45363e2620a6a2ce8ab345d107c47743542
https://github.com/acl2/acl2/commit/868ac45363e2620a6a2ce8ab345d107c47743542
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Extend a theorem.
Commit: 5dde43bbb4eb3c921634a909f3851726bea7a6ad
https://github.com/acl2/acl2/commit/5dde43bbb4eb3c921634a909f3851726bea7a6ad
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C$] Disable a theorem.
Commit: e3d6f158d68db295805c90cd906878f44ce60589
https://github.com/acl2/acl2/commit/e3d6f158d68db295805c90cd906878f44ce60589
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/b16e9d458228...e3d6f158d68d
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Jan 14, 2026, 2:15:50 AM (7 days ago) Jan 14
to acl2-...@googlegroups.com
Branch: refs/heads/master
Alessandro Coglio
Jan 14, 2026, 2:16:38 AM (7 days ago) Jan 14
to acl2-...@googlegroups.com
Branch: refs/heads/testing
acl2buildserver
Jan 15, 2026, 12:36:44 PM (6 days ago) Jan 15
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Commit: 7771ae15a4a4f8ea45e467e348df9c9a2d0809a5
https://github.com/acl2/acl2/commit/7771ae15a4a4f8ea45e467e348df9c9a2d0809a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Improve a fixtype field name.
Commit: 7606afe535a235d3e88ca8ceb9a26718173aa7b5
https://github.com/acl2/acl2/commit/7606afe535a235d3e88ca8ceb9a26718173aa7b5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Extend information about a function-like macro.
Although this is redundant information, it seems better to compute it once.
Commit: c9fc77dc245c121cad7dc1e58312fcb3f3279d13
https://github.com/acl2/acl2/commit/c9fc77dc245c121cad7dc1e58312fcb3f3279d13
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Add a predicate on preprocessing lexemes.
Commit: 7c4258f83fe66ef613043b3ecdf368cb7a5ce3b6
https://github.com/acl2/acl2/commit/7c4258f83fe66ef613043b3ecdf368cb7a5ce3b6
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/doc/relnotes.lisp
M books/projects/hol-in-acl2/README
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
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
Log Message:
-----------
Updated hol-in-acl2 library with help from Konrad Slind. Added eval-events-from-file.
The hol-in-acl2 library is a bit cleaner now, in particular with the
addition of new utility zf::import-theory and files *.defhol generated
(by Konrad) using the hol-to-acl2 translator. Also added a new
utility; see :DOC eval-events-from-file.
Commit: f270dfb641705d84634069832cd119a99fe2796c
https://github.com/acl2/acl2/commit/f270dfb641705d84634069832cd119a99fe2796c
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
Log Message:
-----------
Fixed mix-up with depends-on directives
Commit: 78d52469f0fa82ff1423a404011e2b693d9ac73b
https://github.com/acl2/acl2/commit/78d52469f0fa82ff1423a404011e2b693d9ac73b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Add two theorems.
Commit: 644995e8dde2736cfe781c94f8b8b480b382b7e3
https://github.com/acl2/acl2/commit/644995e8dde2736cfe781c94f8b8b480b382b7e3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Add a predicate on lexemes.
Commit: debe7806338f2b23d2e29aac10e906bf47588692
https://github.com/acl2/acl2/commit/debe7806338f2b23d2e29aac10e906bf47588692
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add support for `#define` directives.
Only for preprocessing the directives themselves for now; still need to add
support for expanding them where/as needed.
Commit: f432338656d9f2d64efdc9039b34827d06029f5f
https://github.com/acl2/acl2/commit/f432338656d9f2d64efdc9039b34827d06029f5f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Add and use specialized testing macro.
Commit: 481aea193f3472396875dfc9e71b520bd0f42e92
https://github.com/acl2/acl2/commit/481aea193f3472396875dfc9e71b520bd0f42e92
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
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/macros.c
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Add several tests for `#define`.
Commit: 3e153beb24051b99ad3aad8897cd52d3d7830ff1
https://github.com/acl2/acl2/commit/3e153beb24051b99ad3aad8897cd52d3d7830ff1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/doc/relnotes.lisp
M books/projects/hol-in-acl2/README
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
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
Log Message:
-----------
Merge.
Commit: bdefdf557923e24cd1a9d0beec29daa861bdb67a
https://github.com/acl2/acl2/commit/bdefdf557923e24cd1a9d0beec29daa861bdb67a
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-01-15 (Thu, 15 Jan 2026)
Changed paths:
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/unguarded-defuns.lisp
M books/kestrel/axe/x86/tester-code-only.lisp
M books/kestrel/axe/x86/unroller-code-only.lisp
Log Message:
-----------
Merge commit '1684163590189f715c9873fd2188e509bcc1680d' into HEAD
Compare: https://github.com/acl2/acl2/compare/168416359018...bdefdf557923
https://github.com/acl2/acl2/commit/7771ae15a4a4f8ea45e467e348df9c9a2d0809a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
Commit: 7606afe535a235d3e88ca8ceb9a26718173aa7b5
https://github.com/acl2/acl2/commit/7606afe535a235d3e88ca8ceb9a26718173aa7b5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
Although this is redundant information, it seems better to compute it once.
Commit: c9fc77dc245c121cad7dc1e58312fcb3f3279d13
https://github.com/acl2/acl2/commit/c9fc77dc245c121cad7dc1e58312fcb3f3279d13
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
Commit: 7c4258f83fe66ef613043b3ecdf368cb7a5ce3b6
https://github.com/acl2/acl2/commit/7c4258f83fe66ef613043b3ecdf368cb7a5ce3b6
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/doc/relnotes.lisp
M books/projects/hol-in-acl2/README
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
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
Log Message:
-----------
Updated hol-in-acl2 library with help from Konrad Slind. Added eval-events-from-file.
The hol-in-acl2 library is a bit cleaner now, in particular with the
addition of new utility zf::import-theory and files *.defhol generated
(by Konrad) using the hol-to-acl2 translator. Also added a new
utility; see :DOC eval-events-from-file.
Commit: f270dfb641705d84634069832cd119a99fe2796c
https://github.com/acl2/acl2/commit/f270dfb641705d84634069832cd119a99fe2796c
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
Log Message:
-----------
Fixed mix-up with depends-on directives
Commit: 78d52469f0fa82ff1423a404011e2b693d9ac73b
https://github.com/acl2/acl2/commit/78d52469f0fa82ff1423a404011e2b693d9ac73b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Add two theorems.
Commit: 644995e8dde2736cfe781c94f8b8b480b382b7e3
https://github.com/acl2/acl2/commit/644995e8dde2736cfe781c94f8b8b480b382b7e3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
Commit: debe7806338f2b23d2e29aac10e906bf47588692
https://github.com/acl2/acl2/commit/debe7806338f2b23d2e29aac10e906bf47588692
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
Only for preprocessing the directives themselves for now; still need to add
support for expanding them where/as needed.
Commit: f432338656d9f2d64efdc9039b34827d06029f5f
https://github.com/acl2/acl2/commit/f432338656d9f2d64efdc9039b34827d06029f5f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Add and use specialized testing macro.
Commit: 481aea193f3472396875dfc9e71b520bd0f42e92
https://github.com/acl2/acl2/commit/481aea193f3472396875dfc9e71b520bd0f42e92
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
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/macros.c
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Add several tests for `#define`.
Commit: 3e153beb24051b99ad3aad8897cd52d3d7830ff1
https://github.com/acl2/acl2/commit/3e153beb24051b99ad3aad8897cd52d3d7830ff1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-14 (Wed, 14 Jan 2026)
Changed paths:
M books/doc/relnotes.lisp
M books/projects/hol-in-acl2/README
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
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
Log Message:
-----------
Merge.
Commit: bdefdf557923e24cd1a9d0beec29daa861bdb67a
https://github.com/acl2/acl2/commit/bdefdf557923e24cd1a9d0beec29daa861bdb67a
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-01-15 (Thu, 15 Jan 2026)
Changed paths:
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/unguarded-defuns.lisp
M books/kestrel/axe/x86/tester-code-only.lisp
M books/kestrel/axe/x86/unroller-code-only.lisp
Log Message:
-----------
Merge commit '1684163590189f715c9873fd2188e509bcc1680d' into HEAD
Compare: https://github.com/acl2/acl2/compare/168416359018...bdefdf557923
Reply all
Reply to author
Forward
0 new messages