[acl2/acl2] 06d9ff: [C$] Use library-generated theorems.
0 views
Skip to first unread message
Alessandro Coglio
12:42 AM (14 hours ago) 12:42 AM
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 06d9ff42923e0c60fca7266a27a6504050f58a8f
https://github.com/acl2/acl2/commit/06d9ff42923e0c60fca7266a27a6504050f58a8f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/external-preprocessing.lisp
M books/kestrel/c/syntax/input-files.lisp
Log Message:
-----------
[C$] Use library-generated theorems.
This theorem is already generated (with a slightly different name) by
`fty::defbytelist`.
Commit: 759de73a68076f2dd5022a105998d32397e45677
https://github.com/acl2/acl2/commit/759de73a68076f2dd5022a105998d32397e45677
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/external-preprocessing.lisp
M books/kestrel/c/syntax/input-files.lisp
Log Message:
-----------
[C$] Remove local theorems apparently no longer needed.
Commit: d9d82c8ec5f3f7c85a3894b90fb3f32d74574b10
https://github.com/acl2/acl2/commit/d9d82c8ec5f3f7c85a3894b90fb3f32d74574b10
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/package.lsp
Log Message:
-----------
[C$] Import a symbol.
Commit: 04ea3c4a52b0ca47276989eab9fd69a3db9aef79
https://github.com/acl2/acl2/commit/04ea3c4a52b0ca47276989eab9fd69a3db9aef79
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Streamline some preprocessor code.
Use lists of strings for the user-specified file paths, along with a string path
prefix, as in `input-files`.
Commit: 9a24fe03e6f481d577740105cab6c560bff8145a
https://github.com/acl2/acl2/commit/9a24fe03e6f481d577740105cab6c560bff8145a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-printer.lisp
Log Message:
-----------
[C$] Remove redundant package prefix.
Commit: e672dc6bf04967c29d08f31463bb49593aed335c
https://github.com/acl2/acl2/commit/e672dc6bf04967c29d08f31463bb49593aed335c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/package.lsp
Log Message:
-----------
[C$] Import a symbol.
Commit: 23bde28155a21deda5e125ffa17ff0e9e17bf6e6
https://github.com/acl2/acl2/commit/23bde28155a21deda5e125ffa17ff0e9e17bf6e6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Add code to read files explicitly specified as input (vs. the ones encountered
in `#include`s).
Add code to detect circular depedencies among fles.
Extend some functions to return state, needed because the function to read bytes
from files returns state.
Commit: 83834b3beba2a25132ad4c80aa5b43230e4c1380
https://github.com/acl2/acl2/commit/83834b3beba2a25132ad4c80aa5b43230e4c1380
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Fix code indentation.
Commit: aa941139c049fcf178691ddfcdf52c2a0ab246db
https://github.com/acl2/acl2/commit/aa941139c049fcf178691ddfcdf52c2a0ab246db
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M apply-prim.lisp
M axioms.lisp
M books/demos/floating-point-log.txt
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M translate.lisp
Log Message:
-----------
Add-macro-alias, add-macro-fn, and add-binop now support a second argument that is a macro-alias. :Trans* uses the :TERM evisc-tuple when printing; clarified :DOC accordingly in :DOC for :trans* and also :trans. Deref-macro-name is now more directly a :logic mode function (doesn't use system-verify-guards mechanism). Removed a confusing comment in (set-table-guard macro-aliases-table ...).
Quoting :DOC note-8-7:
It was the case that in an [event] (add-macro-alias mac fn),
(add-macro-fn mac fn), or (add-binop mac fn), if fn was a macro
name then this event generally had no effect. Now, if in addition
an event (add-macro-alias fn fn2) has first been admitted (and no
later such event has been admitted), then in these three events, fn
will be treated as fn2. See [add-macro-alias]. Thanks to Grant
Jurgensen for sending an example that showed how a confusing
[in-theory] error could occur before this change, in the situation
described above: after the change, (in-theory (disable mac)) is
treated as a directive to [disable] fn2; but before the change it
was treated as an attempt to [disable] the macro, fn, which caused
an error.
The utility :[trans*] new uses the :TERM [evisc-tuple] (see
[set-evisc-tuple]) to print terms, as was already being done by
:[trans].
Removed deref-macro-name from *system-verify-guards-alist* and,
therefore, removed the form (verify-termination deref-macro-name)
from books/system/verified-termination-and-guards.lisp since it was
no longer necessary.
Passed "make proofs" in addition to the usual regression-everything.
Commit: 10af2c0f05a3e4127ff45eb0dede3c4cc466a04a
https://github.com/acl2/acl2/commit/10af2c0f05a3e4127ff45eb0dede3c4cc466a04a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Improve printer implementation.
Use a flag instead of two separate functions to distinguish between inline and
non-inline declarations.
Commit: 02e3efb4c55b08c0d7a12cd34cf3c83ef4489108
https://github.com/acl2/acl2/commit/02e3efb4c55b08c0d7a12cd34cf3c83ef4489108
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Use local stobj for preprocessing each file.
Commit: 7e1117ed109a7e97b04fa74d14b9fc22540de751
https://github.com/acl2/acl2/commit/7e1117ed109a7e97b04fa74d14b9fc22540de751
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Improve printer implementation.
There is no longer a need for lexicographic measures.
Commit: 6dea2320c2c28e86766fb30dbe608e3a33099f97
https://github.com/acl2/acl2/commit/6dea2320c2c28e86766fb30dbe608e3a33099f97
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Start putting the relevant functions into a (bogus, for now) mutual recursion.
Commit: 3fb8d08a7ce784c2b183a06213c908ff32c6d5d6
https://github.com/acl2/acl2/commit/3fb8d08a7ce784c2b183a06213c908ff32c6d5d6
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Made small improvements in :DOC note-8-7.
Commit: 0fccc40267650f2dfab8bdf6249dffa7c8e638dd
https://github.com/acl2/acl2/commit/0fccc40267650f2dfab8bdf6249dffa7c8e638dd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Start a generalization of the printer.
Add an 'inline' flag for (not) printing structure declarations inline under
suitable conditions (still to be implemented).
Commit: 11d1084b5af61655e3f239d483f126c99b6ddacf
https://github.com/acl2/acl2/commit/11d1084b5af61655e3f239d483f126c99b6ddacf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M apply-prim.lisp
M axioms.lisp
M books/demos/floating-point-log.txt
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M translate.lisp
Log Message:
-----------
Merge.
Commit: 639239896ff4384957016da1847ef6ba30f2e5d6
https://github.com/acl2/acl2/commit/639239896ff4384957016da1847ef6ba30f2e5d6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M apply-prim.lisp
M axioms.lisp
M books/demos/floating-point-log.txt
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M translate.lisp
Log Message:
-----------
Merge.
Commit: 41b97a728d9d0c308ce2bedea7f643ba32fa0f4d
https://github.com/acl2/acl2/commit/41b97a728d9d0c308ce2bedea7f643ba32fa0f4d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Expand some doc about the preprocessor.
Commit: aadb2f16a9aecf0c1b00c2f67ce741acc8f674ff
https://github.com/acl2/acl2/commit/aadb2f16a9aecf0c1b00c2f67ce741acc8f674ff
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Fix bug in printer.
A space and some attributes were printed in the wrong order.
Commit: 5336bc2276b36c466a0bde50e65bb53a2573c7ea
https://github.com/acl2/acl2/commit/5336bc2276b36c466a0bde50e65bb53a2573c7ea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add and document reversing of lexemes in preprocessor.
Commit: a44f8ced66c5506dafa0414d367fc3cd86f6b512
https://github.com/acl2/acl2/commit/a44f8ced66c5506dafa0414d367fc3cd86f6b512
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Slightly simplify some printer code.
Commit: 4c3f59dbdc03caced0c3da47ebabfa1b0d1792ce
https://github.com/acl2/acl2/commit/4c3f59dbdc03caced0c3da47ebabfa1b0d1792ce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Generalize some printer code.
Add a flag for priting structure or union specifiers on multiple lines.
Commit: 56b350e806c4adc84621a5b5e129a4e93fd41098
https://github.com/acl2/acl2/commit/56b350e806c4adc84621a5b5e129a4e93fd41098
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Generalize some printer code.
Add an inline flag to the function to print type specifiers.
Commit: 6a5f2d68050a792dec3a63b30faf3372d9e7d06a
https://github.com/acl2/acl2/commit/6a5f2d68050a792dec3a63b30faf3372d9e7d06a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/package.lsp
Log Message:
-----------
[C$] Import symbol into package.
Commit: e6e128e1c3376e639f8a66d1831d7e1a0210bfc8
https://github.com/acl2/acl2/commit/e6e128e1c3376e639f8a66d1831d7e1a0210bfc8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Add loop through group parts.
Add proper measures.
Add `mbt` checks for termination.
Add theorems about size of `preprocessed` alist.
Commit: 447b512cb07d6f81703cb6c4f0d5174b4d6f65cb
https://github.com/acl2/acl2/commit/447b512cb07d6f81703cb6c4f0d5174b4d6f65cb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Generalize some printer code.
Add more `inlinep` flags.
Also improve some documentation of these flags.
Commit: affebec033c33b6b73ce20256b9513aff20bce52
https://github.com/acl2/acl2/commit/affebec033c33b6b73ce20256b9513aff20bce52
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
Log Message:
-----------
[C$] Improve printer.
Now `struct`s and `union`s, when "isolated", are printed on multiple lines as
idiomatic.
Commit: 7b7f2b55a81f392b4f1b680d9594431f959a3426
https://github.com/acl2/acl2/commit/7b7f2b55a81f392b4f1b680d9594431f959a3426
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Add a theorem.
Commit: 78ca920a0f2809e465b95eb2c4d80ad5c087ff45
https://github.com/acl2/acl2/commit/78ca920a0f2809e465b95eb2c4d80ad5c087ff45
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Add handling of EOF and of text lines without tokens.
Commit: 9d14bb83a5131ab4e84c816fceb170b609e7107f
https://github.com/acl2/acl2/commit/9d14bb83a5131ab4e84c816fceb170b609e7107f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add mapping of preprocessor lexemes to messages.
Commit: 98e56d41456dbca05f433b622a17cc225f1c5375
https://github.com/acl2/acl2/commit/98e56d41456dbca05f433b622a17cc225f1c5375
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add a comment.
Commit: 796adb962260f92d1d6c8fcf5d94a96400bec3b4
https://github.com/acl2/acl2/commit/796adb962260f92d1d6c8fcf5d94a96400bec3b4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Add a predicate on lexemes.
Commit: b2b8221777458852da0df60a9f18dc65bb7d044b
https://github.com/acl2/acl2/commit/b2b8221777458852da0df60a9f18dc65bb7d044b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve/extend some preprocessor code.
Commit: eb2e6e8dbfcb3d139f5c9a4e8b6907ace4a3066b
https://github.com/acl2/acl2/commit/eb2e6e8dbfcb3d139f5c9a4e8b6907ace4a3066b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
Log Message:
-----------
[C$] Improve printer.
Print structs and union on multiple lines in more circumstances.
Commit: 4d1dc888e656f6f7dcfa04bf165881e6fdb335b7
https://github.com/acl2/acl2/commit/4d1dc888e656f6f7dcfa04bf165881e6fdb335b7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Commit: 717a1fcf8d2086c3d38f080a1b8d76faa49692fa
https://github.com/acl2/acl2/commit/717a1fcf8d2086c3d38f080a1b8d76faa49692fa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Simplify some code.
Commit: 98ebcf0448af9a6a9e99fc9ca288876d56853deb
https://github.com/acl2/acl2/commit/98ebcf0448af9a6a9e99fc9ca288876d56853deb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/efbfc290fe21...98ebcf0448af
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 06d9ff42923e0c60fca7266a27a6504050f58a8f
https://github.com/acl2/acl2/commit/06d9ff42923e0c60fca7266a27a6504050f58a8f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/external-preprocessing.lisp
M books/kestrel/c/syntax/input-files.lisp
Log Message:
-----------
[C$] Use library-generated theorems.
This theorem is already generated (with a slightly different name) by
`fty::defbytelist`.
Commit: 759de73a68076f2dd5022a105998d32397e45677
https://github.com/acl2/acl2/commit/759de73a68076f2dd5022a105998d32397e45677
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/external-preprocessing.lisp
M books/kestrel/c/syntax/input-files.lisp
Log Message:
-----------
[C$] Remove local theorems apparently no longer needed.
Commit: d9d82c8ec5f3f7c85a3894b90fb3f32d74574b10
https://github.com/acl2/acl2/commit/d9d82c8ec5f3f7c85a3894b90fb3f32d74574b10
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/package.lsp
Log Message:
-----------
[C$] Import a symbol.
Commit: 04ea3c4a52b0ca47276989eab9fd69a3db9aef79
https://github.com/acl2/acl2/commit/04ea3c4a52b0ca47276989eab9fd69a3db9aef79
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Streamline some preprocessor code.
Use lists of strings for the user-specified file paths, along with a string path
prefix, as in `input-files`.
Commit: 9a24fe03e6f481d577740105cab6c560bff8145a
https://github.com/acl2/acl2/commit/9a24fe03e6f481d577740105cab6c560bff8145a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-printer.lisp
Log Message:
-----------
[C$] Remove redundant package prefix.
Commit: e672dc6bf04967c29d08f31463bb49593aed335c
https://github.com/acl2/acl2/commit/e672dc6bf04967c29d08f31463bb49593aed335c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/package.lsp
Log Message:
-----------
[C$] Import a symbol.
Commit: 23bde28155a21deda5e125ffa17ff0e9e17bf6e6
https://github.com/acl2/acl2/commit/23bde28155a21deda5e125ffa17ff0e9e17bf6e6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Add code to read files explicitly specified as input (vs. the ones encountered
in `#include`s).
Add code to detect circular depedencies among fles.
Extend some functions to return state, needed because the function to read bytes
from files returns state.
Commit: 83834b3beba2a25132ad4c80aa5b43230e4c1380
https://github.com/acl2/acl2/commit/83834b3beba2a25132ad4c80aa5b43230e4c1380
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Fix code indentation.
Commit: aa941139c049fcf178691ddfcdf52c2a0ab246db
https://github.com/acl2/acl2/commit/aa941139c049fcf178691ddfcdf52c2a0ab246db
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M apply-prim.lisp
M axioms.lisp
M books/demos/floating-point-log.txt
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M translate.lisp
Log Message:
-----------
Add-macro-alias, add-macro-fn, and add-binop now support a second argument that is a macro-alias. :Trans* uses the :TERM evisc-tuple when printing; clarified :DOC accordingly in :DOC for :trans* and also :trans. Deref-macro-name is now more directly a :logic mode function (doesn't use system-verify-guards mechanism). Removed a confusing comment in (set-table-guard macro-aliases-table ...).
Quoting :DOC note-8-7:
It was the case that in an [event] (add-macro-alias mac fn),
(add-macro-fn mac fn), or (add-binop mac fn), if fn was a macro
name then this event generally had no effect. Now, if in addition
an event (add-macro-alias fn fn2) has first been admitted (and no
later such event has been admitted), then in these three events, fn
will be treated as fn2. See [add-macro-alias]. Thanks to Grant
Jurgensen for sending an example that showed how a confusing
[in-theory] error could occur before this change, in the situation
described above: after the change, (in-theory (disable mac)) is
treated as a directive to [disable] fn2; but before the change it
was treated as an attempt to [disable] the macro, fn, which caused
an error.
The utility :[trans*] new uses the :TERM [evisc-tuple] (see
[set-evisc-tuple]) to print terms, as was already being done by
:[trans].
Removed deref-macro-name from *system-verify-guards-alist* and,
therefore, removed the form (verify-termination deref-macro-name)
from books/system/verified-termination-and-guards.lisp since it was
no longer necessary.
Passed "make proofs" in addition to the usual regression-everything.
Commit: 10af2c0f05a3e4127ff45eb0dede3c4cc466a04a
https://github.com/acl2/acl2/commit/10af2c0f05a3e4127ff45eb0dede3c4cc466a04a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Improve printer implementation.
Use a flag instead of two separate functions to distinguish between inline and
non-inline declarations.
Commit: 02e3efb4c55b08c0d7a12cd34cf3c83ef4489108
https://github.com/acl2/acl2/commit/02e3efb4c55b08c0d7a12cd34cf3c83ef4489108
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Use local stobj for preprocessing each file.
Commit: 7e1117ed109a7e97b04fa74d14b9fc22540de751
https://github.com/acl2/acl2/commit/7e1117ed109a7e97b04fa74d14b9fc22540de751
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Improve printer implementation.
There is no longer a need for lexicographic measures.
Commit: 6dea2320c2c28e86766fb30dbe608e3a33099f97
https://github.com/acl2/acl2/commit/6dea2320c2c28e86766fb30dbe608e3a33099f97
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Start putting the relevant functions into a (bogus, for now) mutual recursion.
Commit: 3fb8d08a7ce784c2b183a06213c908ff32c6d5d6
https://github.com/acl2/acl2/commit/3fb8d08a7ce784c2b183a06213c908ff32c6d5d6
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Made small improvements in :DOC note-8-7.
Commit: 0fccc40267650f2dfab8bdf6249dffa7c8e638dd
https://github.com/acl2/acl2/commit/0fccc40267650f2dfab8bdf6249dffa7c8e638dd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Start a generalization of the printer.
Add an 'inline' flag for (not) printing structure declarations inline under
suitable conditions (still to be implemented).
Commit: 11d1084b5af61655e3f239d483f126c99b6ddacf
https://github.com/acl2/acl2/commit/11d1084b5af61655e3f239d483f126c99b6ddacf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M apply-prim.lisp
M axioms.lisp
M books/demos/floating-point-log.txt
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M translate.lisp
Log Message:
-----------
Merge.
Commit: 639239896ff4384957016da1847ef6ba30f2e5d6
https://github.com/acl2/acl2/commit/639239896ff4384957016da1847ef6ba30f2e5d6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M apply-prim.lisp
M axioms.lisp
M books/demos/floating-point-log.txt
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M translate.lisp
Log Message:
-----------
Merge.
Commit: 41b97a728d9d0c308ce2bedea7f643ba32fa0f4d
https://github.com/acl2/acl2/commit/41b97a728d9d0c308ce2bedea7f643ba32fa0f4d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Expand some doc about the preprocessor.
Commit: aadb2f16a9aecf0c1b00c2f67ce741acc8f674ff
https://github.com/acl2/acl2/commit/aadb2f16a9aecf0c1b00c2f67ce741acc8f674ff
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Fix bug in printer.
A space and some attributes were printed in the wrong order.
Commit: 5336bc2276b36c466a0bde50e65bb53a2573c7ea
https://github.com/acl2/acl2/commit/5336bc2276b36c466a0bde50e65bb53a2573c7ea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add and document reversing of lexemes in preprocessor.
Commit: a44f8ced66c5506dafa0414d367fc3cd86f6b512
https://github.com/acl2/acl2/commit/a44f8ced66c5506dafa0414d367fc3cd86f6b512
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Slightly simplify some printer code.
Commit: 4c3f59dbdc03caced0c3da47ebabfa1b0d1792ce
https://github.com/acl2/acl2/commit/4c3f59dbdc03caced0c3da47ebabfa1b0d1792ce
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Generalize some printer code.
Add a flag for priting structure or union specifiers on multiple lines.
Commit: 56b350e806c4adc84621a5b5e129a4e93fd41098
https://github.com/acl2/acl2/commit/56b350e806c4adc84621a5b5e129a4e93fd41098
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Generalize some printer code.
Add an inline flag to the function to print type specifiers.
Commit: 6a5f2d68050a792dec3a63b30faf3372d9e7d06a
https://github.com/acl2/acl2/commit/6a5f2d68050a792dec3a63b30faf3372d9e7d06a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/package.lsp
Log Message:
-----------
[C$] Import symbol into package.
Commit: e6e128e1c3376e639f8a66d1831d7e1a0210bfc8
https://github.com/acl2/acl2/commit/e6e128e1c3376e639f8a66d1831d7e1a0210bfc8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Add loop through group parts.
Add proper measures.
Add `mbt` checks for termination.
Add theorems about size of `preprocessed` alist.
Commit: 447b512cb07d6f81703cb6c4f0d5174b4d6f65cb
https://github.com/acl2/acl2/commit/447b512cb07d6f81703cb6c4f0d5174b4d6f65cb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Generalize some printer code.
Add more `inlinep` flags.
Also improve some documentation of these flags.
Commit: affebec033c33b6b73ce20256b9513aff20bce52
https://github.com/acl2/acl2/commit/affebec033c33b6b73ce20256b9513aff20bce52
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
Log Message:
-----------
[C$] Improve printer.
Now `struct`s and `union`s, when "isolated", are printed on multiple lines as
idiomatic.
Commit: 7b7f2b55a81f392b4f1b680d9594431f959a3426
https://github.com/acl2/acl2/commit/7b7f2b55a81f392b4f1b680d9594431f959a3426
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Add a theorem.
Commit: 78ca920a0f2809e465b95eb2c4d80ad5c087ff45
https://github.com/acl2/acl2/commit/78ca920a0f2809e465b95eb2c4d80ad5c087ff45
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Add handling of EOF and of text lines without tokens.
Commit: 9d14bb83a5131ab4e84c816fceb170b609e7107f
https://github.com/acl2/acl2/commit/9d14bb83a5131ab4e84c816fceb170b609e7107f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add mapping of preprocessor lexemes to messages.
Commit: 98e56d41456dbca05f433b622a17cc225f1c5375
https://github.com/acl2/acl2/commit/98e56d41456dbca05f433b622a17cc225f1c5375
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add a comment.
Commit: 796adb962260f92d1d6c8fcf5d94a96400bec3b4
https://github.com/acl2/acl2/commit/796adb962260f92d1d6c8fcf5d94a96400bec3b4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Add a predicate on lexemes.
Commit: b2b8221777458852da0df60a9f18dc65bb7d044b
https://github.com/acl2/acl2/commit/b2b8221777458852da0df60a9f18dc65bb7d044b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve/extend some preprocessor code.
Commit: eb2e6e8dbfcb3d139f5c9a4e8b6907ace4a3066b
https://github.com/acl2/acl2/commit/eb2e6e8dbfcb3d139f5c9a4e8b6907ace4a3066b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
Log Message:
-----------
[C$] Improve printer.
Print structs and union on multiple lines in more circumstances.
Commit: 4d1dc888e656f6f7dcfa04bf165881e6fdb335b7
https://github.com/acl2/acl2/commit/4d1dc888e656f6f7dcfa04bf165881e6fdb335b7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Commit: 717a1fcf8d2086c3d38f080a1b8d76faa49692fa
https://github.com/acl2/acl2/commit/717a1fcf8d2086c3d38f080a1b8d76faa49692fa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Simplify some code.
Commit: 98ebcf0448af9a6a9e99fc9ca288876d56853deb
https://github.com/acl2/acl2/commit/98ebcf0448af9a6a9e99fc9ca288876d56853deb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/efbfc290fe21...98ebcf0448af
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
2:53 AM (12 hours ago) 2:53 AM
to acl2-...@googlegroups.com
Alessandro Coglio
2:53 AM (12 hours ago) 2:53 AM
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
12:01 PM (3 hours ago) 12:01 PM
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Compare: https://github.com/acl2/acl2/compare/efbfc290fe21...98ebcf0448af
Commit: aa941139c049fcf178691ddfcdf52c2a0ab246db
https://github.com/acl2/acl2/commit/aa941139c049fcf178691ddfcdf52c2a0ab246db
Author: Matt Kaufmann <matthew.j...@gmail.com>
https://github.com/acl2/acl2/commit/aa941139c049fcf178691ddfcdf52c2a0ab246db
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2025-12-14 (Sun, 14 Dec 2025)
Changed paths:
Changed paths:
M apply-prim.lisp
M axioms.lisp
M books/demos/floating-point-log.txt
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M translate.lisp
Log Message:
-----------
M axioms.lisp
M books/demos/floating-point-log.txt
M books/system/doc/acl2-doc.lisp
M books/system/verified-termination-and-guards.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
M translate.lisp
Log Message:
-----------
Add-macro-alias, add-macro-fn, and add-binop now support a second argument that is a macro-alias. :Trans* uses the :TERM evisc-tuple when printing; clarified :DOC accordingly in :DOC for :trans* and also :trans. Deref-macro-name is now more directly a :logic mode function (doesn't use system-verify-guards mechanism). Removed a confusing comment in (set-table-guard macro-aliases-table ...).
Quoting :DOC note-8-7:
It was the case that in an [event] (add-macro-alias mac fn),
(add-macro-fn mac fn), or (add-binop mac fn), if fn was a macro
name then this event generally had no effect. Now, if in addition
an event (add-macro-alias fn fn2) has first been admitted (and no
later such event has been admitted), then in these three events, fn
will be treated as fn2. See [add-macro-alias]. Thanks to Grant
Jurgensen for sending an example that showed how a confusing
[in-theory] error could occur before this change, in the situation
described above: after the change, (in-theory (disable mac)) is
treated as a directive to [disable] fn2; but before the change it
was treated as an attempt to [disable] the macro, fn, which caused
an error.
The utility :[trans*] new uses the :TERM [evisc-tuple] (see
[set-evisc-tuple]) to print terms, as was already being done by
:[trans].
Removed deref-macro-name from *system-verify-guards-alist* and,
therefore, removed the form (verify-termination deref-macro-name)
from books/system/verified-termination-and-guards.lisp since it was
no longer necessary.
Passed "make proofs" in addition to the usual regression-everything.
Quoting :DOC note-8-7:
It was the case that in an [event] (add-macro-alias mac fn),
(add-macro-fn mac fn), or (add-binop mac fn), if fn was a macro
name then this event generally had no effect. Now, if in addition
an event (add-macro-alias fn fn2) has first been admitted (and no
later such event has been admitted), then in these three events, fn
will be treated as fn2. See [add-macro-alias]. Thanks to Grant
Jurgensen for sending an example that showed how a confusing
[in-theory] error could occur before this change, in the situation
described above: after the change, (in-theory (disable mac)) is
treated as a directive to [disable] fn2; but before the change it
was treated as an attempt to [disable] the macro, fn, which caused
an error.
The utility :[trans*] new uses the :TERM [evisc-tuple] (see
[set-evisc-tuple]) to print terms, as was already being done by
:[trans].
Removed deref-macro-name from *system-verify-guards-alist* and,
therefore, removed the form (verify-termination deref-macro-name)
from books/system/verified-termination-and-guards.lisp since it was
no longer necessary.
Passed "make proofs" in addition to the usual regression-everything.
Commit: 3fb8d08a7ce784c2b183a06213c908ff32c6d5d6
https://github.com/acl2/acl2/commit/3fb8d08a7ce784c2b183a06213c908ff32c6d5d6
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
https://github.com/acl2/acl2/commit/3fb8d08a7ce784c2b183a06213c908ff32c6d5d6
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-12-15 (Mon, 15 Dec 2025)
Changed paths:
M books/system/doc/acl2-doc.lisp
Changed paths:
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M doc/acl2-code-size.txt
M doc/home-page.html
Log Message:
-----------
Made small improvements in :DOC note-8-7.
-----------
Made small improvements in :DOC note-8-7.
Reply all
Reply to author
Forward
0 new messages