[acl2/acl2] c4cd40: [C$] Remove some unnecessary hints.

0 views
Skip to first unread message

Alessandro Coglio

unread,
Dec 16, 2025, 11:10:37 PM (4 days ago) Dec 16
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: c4cd40f1b0decacf2a891dbc13bf3c6ab67b731b
https://github.com/acl2/acl2/commit/c4cd40f1b0decacf2a891dbc13bf3c6ab67b731b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Remove some unnecessary hints.


Commit: c6663108855825388fac5dd8e9481ad00dba4540
https://github.com/acl2/acl2/commit/c6663108855825388fac5dd8e9481ad00dba4540
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Remove some unnecessary hints, using library theorems.


Commit: 53831c8b283d401338063cd2490a9cd9c4ae9a48
https://github.com/acl2/acl2/commit/53831c8b283d401338063cd2490a9cd9c4ae9a48
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Advance preprocessor.

Add code to unread (i.e. put back) tokens.

Add and call (stub) function to preprocess text lines.


Commit: 9a97d72e365bfb4a28e90bac96858699b5b9fd9d
https://github.com/acl2/acl2/commit/9a97d72e365bfb4a28e90bac96858699b5b9fd9d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Add some clarifying doc.


Commit: b1954183a6527cb0bad4fd2bac4dc280a838f8cc
https://github.com/acl2/acl2/commit/b1954183a6527cb0bad4fd2bac4dc280a838f8cc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Improve preprocessor.

Pass whitespace and comments before hashes to the dedicated preprocessing
functions.


Commit: 4ffd00409a55b7bf364cd84f0a66ae314eb79fb1
https://github.com/acl2/acl2/commit/4ffd00409a55b7bf364cd84f0a66ae314eb79fb1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/compilation-db.lisp
M books/kestrel/c/syntax/lexer.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-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp

Log Message:
-----------
[C$] Make terminology in doc more consistent.

In documentation (not necessarily code), we consistently say 'white space'
(instead of 'whitespace') and 'new line' (instead of 'newline'), as in the C
standard. We hyphenate when the role is attributive (e.g. 'new-line character').


Commit: 73f1122c5aafa43d5b30389435a809d25f7117a9
https://github.com/acl2/acl2/commit/73f1122c5aafa43d5b30389435a809d25f7117a9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/grammar/all.abnf

Log Message:
-----------
[C$] Tweak some doc comments in the grammar.


Commit: f93e46c2176b843fe1ca2ed0ffa8211336660b4e
https://github.com/acl2/acl2/commit/f93e46c2176b843fe1ca2ed0ffa8211336660b4e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Shorten some variable names.


Commit: e5e392bbec251d4e4375006be9b20c6262ac758a
https://github.com/acl2/acl2/commit/e5e392bbec251d4e4375006be9b20c6262ac758a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Advance preprocessor.

Add support for the null directive.


Commit: e29e1b18be210898a76672c68be4c41e77ae607e
https://github.com/acl2/acl2/commit/e29e1b18be210898a76672c68be4c41e77ae607e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
A books/kestrel/c/syntax/tests/empty.c
A books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/whitespace.c

Log Message:
-----------
[C$] Start adding preprocessor tests.


Commit: d43af4887708304168d0a32f682b119152ebfa3b
https://github.com/acl2/acl2/commit/d43af4887708304168d0a32f682b119152ebfa3b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/grammar/all.abnf

Log Message:
-----------
[C$] Make a grammar rule more precise.


Commit: aa2455c5b48d6099dd19897b17edb26fc38778de
https://github.com/acl2/acl2/commit/aa2455c5b48d6099dd19897b17edb26fc38778de
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Fix bug in preprocessor uncovered by testing.

We need to check for new lines and line comments.


Commit: 9b76c92bf78345a38633c6bd5d6c90ded083230f
https://github.com/acl2/acl2/commit/9b76c92bf78345a38633c6bd5d6c90ded083230f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/tests/preprocessor.lisp
M books/kestrel/c/syntax/tests/whitespace.c

