Branch: refs/heads/testing-user-01
Commit: 98276b7dbea64872a91025c5a8513adaa4fc0528
https://github.com/acl2/acl2/commit/98276b7dbea64872a91025c5a8513adaa4fc0528
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Improve/update some doc.
In general, the AST documentation should refer to the ABNF grammar, rather than
the grammar in the standard(s). This commit edits the top doc of ASTs
accordingly, but the rest of the file will be updated as we go.
Commit: 02b496586b4bdfc603dc99afaaef22f5e5fd0ed1
https://github.com/acl2/acl2/commit/02b496586b4bdfc603dc99afaaef22f5e5fd0ed1
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
Log Message:
-----------
[C$] Extend data structure for preprocessing numbers.
Include (indications of) optional single quotes, to accommodate C23.
Commit: 64d5f8c6042de1276e714663957c9400144daab6
https://github.com/acl2/acl2/commit/64d5f8c6042de1276e714663957c9400144daab6
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/hash-conditional-evaluation.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/token-concatenation.lisp
Log Message:
-----------
[C$] Add explicit fields in some pnumber constructors.
Commit: e00d4db1b78b437f2002b06c68aa388d774b6cb7
https://github.com/acl2/acl2/commit/e00d4db1b78b437f2002b06c68aa388d774b6cb7
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Improve a function name.
Commit: 81ca700810aa9ca6b70a80abfa6e33ca6ca1abcf
https://github.com/acl2/acl2/commit/81ca700810aa9ca6b70a80abfa6e33ca6ca1abcf
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/compilation-db.lisp
A books/kestrel/c/syntax/evaluation.lisp
M books/kestrel/c/syntax/infer-ienv.lisp
M books/kestrel/c/syntax/output-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/tests/compilation-db.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/tests/preprocess-file.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/reader.lisp
M books/kestrel/c/syntax/top.lisp
Log Message:
-----------
[C$] Add support for basic constant evaluation.
The symbol 'value is no longer exported from the ACL2 package. This
commit therefore features a number of incidental changes, where the
acl2::value function had to be explicitly prefixed by the acl2 package.
Commit: 006bea42cf7c1f777a5d187961219d113bda89b1
https://github.com/acl2/acl2/commit/006bea42cf7c1f777a5d187961219d113bda89b1
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Make valid-dec/oct/hex-const delegate to dec/oct/hex-const->value.
Move the canonical implementation to abstract-syntax-operations,
with documentation. The validator's valid-dec/oct/hex-const now
simply calls dec/oct/hex-const->value.
Co-Authored-By: Claude Sonnet 4.6 <
nor...@anthropic.com>
Commit: 4ab7e1957144fd9ad8cfcd13e0ba92f743bfff22
https://github.com/acl2/acl2/commit/4ab7e1957144fd9ad8cfcd13e0ba92f743bfff22
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/evaluation.lisp
Log Message:
-----------
[C$] Incorporate Alessandro Coglio's suggestions
On PR 1931.
Commit: 31e0c0e5edbd98545950481921e190dc98fb45c7
https://github.com/acl2/acl2/commit/31e0c0e5edbd98545950481921e190dc98fb45c7
Author: Grant Jurgensen <
gr...@jurgensen.dev>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/evaluation.lisp
Log Message:
-----------
[C$] Fix XDOC links.
Commit: a12a8ed45d3bbaf3e57950fbaadf37eaed5bb81f
https://github.com/acl2/acl2/commit/a12a8ed45d3bbaf3e57950fbaadf37eaed5bb81f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Improve a function name.
Commit: 4bcb466f78827422c0f7a2e9ef095bde6e14c049
https://github.com/acl2/acl2/commit/4bcb466f78827422c0f7a2e9ef095bde6e14c049
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
Log Message:
-----------
[C$] Extend the preprocessor lexer.
Extend the lexing of preprocessing numbers to allow the optional single quotes
when the standard is C23.
Commit: 0a67ebbcab525f2e81c617e4b1c08c7ac6bbbd77
https://github.com/acl2/acl2/commit/0a67ebbcab525f2e81c617e4b1c08c7ac6bbbd77
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/hash-conditional-evaluation.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/token-concatenation.lisp
Log Message:
-----------
Merge.
Commit: 34614fd7528ed3905b2f682a96e9f55b24701afc
https://github.com/acl2/acl2/commit/34614fd7528ed3905b2f682a96e9f55b24701afc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2026-04-14 (Tue, 14 Apr 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/compilation-db.lisp
A books/kestrel/c/syntax/evaluation.lisp
M books/kestrel/c/syntax/infer-ienv.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/output-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/tests/compilation-db.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/tests/preprocess-file.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/reader.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
Merge.
Compare:
https://github.com/acl2/acl2/compare/db2285689bff...34614fd7528e