[acl2/acl2] 1a962e: [C$] Refactor preprocessor testing code.
0 views
Skip to first unread message
Alessandro Coglio
Feb 4, 2026, 3:10:24 AM (7 days ago) Feb 4
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 1a962e59dd67932738eebb06460dc87d363d1fa8
https://github.com/acl2/acl2/commit/1a962e59dd67932738eebb06460dc87d363d1fa8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
A books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Refactor preprocessor testing code.
Put testing macros into a separate dedicated file.
Commit: 9da88706f2ab9a5a6dbc5bad13ad85afaf23831e
https://github.com/acl2/acl2/commit/9da88706f2ab9a5a6dbc5bad13ad85afaf23831e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/input-files.lisp
Log Message:
-----------
[C$] Move some code.
As agreed with Grant Jurgensen.
Commit: 5f5cf7792666fdfff3457c25bb41dea65c1fa139
https://github.com/acl2/acl2/commit/5f5cf7792666fdfff3457c25bb41dea65c1fa139
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
Log Message:
-----------
[C$] Reduce book inclusions.
Commit: 5faff7d6a50a55fae8106e7548d576161be1062e
https://github.com/acl2/acl2/commit/5faff7d6a50a55fae8106e7548d576161be1062e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
Log Message:
-----------
[C$] Generalize a preprocessor testing macro.
Commit: 0e116946214175aa763be3a3082e9b3d49a053ea
https://github.com/acl2/acl2/commit/0e116946214175aa763be3a3082e9b3d49a053ea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
Log Message:
-----------
[C$] Add two preprocessor testing macros.
Commit: 8d53216db898387aef721371a7469e8c75f40e02
https://github.com/acl2/acl2/commit/8d53216db898387aef721371a7469e8c75f40e02
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve handling of `#error` directive.
Pretty-print the lexemes that follow the `#error` part, otherwise it may not
be particularly readable.
Commit: 5dca2e360846614a7f090a7a5b199375baa29306
https://github.com/acl2/acl2/commit/5dca2e360846614a7f090a7a5b199375baa29306
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
Log Message:
-----------
[C$] Fix bug in preprocessor expression parser.
Forgot to put back the token when attempting to read a unary operator that turns
out not to be a unary operator.
Commit: 51803a634b2dd99df5a6166be00bcc0de8cfceda
https://github.com/acl2/acl2/commit/51803a634b2dd99df5a6166be00bcc0de8cfceda
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
A books/kestrel/c/syntax/tests/conditional.c
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Add some preprocessor tests.
Commit: b77db74695f80b77f558aa0a4cd8d6b4ffcdb166
https://github.com/acl2/acl2/commit/b77db74695f80b77f558aa0a4cd8d6b4ffcdb166
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
Log Message:
-----------
[C$] Add a type prescription rule.
Commit: 84966aff66f2096996c6b8e4bcc043f861995432
https://github.com/acl2/acl2/commit/84966aff66f2096996c6b8e4bcc043f861995432
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add support for `#warning` directive.
This is only allowed in C23 (not C17), or if GCC or Clang extensions are
enabled.
Commit: 0decde4122bacb73dfef86e3dc89625e8792a881
https://github.com/acl2/acl2/commit/0decde4122bacb73dfef86e3dc89625e8792a881
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
Log Message:
-----------
[C$] Extend some testing macros.
Commit: 1ff43e784b60b9c7844a0f42c57703c20f454a49
https://github.com/acl2/acl2/commit/1ff43e784b60b9c7844a0f42c57703c20f454a49
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
Log Message:
-----------
[C$] Add a few predefined macros for preprocessor.
Commit: 1f1dfecc49b138aaf52a180199bddfc2b9dbdb1e
https://github.com/acl2/acl2/commit/1f1dfecc49b138aaf52a180199bddfc2b9dbdb1e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
Log Message:
-----------
[C$] Reduce book inclusions.
Commit: 1c722fbe2246f0e6b4cbf428281d261bde93d345
https://github.com/acl2/acl2/commit/1c722fbe2246f0e6b4cbf428281d261bde93d345
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Fix skipping of empty line.
Commit: 48ec75d8d717f35daea0c87a81665e6163400a08
https://github.com/acl2/acl2/commit/48ec75d8d717f35daea0c87a81665e6163400a08
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/axe/translate-dag-to-stp.lisp
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/tests/output-files.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
A books/kestrel/c/transformation/add-section-attr-doc.lisp
A books/kestrel/c/transformation/add-section-attr.lisp
M books/kestrel/c/transformation/command-line/wrappers.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-all-gso.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
A books/kestrel/c/transformation/tests/add-section-attr/.gitignore
A books/kestrel/c/transformation/tests/add-section-attr/acl2-customization.lsp
A books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/cert.acl2
A books/kestrel/c/transformation/tests/add-section-attr/test1.c
A books/kestrel/c/transformation/tests/add-section-attr/test2.c
A books/kestrel/c/transformation/tests/add-section-attr/test3.c
M books/kestrel/c/transformation/top.lisp
A books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
A books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/utilities/top.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
M books/kestrel/fty/deffold-map-doc.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/utilities/run-json-command.lisp
A books/projects/hol-in-acl2/acl2/hpp-set.lisp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
Log Message:
-----------
Merge.
Commit: 7c7e62bba6ff7b00970aa8e1f6a1993e07f09d6a
https://github.com/acl2/acl2/commit/7c7e62bba6ff7b00970aa8e1f6a1993e07f09d6a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/std/util/defaggregate.lisp
M books/std/util/tests/defaggregate.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/bb9c654461a0...7c7e62bba6ff
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 1a962e59dd67932738eebb06460dc87d363d1fa8
https://github.com/acl2/acl2/commit/1a962e59dd67932738eebb06460dc87d363d1fa8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
A books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Refactor preprocessor testing code.
Put testing macros into a separate dedicated file.
Commit: 9da88706f2ab9a5a6dbc5bad13ad85afaf23831e
https://github.com/acl2/acl2/commit/9da88706f2ab9a5a6dbc5bad13ad85afaf23831e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/input-files.lisp
Log Message:
-----------
[C$] Move some code.
As agreed with Grant Jurgensen.
Commit: 5f5cf7792666fdfff3457c25bb41dea65c1fa139
https://github.com/acl2/acl2/commit/5f5cf7792666fdfff3457c25bb41dea65c1fa139
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
Log Message:
-----------
[C$] Reduce book inclusions.
Commit: 5faff7d6a50a55fae8106e7548d576161be1062e
https://github.com/acl2/acl2/commit/5faff7d6a50a55fae8106e7548d576161be1062e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
Log Message:
-----------
[C$] Generalize a preprocessor testing macro.
Commit: 0e116946214175aa763be3a3082e9b3d49a053ea
https://github.com/acl2/acl2/commit/0e116946214175aa763be3a3082e9b3d49a053ea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
Log Message:
-----------
[C$] Add two preprocessor testing macros.
Commit: 8d53216db898387aef721371a7469e8c75f40e02
https://github.com/acl2/acl2/commit/8d53216db898387aef721371a7469e8c75f40e02
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve handling of `#error` directive.
Pretty-print the lexemes that follow the `#error` part, otherwise it may not
be particularly readable.
Commit: 5dca2e360846614a7f090a7a5b199375baa29306
https://github.com/acl2/acl2/commit/5dca2e360846614a7f090a7a5b199375baa29306
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
Log Message:
-----------
[C$] Fix bug in preprocessor expression parser.
Forgot to put back the token when attempting to read a unary operator that turns
out not to be a unary operator.
Commit: 51803a634b2dd99df5a6166be00bcc0de8cfceda
https://github.com/acl2/acl2/commit/51803a634b2dd99df5a6166be00bcc0de8cfceda
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
A books/kestrel/c/syntax/tests/conditional.c
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Add some preprocessor tests.
Commit: b77db74695f80b77f558aa0a4cd8d6b4ffcdb166
https://github.com/acl2/acl2/commit/b77db74695f80b77f558aa0a4cd8d6b4ffcdb166
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
Log Message:
-----------
[C$] Add a type prescription rule.
Commit: 84966aff66f2096996c6b8e4bcc043f861995432
https://github.com/acl2/acl2/commit/84966aff66f2096996c6b8e4bcc043f861995432
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add support for `#warning` directive.
This is only allowed in C23 (not C17), or if GCC or Clang extensions are
enabled.
Commit: 0decde4122bacb73dfef86e3dc89625e8792a881
https://github.com/acl2/acl2/commit/0decde4122bacb73dfef86e3dc89625e8792a881
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
Log Message:
-----------
[C$] Extend some testing macros.
Commit: 1ff43e784b60b9c7844a0f42c57703c20f454a49
https://github.com/acl2/acl2/commit/1ff43e784b60b9c7844a0f42c57703c20f454a49
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
Log Message:
-----------
[C$] Add a few predefined macros for preprocessor.
Commit: 1f1dfecc49b138aaf52a180199bddfc2b9dbdb1e
https://github.com/acl2/acl2/commit/1f1dfecc49b138aaf52a180199bddfc2b9dbdb1e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
Log Message:
-----------
[C$] Reduce book inclusions.
Commit: 1c722fbe2246f0e6b4cbf428281d261bde93d345
https://github.com/acl2/acl2/commit/1c722fbe2246f0e6b4cbf428281d261bde93d345
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Fix skipping of empty line.
Commit: 48ec75d8d717f35daea0c87a81665e6163400a08
https://github.com/acl2/acl2/commit/48ec75d8d717f35daea0c87a81665e6163400a08
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/axe/translate-dag-to-stp.lisp
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/tests/output-files.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
A books/kestrel/c/transformation/add-section-attr-doc.lisp
A books/kestrel/c/transformation/add-section-attr.lisp
M books/kestrel/c/transformation/command-line/wrappers.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-all-gso.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
A books/kestrel/c/transformation/tests/add-section-attr/.gitignore
A books/kestrel/c/transformation/tests/add-section-attr/acl2-customization.lsp
A books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/cert.acl2
A books/kestrel/c/transformation/tests/add-section-attr/test1.c
A books/kestrel/c/transformation/tests/add-section-attr/test2.c
A books/kestrel/c/transformation/tests/add-section-attr/test3.c
M books/kestrel/c/transformation/top.lisp
A books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
A books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/utilities/top.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
M books/kestrel/fty/deffold-map-doc.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/utilities/run-json-command.lisp
A books/projects/hol-in-acl2/acl2/hpp-set.lisp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
Log Message:
-----------
Merge.
Commit: 7c7e62bba6ff7b00970aa8e1f6a1993e07f09d6a
https://github.com/acl2/acl2/commit/7c7e62bba6ff7b00970aa8e1f6a1993e07f09d6a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/std/util/defaggregate.lisp
M books/std/util/tests/defaggregate.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/bb9c654461a0...7c7e62bba6ff
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Feb 4, 2026, 3:11:36 AM (7 days ago) Feb 4
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Feb 5, 2026, 1:55:25 AM (6 days ago) Feb 5
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Commit: 73c417ec3457dc8be4974600e678cbddbfd63697
https://github.com/acl2/acl2/commit/73c417ec3457dc8be4974600e678cbddbfd63697
Author: Matt Kaufmann <matthew.j...@gmail.com>
Commit: 84d70e79290a0a817ccce18d56305869376bf480
https://github.com/acl2/acl2/commit/84d70e79290a0a817ccce18d56305869376bf480
Author: ACL2 Build Server <acl2bui...@gmail.com>
Log Message:
-----------
Merge commit '5bce3ca19bc16462c08aeea29ce5a10914e19bd0' into HEAD
Commit: bb9c654461a0824e008b52e154fde5424f79eca0
https://github.com/acl2/acl2/commit/bb9c654461a0824e008b52e154fde5424f79eca0
Author: ACL2 Build Server <acl2bui...@gmail.com>
Commit: 223141e65ea78a6131623aaaad4c20e187716b27
https://github.com/acl2/acl2/commit/223141e65ea78a6131623aaaad4c20e187716b27
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
A books/kestrel/arm/top.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/unroller.lisp
R books/kestrel/axe/x86/evaluator-x86.acl2
M books/kestrel/axe/x86/evaluator-x86.lisp
A books/kestrel/axe/x86/lifter-support.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/top.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/top.lisp
M books/kestrel/utilities/redundancy.lisp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
R books/kestrel/x86/x86-changes.acl2
M books/kestrel/x86/x86-changes.lisp
Log Message:
-----------
Merge commit 'a1674138cba2b2924f5563ebad7cf1eecd622d91' into HEAD
Commit: 1c31d98cf7eb8d8b5fd477dd5a153c46a7abda69
https://github.com/acl2/acl2/commit/1c31d98cf7eb8d8b5fd477dd5a153c46a7abda69
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/add-section-attr-doc.lisp
M books/kestrel/c/transformation/add-section-attr.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/external-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
Log Message:
-----------
Merge commit '341173cf7808df48111de7d6d314234934c26773' into HEAD
Commit: 58fdb80ad68176631088cf983438d3c49d8ba626
https://github.com/acl2/acl2/commit/58fdb80ad68176631088cf983438d3c49d8ba626
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/macro-tables.lisp
Log Message:
-----------
[C$] Add a built-in macro.
Commit: ca2a083403136b8e8c396f2cdd8649c1d0ba686a
https://github.com/acl2/acl2/commit/ca2a083403136b8e8c396f2cdd8649c1d0ba686a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Increase and discuss a stobj array size.
Commit: 5252067135c53951ea8a7e04b319ca73e1528c80
https://github.com/acl2/acl2/commit/5252067135c53951ea8a7e04b319ca73e1528c80
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/macro-tables.lisp
Log Message:
-----------
[C$] Add and discuss a predefined macro.
Commit: 2a987aece106ffa962bc3ff3c3e7b342311abca3
https://github.com/acl2/acl2/commit/2a987aece106ffa962bc3ff3c3e7b342311abca3
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/transformation/command-line/transform-c.lisp
M books/kestrel/utilities/run-json-command.lisp
Log Message:
-----------
Merge commit '4c26145746407b96922b06cadd3367946b777f54' into HEAD
Commit: ecbe2336b8ef442eb64eb056a60a18597a233f30
https://github.com/acl2/acl2/commit/ecbe2336b8ef442eb64eb056a60a18597a233f30
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve handling of self-contained files.
See added and updated documentation.
Commit: b6ff8328b8a00b50623e1848be812be549715852
https://github.com/acl2/acl2/commit/b6ff8328b8a00b50623e1848be812be549715852
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve preprocessor.
Improve handling of self-contained files. Avoid "re-using" the error-value-tuple
mechanism for throwing/propagating/handling the "non-self-contained exception",
because we need to preserve the `preprocessed` alist. Instead, add an explicit
flag, which is thrown/propagated/handled explicitly.
Commit: 6356fc47b78c9b250a312b412b66d9eabddde85c
https://github.com/acl2/acl2/commit/6356fc47b78c9b250a312b412b66d9eabddde85c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/add-section-attr-doc.lisp
M books/kestrel/c/transformation/add-section-attr.lisp
M books/kestrel/c/transformation/command-line/transform-c.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/external-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/utilities/run-json-command.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/4c2614574640...6356fc47b78c
https://github.com/acl2/acl2/commit/73c417ec3457dc8be4974600e678cbddbfd63697
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
Changed paths:
A books/projects/hol-in-acl2/acl2/hpp-set.lisp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
Log Message:
-----------
Tweaked theorem about a set of HOL values to be about a set of HOL value pairs.
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
Log Message:
-----------
Commit: 84d70e79290a0a817ccce18d56305869376bf480
https://github.com/acl2/acl2/commit/84d70e79290a0a817ccce18d56305869376bf480
Author: ACL2 Build Server <acl2bui...@gmail.com>
-----------
Merge commit '5bce3ca19bc16462c08aeea29ce5a10914e19bd0' into HEAD
https://github.com/acl2/acl2/commit/bb9c654461a0824e008b52e154fde5424f79eca0
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/std/util/defaggregate.lisp
M books/std/util/tests/defaggregate.lisp
Log Message:
-----------
Merge commit '85d75d8331db1ed76aa0ede0df1414f74dd1f03c' into HEAD
Changed paths:
M books/std/util/defaggregate.lisp
M books/std/util/tests/defaggregate.lisp
Log Message:
-----------
https://github.com/acl2/acl2/commit/223141e65ea78a6131623aaaad4c20e187716b27
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
A books/kestrel/arm/top.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/unroller.lisp
R books/kestrel/axe/x86/evaluator-x86.acl2
M books/kestrel/axe/x86/evaluator-x86.lisp
A books/kestrel/axe/x86/lifter-support.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/top.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/top.lisp
M books/kestrel/utilities/redundancy.lisp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
R books/kestrel/x86/x86-changes.acl2
M books/kestrel/x86/x86-changes.lisp
Log Message:
-----------
Merge commit 'a1674138cba2b2924f5563ebad7cf1eecd622d91' into HEAD
Commit: 1c31d98cf7eb8d8b5fd477dd5a153c46a7abda69
https://github.com/acl2/acl2/commit/1c31d98cf7eb8d8b5fd477dd5a153c46a7abda69
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/add-section-attr-doc.lisp
M books/kestrel/c/transformation/add-section-attr.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/external-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
Log Message:
-----------
Merge commit '341173cf7808df48111de7d6d314234934c26773' into HEAD
Commit: 58fdb80ad68176631088cf983438d3c49d8ba626
https://github.com/acl2/acl2/commit/58fdb80ad68176631088cf983438d3c49d8ba626
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/macro-tables.lisp
Log Message:
-----------
[C$] Add a built-in macro.
Commit: ca2a083403136b8e8c396f2cdd8649c1d0ba686a
https://github.com/acl2/acl2/commit/ca2a083403136b8e8c396f2cdd8649c1d0ba686a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Increase and discuss a stobj array size.
Commit: 5252067135c53951ea8a7e04b319ca73e1528c80
https://github.com/acl2/acl2/commit/5252067135c53951ea8a7e04b319ca73e1528c80
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/macro-tables.lisp
Log Message:
-----------
[C$] Add and discuss a predefined macro.
Commit: 2a987aece106ffa962bc3ff3c3e7b342311abca3
https://github.com/acl2/acl2/commit/2a987aece106ffa962bc3ff3c3e7b342311abca3
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/transformation/command-line/transform-c.lisp
M books/kestrel/utilities/run-json-command.lisp
Log Message:
-----------
Merge commit '4c26145746407b96922b06cadd3367946b777f54' into HEAD
Commit: ecbe2336b8ef442eb64eb056a60a18597a233f30
https://github.com/acl2/acl2/commit/ecbe2336b8ef442eb64eb056a60a18597a233f30
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
See added and updated documentation.
Commit: b6ff8328b8a00b50623e1848be812be549715852
https://github.com/acl2/acl2/commit/b6ff8328b8a00b50623e1848be812be549715852
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
Improve handling of self-contained files. Avoid "re-using" the error-value-tuple
mechanism for throwing/propagating/handling the "non-self-contained exception",
because we need to preserve the `preprocessed` alist. Instead, add an explicit
flag, which is thrown/propagated/handled explicitly.
Commit: 6356fc47b78c9b250a312b412b66d9eabddde85c
https://github.com/acl2/acl2/commit/6356fc47b78c9b250a312b412b66d9eabddde85c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/add-section-attr-doc.lisp
M books/kestrel/c/transformation/add-section-attr.lisp
M books/kestrel/c/transformation/command-line/transform-c.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/external-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/utilities/run-json-command.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/4c2614574640...6356fc47b78c
Reply all
Reply to author
Forward
0 new messages