Log Message:
-----------
[C$] Slightly extend a preprocessor test.


Commit: 9f58f8dae3c5ec9ae93af18c3012715e6104c0e9
https://github.com/acl2/acl2/commit/9f58f8dae3c5ec9ae93af18c3012715e6104c0e9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp

Log Message:
-----------
[C$] Improve preprocessor lexer.

Keep track of the exact new lines that terminate line comments, so they can be
printed out properly after preprocessing.


Commit: c8ad27551a6ad3d902417761703ebe38b0bab5a3
https://github.com/acl2/acl2/commit/c8ad27551a6ad3d902417761703ebe38b0bab5a3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
A books/kestrel/c/syntax/tests/comments.c
M books/kestrel/c/syntax/tests/preprocessor.lisp

Log Message:
-----------
[C$] Add a preprocessor test.


Commit: b73b7b2173d855e80fe2529c20889be7989aa6ad
https://github.com/acl2/acl2/commit/b73b7b2173d855e80fe2529c20889be7989aa6ad
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Improve preprocessor.

Handle null directive more uniformly when terminated by line comment.


Commit: 357b139c8863a7d242ba9098787c6f3f14ca49ce
https://github.com/acl2/acl2/commit/357b139c8863a7d242ba9098787c6f3f14ca49ce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/tests/preprocessor.lisp

Log Message:
-----------
[C$] Add preprocessor tests for null directives.


Commit: c338a7a9786c9b04a5fdfb81645bf225ec48df32
https://github.com/acl2/acl2/commit/c338a7a9786c9b04a5fdfb81645bf225ec48df32
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/preprocessor-messages.lisp

Log Message:
-----------
[C$] Improve error messages.

Refine the mapping of identifiers to messages in the preprocessor. This is
motivated by the fact that we need to distinguish different identifiers as names
of directives.


Commit: 72b7d1ef6aaae4f153117ab2e1c9bdcea5bb5f0e
https://github.com/acl2/acl2/commit/72b7d1ef6aaae4f153117ab2e1c9bdcea5bb5f0e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Advance preprocessor.

Start fleshing out the handling of the different directives.


Commit: 4e1bb9edd8c0915ba2022471367e7a9957201598
https://github.com/acl2/acl2/commit/4e1bb9edd8c0915ba2022471367e7a9957201598
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast.lisp
M books/kestrel/c/transformation/tests/simpadd0/file-scope.lisp
M books/kestrel/c/transformation/tests/simpadd0/global.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/unary.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-fn-when/split-fn-when.lisp
M books/kestrel/c/transformation/tests/split-fn/split-fn.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
M books/kestrel/c/transformation/tests/wrap-fn/wrap-fn.lisp

Log Message:
-----------
[C$] Improve printer.

Print a blank line between external declarations, as the documentation of the
printing function already said in fact (but apparently the code failed to
fulfill that).


Commit: 14bb5557cece91b2fb961ef5e07413bc3bf788bb
https://github.com/acl2/acl2/commit/14bb5557cece91b2fb961ef5e07413bc3bf788bb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Simplify preprocessor.

Discard white space and comments preceding directives.


Commit: 3c2c5578561c0d40a2c797e180aa09f6f3256111
https://github.com/acl2/acl2/commit/3c2c5578561c0d40a2c797e180aa09f6f3256111
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

Log Message:
-----------
[C$] Advance preprocessor.

Start handling `#include` directives.


Commit: 10d7f1bfc882b7e7ce06b5a62af67f299cba5026
https://github.com/acl2/acl2/commit/10d7f1bfc882b7e7ce06b5a62af67f299cba5026
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.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

Log Message:
-----------
[C$] Extend AST of translation units.

Add an optional line comment at the beginning of the translation unit.

Extend the printer to handle that.


Commit: 3da8ff662ea5a387d0e02e1f469e9431d6efd886
https://github.com/acl2/acl2/commit/3da8ff662ea5a387d0e02e1f469e9431d6efd886
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-multi.lisp
M books/kestrel/c/transformation/tests/simpadd0/bin.lisp
M books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast.lisp
M books/kestrel/c/transformation/tests/simpadd0/constant.lisp
M books/kestrel/c/transformation/tests/simpadd0/decl.lisp
M books/kestrel/c/transformation/tests/simpadd0/dowhile.lisp
M books/kestrel/c/transformation/tests/simpadd0/file-scope.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/global.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-const.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-param.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-return.lisp
M books/kestrel/c/transformation/tests/simpadd0/noninteger.lisp
M books/kestrel/c/transformation/tests/simpadd0/paren.lisp
M books/kestrel/c/transformation/tests/simpadd0/pure-expr-stmt.lisp
M books/kestrel/c/transformation/tests/simpadd0/return-void.lisp
M books/kestrel/c/transformation/tests/simpadd0/stmt-null.lisp
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/unary.lisp
M books/kestrel/c/transformation/tests/simpadd0/variable.lisp
M books/kestrel/c/transformation/tests/simpadd0/while.lisp

Log Message:
-----------
[C2C] Improve `simpadd0`.

Generate a comment at the beginning of each generate file saying that the file
is generated by this transformation.

Adjust test expectations.


Commit: 734f40d6222a9cb2f65bd1cd55683b2f8b1d887a
https://github.com/acl2/acl2/commit/734f40d6222a9cb2f65bd1cd55683b2f8b1d887a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

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

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


Commit: 086abc06614b5855e0cc9ed2c7e4ac066c8fb4cc
https://github.com/acl2/acl2/commit/086abc06614b5855e0cc9ed2c7e4ac066c8fb4cc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.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
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-multi.lisp
M books/kestrel/c/transformation/tests/simpadd0/bin.lisp
M books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast.lisp
M books/kestrel/c/transformation/tests/simpadd0/constant.lisp
M books/kestrel/c/transformation/tests/simpadd0/decl.lisp
M books/kestrel/c/transformation/tests/simpadd0/dowhile.lisp
M books/kestrel/c/transformation/tests/simpadd0/file-scope.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/global.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-const.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-param.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-return.lisp
M books/kestrel/c/transformation/tests/simpadd0/noninteger.lisp
M books/kestrel/c/transformation/tests/simpadd0/paren.lisp
M books/kestrel/c/transformation/tests/simpadd0/pure-expr-stmt.lisp
M books/kestrel/c/transformation/tests/simpadd0/return-void.lisp
M books/kestrel/c/transformation/tests/simpadd0/stmt-null.lisp
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/unary.lisp
M books/kestrel/c/transformation/tests/simpadd0/variable.lisp
M books/kestrel/c/transformation/tests/simpadd0/while.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-fn-when/split-fn-when.lisp
M books/kestrel/c/transformation/tests/split-fn/split-fn.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
M books/kestrel/c/transformation/tests/wrap-fn/wrap-fn.lisp

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


Compare: https://github.com/acl2/acl2/compare/98ebcf0448af...086abc06614b

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

Alessandro Coglio

unread,
Dec 17, 2025, 2:07:29 AM (4 days ago) Dec 17
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: 1b72d7353a49bb447c40840f8dff101649556831
https://github.com/acl2/acl2/commit/1b72d7353a49bb447c40840f8dff101649556831
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)

Changed paths:
A books/kestrel/c/syntax/tests/null-directive.c

Log Message:
-----------
[C$] Add forgotten test file.


Compare: https://github.com/acl2/acl2/compare/98ebcf0448af...1b72d7353a49

Alessandro Coglio

unread,
Dec 17, 2025, 2:08:38 AM (4 days ago) Dec 17
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Dec 17, 2025, 12:03:05 PM (4 days ago) Dec 17
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Reply all
Reply to author
Forward
0 new messages