[acl2/acl2] 270694: [C2C] Reorder some code.
0 views
Skip to first unread message
Alessandro Coglio
Jan 13, 2026, 12:13:22 AM (8 days ago) Jan 13
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 270694db49be35512f0e1161334146c2fd2cc3b4
https://github.com/acl2/acl2/commit/270694db49be35512f0e1161334146c2fd2cc3b4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Reorder some code.
Put guard verification earlier, as soon as all the theorems it needs are proved.
Commit: 533c78c3c6fda4f453966df7149e446ad7448777
https://github.com/acl2/acl2/commit/533c78c3c6fda4f453966df7149e446ad7448777
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Fix some `defret-mutual` names.
Commit: af47c9e42b336fb0ef3cf6eb158344e40aa1df22
https://github.com/acl2/acl2/commit/af47c9e42b336fb0ef3cf6eb158344e40aa1df22
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-09 (Fri, 09 Jan 2026)
Changed paths:
M acl2-init.lisp
Log Message:
-----------
Disable xref recording in SBCL.
This didn't noticeably affect "make regression-everything" time (using -j 20 on Linux):
;;; Previous (Jan. 7):
97642.058u 6791.411s 1:52:23.62 1548.6% 0+0k 4056816+11973888io 30pf+0w
;;; New:
97399.966u 6992.549s 1:51:44.33 1557.0% 0+0k 3353848+12250952io 31pf+0w
I added the following comment in acl2-init.lisp to explain the change,
which was contributed by Jim White (thanks!).
; The following was contributed by Jim White, who used Copilot on 1/8/2026 to
; suggest the following addition to prevent raw Lisp errors when certifying the
; following with SBCL 2.9.11 on ARM64 (Ubuntu 24.04.3 LTS running in Docker
; container): demos/congruent-stobjs-book, demos/brr-test-book,
; demos/refinement-failure-test-book, demos/brr-free-variables-book, and
; workshops/2023/kaufmann-moore/brr-book. If SBCL bug #2137765 is fixed
; (https://bugs.launchpad.net/sbcl/+bug/2137765), then we might remove this
; change sometime later.
Commit: a2672b98a1e39194eff59483fbf5697ce6587d45
https://github.com/acl2/acl2/commit/a2672b98a1e39194eff59483fbf5697ce6587d45
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-09 (Fri, 09 Jan 2026)
Changed paths:
M acl2-init.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/including.c
M books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/text.c
Log Message:
-----------
Merge.
Commit: 466cd060dafeb08e9e5fadd09170817c0626b923
https://github.com/acl2/acl2/commit/466cd060dafeb08e9e5fadd09170817c0626b923
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Take fixtype from library.
Commit: 42d5d485f67d5adc889e1dcf9b67bfebd65b3ddb
https://github.com/acl2/acl2/commit/42d5d485f67d5adc889e1dcf9b67bfebd65b3ddb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Simplify some hints.
This is already enabled locally to the `defsection`.
Commit: d4411252f926f9bbf081469aca7f2fe0f948fe60
https://github.com/acl2/acl2/commit/d4411252f926f9bbf081469aca7f2fe0f948fe60
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Fix doc.
Commit: 634a57fd1ab0c1d6f7033494101f4783a11fa5e3
https://github.com/acl2/acl2/commit/634a57fd1ab0c1d6f7033494101f4783a11fa5e3
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-top.lisp
Log Message:
-----------
For hol-in-acl2 library: tweaked eval_poly example, and changed ex1 example to be much more interesting.
Thanks to Konrad Slind for running the translator to get this
extension of the ex1 example.
Commit: 78f209a2e9fcdbe5840d043d5669369872d543f4
https://github.com/acl2/acl2/commit/78f209a2e9fcdbe5840d043d5669369872d543f4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-top.lisp
Log Message:
-----------
Merge.
Commit: 5ac06760aeaea56329a88cab544a14837f1ad4aa
https://github.com/acl2/acl2/commit/5ac06760aeaea56329a88cab544a14837f1ad4aa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Extend some preprocessor data structures.
Add markers used for preventing recursive macro expansion and for handling the
`##` operator.
Commit: 0f3d5a9870deb5a82ea1317a6bd973950d65a5be
https://github.com/acl2/acl2/commit/0f3d5a9870deb5a82ea1317a6bd973950d65a5be
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-top.lisp
Log Message:
-----------
Merge.
Commit: 692e6a261f9d0f810e43630605b106992628fc09
https://github.com/acl2/acl2/commit/692e6a261f9d0f810e43630605b106992628fc09
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Abbreviate some names.
Commit: a8b9cbdb970af8aa3d62ed93aa8c04d69106cf7e
https://github.com/acl2/acl2/commit/a8b9cbdb970af8aa3d62ed93aa8c04d69106cf7e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Simplify some hints.
This is locally enabled.
Commit: edcff5efd6e74c4146dbae6673a34f86aed994e6
https://github.com/acl2/acl2/commit/edcff5efd6e74c4146dbae6673a34f86aed994e6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Simplify some hints.
This is still auto-enabled by `defstobj`, until it is disabled at the end of the
`defsection`.
Commit: e26e91df44ed97bffdcce9e17d01fb056da45e6c
https://github.com/acl2/acl2/commit/e26e91df44ed97bffdcce9e17d01fb056da45e6c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Update some doc to new nomenclature.
Commit: d89f35735502a65480b8606112decd36204b35ed
https://github.com/acl2/acl2/commit/d89f35735502a65480b8606112decd36204b35ed
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Revise preprocessing lexemes in stobj.
Use a simple list of lexmarks. This can be turned into an array if efficiency is
an issue, but we don't need the back-and-forth of read/unread lexemes as we do
for tokens (in the parser) and for characters (in the parser and preprocessor).
Commit: 63ca027466fcf8cb25869bd807000a1006bc7d40
https://github.com/acl2/acl2/commit/63ca027466fcf8cb25869bd807000a1006bc7d40
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
Log Message:
-----------
[C$] Rename a funcion.
Commit: 54939142fc2c46e05df2360825f45bf45ecd1610
https://github.com/acl2/acl2/commit/54939142fc2c46e05df2360825f45bf45ecd1610
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
Log Message:
-----------
[C$] Rename function.
Commit: 56fa21aa16d544e6cb1c95c2921ea2b751f45f96
https://github.com/acl2/acl2/commit/56fa21aa16d544e6cb1c95c2921ea2b751f45f96
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Move a function.
Commit: c59a2c30e0ac78173df413c99f20dfe80d7c89e5
https://github.com/acl2/acl2/commit/c59a2c30e0ac78173df413c99f20dfe80d7c89e5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add and use an operation on preprocessing states.
Commit: 2324bca07fc296fadb3f9a92891bfb4b0d1b3b40
https://github.com/acl2/acl2/commit/2324bca07fc296fadb3f9a92891bfb4b0d1b3b40
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Add missing stobj update.
Commit: db2ba721e37bcefea123712c102dba26224a0a51
https://github.com/acl2/acl2/commit/db2ba721e37bcefea123712c102dba26224a0a51
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Remove list fixtype no longer needed.
Commit: efd30628c83e0440befb7edcbd7885d7d5785152
https://github.com/acl2/acl2/commit/efd30628c83e0440befb7edcbd7885d7d5785152
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Eliminate a data structure no longer needed.
We "inline" lexeme and span into a lexmark. We also make the span optional.
Commit: 5282f27b973d3be9faf0c0cd697292a0a50169a4
https://github.com/acl2/acl2/commit/5282f27b973d3be9faf0c0cd697292a0a50169a4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Require spans in lexmarks that are lexemes.
Commit: 9fcb317a2cd13186732121388db829f22d76f555
https://github.com/acl2/acl2/commit/9fcb317a2cd13186732121388db829f22d76f555
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Remove theorems no longer needed.
Commit: fc6636d73bd535a97b28f3baf0b8cf65b8d8a0ab
https://github.com/acl2/acl2/commit/fc6636d73bd535a97b28f3baf0b8cf65b8d8a0ab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
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/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
Log Message:
-----------
[C$] Streamline handling of line comments.
Exclude the ending new line from the line comment lexeme. This makes for a more
uniform treatment of new lines.
Commit: cce802edcf32aaddf223df996dcea7bcf8437593
https://github.com/acl2/acl2/commit/cce802edcf32aaddf223df996dcea7bcf8437593
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Make all stobj readers fixing.
Commit: 924b1c7247a4f512ca6f80c0c1f44efad86a6bf2
https://github.com/acl2/acl2/commit/924b1c7247a4f512ca6f80c0c1f44efad86a6bf2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Have all `ppstate` writes fix their inputs.
Commit: ae5fa114bbcbf3a99cb283f75c39b003cf1a11ba
https://github.com/acl2/acl2/commit/ae5fa114bbcbf3a99cb283f75c39b003cf1a11ba
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Factor some enablements.
Commit: c3b7b27665cada7904a8c4d0354a9d5849e48a91
https://github.com/acl2/acl2/commit/c3b7b27665cada7904a8c4d0354a9d5849e48a91
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Add a theorem.
Commit: 27b60c5a3d36fdbb315b07e84258f64272ac5808
https://github.com/acl2/acl2/commit/27b60c5a3d36fdbb315b07e84258f64272ac5808
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Factor some enablements.
Commit: a1073e65c302878283b8ae5870f9b78531df9cfc
https://github.com/acl2/acl2/commit/a1073e65c302878283b8ae5870f9b78531df9cfc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Factor more enablements.
Commit: 302e1e34be088e2e4750aba391512102fa8ba509
https://github.com/acl2/acl2/commit/302e1e34be088e2e4750aba391512102fa8ba509
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Consolidate some hints.
Commit: 0279bacc8f232262c38ae68e568c17d36482658a
https://github.com/acl2/acl2/commit/0279bacc8f232262c38ae68e568c17d36482658a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Add a theorem.
Commit: 9f674c67ce656cebbd962eb7e58cc735ecf8c436
https://github.com/acl2/acl2/commit/9f674c67ce656cebbd962eb7e58cc735ecf8c436
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Remove redundant hints.
Commit: 4e6546503c1a2739ccb7e3833abb83a96a7b245f
https://github.com/acl2/acl2/commit/4e6546503c1a2739ccb7e3833abb83a96a7b245f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Remove unnecessary hint.
Commit: ef3d6b4e76ce9f918b977775485fc9486a6257d1
https://github.com/acl2/acl2/commit/ef3d6b4e76ce9f918b977775485fc9486a6257d1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/std/util/defprojection.lisp
Log Message:
-----------
[Std/util] Fix doc.
Commit: c49e4f7673537e0fd68cf28a22f42317f351f787
https://github.com/acl2/acl2/commit/c49e4f7673537e0fd68cf28a22f42317f351f787
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/atc/generation.lisp
A books/kestrel/c/atc/limits.lisp
Log Message:
-----------
[ATC] Add a data structure for limits.
Commit: 78057776cd527f9ff91bd549f6b155d3f7232144
https://github.com/acl2/acl2/commit/78057776cd527f9ff91bd549f6b155d3f7232144
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Add some fixing theorems.
Commit: ba6d16df703a0a5601f552712f819ce70b799b01
https://github.com/acl2/acl2/commit/ba6d16df703a0a5601f552712f819ce70b799b01
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Extend some theorems.
Commit: 86abf8450679cbad5bb7fa3917bcfdac9a367922
https://github.com/acl2/acl2/commit/86abf8450679cbad5bb7fa3917bcfdac9a367922
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Simplify some code.
Commit: 6264a7c6db8e5e72cdc753a516c8505d00fa495f
https://github.com/acl2/acl2/commit/6264a7c6db8e5e72cdc753a516c8505d00fa495f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
Merge.
Commit: 268423724700e2858c032161a7313b574e285f24
https://github.com/acl2/acl2/commit/268423724700e2858c032161a7313b574e285f24
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/atc/generation.lisp
A books/kestrel/c/atc/limits.lisp
M books/std/util/defprojection.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/4bbef68be50d...268423724700
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 270694db49be35512f0e1161334146c2fd2cc3b4
https://github.com/acl2/acl2/commit/270694db49be35512f0e1161334146c2fd2cc3b4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Reorder some code.
Put guard verification earlier, as soon as all the theorems it needs are proved.
Commit: 533c78c3c6fda4f453966df7149e446ad7448777
https://github.com/acl2/acl2/commit/533c78c3c6fda4f453966df7149e446ad7448777
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Fix some `defret-mutual` names.
Commit: af47c9e42b336fb0ef3cf6eb158344e40aa1df22
https://github.com/acl2/acl2/commit/af47c9e42b336fb0ef3cf6eb158344e40aa1df22
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-09 (Fri, 09 Jan 2026)
Changed paths:
M acl2-init.lisp
Log Message:
-----------
Disable xref recording in SBCL.
This didn't noticeably affect "make regression-everything" time (using -j 20 on Linux):
;;; Previous (Jan. 7):
97642.058u 6791.411s 1:52:23.62 1548.6% 0+0k 4056816+11973888io 30pf+0w
;;; New:
97399.966u 6992.549s 1:51:44.33 1557.0% 0+0k 3353848+12250952io 31pf+0w
I added the following comment in acl2-init.lisp to explain the change,
which was contributed by Jim White (thanks!).
; The following was contributed by Jim White, who used Copilot on 1/8/2026 to
; suggest the following addition to prevent raw Lisp errors when certifying the
; following with SBCL 2.9.11 on ARM64 (Ubuntu 24.04.3 LTS running in Docker
; container): demos/congruent-stobjs-book, demos/brr-test-book,
; demos/refinement-failure-test-book, demos/brr-free-variables-book, and
; workshops/2023/kaufmann-moore/brr-book. If SBCL bug #2137765 is fixed
; (https://bugs.launchpad.net/sbcl/+bug/2137765), then we might remove this
; change sometime later.
Commit: a2672b98a1e39194eff59483fbf5697ce6587d45
https://github.com/acl2/acl2/commit/a2672b98a1e39194eff59483fbf5697ce6587d45
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-09 (Fri, 09 Jan 2026)
Changed paths:
M acl2-init.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/including.c
M books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/text.c
Log Message:
-----------
Merge.
Commit: 466cd060dafeb08e9e5fadd09170817c0626b923
https://github.com/acl2/acl2/commit/466cd060dafeb08e9e5fadd09170817c0626b923
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Take fixtype from library.
Commit: 42d5d485f67d5adc889e1dcf9b67bfebd65b3ddb
https://github.com/acl2/acl2/commit/42d5d485f67d5adc889e1dcf9b67bfebd65b3ddb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Simplify some hints.
This is already enabled locally to the `defsection`.
Commit: d4411252f926f9bbf081469aca7f2fe0f948fe60
https://github.com/acl2/acl2/commit/d4411252f926f9bbf081469aca7f2fe0f948fe60
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Fix doc.
Commit: 634a57fd1ab0c1d6f7033494101f4783a11fa5e3
https://github.com/acl2/acl2/commit/634a57fd1ab0c1d6f7033494101f4783a11fa5e3
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-top.lisp
Log Message:
-----------
For hol-in-acl2 library: tweaked eval_poly example, and changed ex1 example to be much more interesting.
Thanks to Konrad Slind for running the translator to get this
extension of the ex1 example.
Commit: 78f209a2e9fcdbe5840d043d5669369872d543f4
https://github.com/acl2/acl2/commit/78f209a2e9fcdbe5840d043d5669369872d543f4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-top.lisp
Log Message:
-----------
Merge.
Commit: 5ac06760aeaea56329a88cab544a14837f1ad4aa
https://github.com/acl2/acl2/commit/5ac06760aeaea56329a88cab544a14837f1ad4aa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Extend some preprocessor data structures.
Add markers used for preventing recursive macro expansion and for handling the
`##` operator.
Commit: 0f3d5a9870deb5a82ea1317a6bd973950d65a5be
https://github.com/acl2/acl2/commit/0f3d5a9870deb5a82ea1317a6bd973950d65a5be
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-top.lisp
Log Message:
-----------
Merge.
Commit: 692e6a261f9d0f810e43630605b106992628fc09
https://github.com/acl2/acl2/commit/692e6a261f9d0f810e43630605b106992628fc09
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Abbreviate some names.
Commit: a8b9cbdb970af8aa3d62ed93aa8c04d69106cf7e
https://github.com/acl2/acl2/commit/a8b9cbdb970af8aa3d62ed93aa8c04d69106cf7e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Simplify some hints.
This is locally enabled.
Commit: edcff5efd6e74c4146dbae6673a34f86aed994e6
https://github.com/acl2/acl2/commit/edcff5efd6e74c4146dbae6673a34f86aed994e6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Simplify some hints.
This is still auto-enabled by `defstobj`, until it is disabled at the end of the
`defsection`.
Commit: e26e91df44ed97bffdcce9e17d01fb056da45e6c
https://github.com/acl2/acl2/commit/e26e91df44ed97bffdcce9e17d01fb056da45e6c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Update some doc to new nomenclature.
Commit: d89f35735502a65480b8606112decd36204b35ed
https://github.com/acl2/acl2/commit/d89f35735502a65480b8606112decd36204b35ed
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Revise preprocessing lexemes in stobj.
Use a simple list of lexmarks. This can be turned into an array if efficiency is
an issue, but we don't need the back-and-forth of read/unread lexemes as we do
for tokens (in the parser) and for characters (in the parser and preprocessor).
Commit: 63ca027466fcf8cb25869bd807000a1006bc7d40
https://github.com/acl2/acl2/commit/63ca027466fcf8cb25869bd807000a1006bc7d40
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
Log Message:
-----------
[C$] Rename a funcion.
Commit: 54939142fc2c46e05df2360825f45bf45ecd1610
https://github.com/acl2/acl2/commit/54939142fc2c46e05df2360825f45bf45ecd1610
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
Log Message:
-----------
[C$] Rename function.
Commit: 56fa21aa16d544e6cb1c95c2921ea2b751f45f96
https://github.com/acl2/acl2/commit/56fa21aa16d544e6cb1c95c2921ea2b751f45f96
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Move a function.
Commit: c59a2c30e0ac78173df413c99f20dfe80d7c89e5
https://github.com/acl2/acl2/commit/c59a2c30e0ac78173df413c99f20dfe80d7c89e5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add and use an operation on preprocessing states.
Commit: 2324bca07fc296fadb3f9a92891bfb4b0d1b3b40
https://github.com/acl2/acl2/commit/2324bca07fc296fadb3f9a92891bfb4b0d1b3b40
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Add missing stobj update.
Commit: db2ba721e37bcefea123712c102dba26224a0a51
https://github.com/acl2/acl2/commit/db2ba721e37bcefea123712c102dba26224a0a51
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Remove list fixtype no longer needed.
Commit: efd30628c83e0440befb7edcbd7885d7d5785152
https://github.com/acl2/acl2/commit/efd30628c83e0440befb7edcbd7885d7d5785152
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Eliminate a data structure no longer needed.
We "inline" lexeme and span into a lexmark. We also make the span optional.
Commit: 5282f27b973d3be9faf0c0cd697292a0a50169a4
https://github.com/acl2/acl2/commit/5282f27b973d3be9faf0c0cd697292a0a50169a4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Require spans in lexmarks that are lexemes.
Commit: 9fcb317a2cd13186732121388db829f22d76f555
https://github.com/acl2/acl2/commit/9fcb317a2cd13186732121388db829f22d76f555
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Remove theorems no longer needed.
Commit: fc6636d73bd535a97b28f3baf0b8cf65b8d8a0ab
https://github.com/acl2/acl2/commit/fc6636d73bd535a97b28f3baf0b8cf65b8d8a0ab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
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/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
Log Message:
-----------
[C$] Streamline handling of line comments.
Exclude the ending new line from the line comment lexeme. This makes for a more
uniform treatment of new lines.
Commit: cce802edcf32aaddf223df996dcea7bcf8437593
https://github.com/acl2/acl2/commit/cce802edcf32aaddf223df996dcea7bcf8437593
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Make all stobj readers fixing.
Commit: 924b1c7247a4f512ca6f80c0c1f44efad86a6bf2
https://github.com/acl2/acl2/commit/924b1c7247a4f512ca6f80c0c1f44efad86a6bf2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Have all `ppstate` writes fix their inputs.
Commit: ae5fa114bbcbf3a99cb283f75c39b003cf1a11ba
https://github.com/acl2/acl2/commit/ae5fa114bbcbf3a99cb283f75c39b003cf1a11ba
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Factor some enablements.
Commit: c3b7b27665cada7904a8c4d0354a9d5849e48a91
https://github.com/acl2/acl2/commit/c3b7b27665cada7904a8c4d0354a9d5849e48a91
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
Log Message:
-----------
[C$] Add a theorem.
Commit: 27b60c5a3d36fdbb315b07e84258f64272ac5808
https://github.com/acl2/acl2/commit/27b60c5a3d36fdbb315b07e84258f64272ac5808
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Factor some enablements.
Commit: a1073e65c302878283b8ae5870f9b78531df9cfc
https://github.com/acl2/acl2/commit/a1073e65c302878283b8ae5870f9b78531df9cfc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Factor more enablements.
Commit: 302e1e34be088e2e4750aba391512102fa8ba509
https://github.com/acl2/acl2/commit/302e1e34be088e2e4750aba391512102fa8ba509
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Consolidate some hints.
Commit: 0279bacc8f232262c38ae68e568c17d36482658a
https://github.com/acl2/acl2/commit/0279bacc8f232262c38ae68e568c17d36482658a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Add a theorem.
Commit: 9f674c67ce656cebbd962eb7e58cc735ecf8c436
https://github.com/acl2/acl2/commit/9f674c67ce656cebbd962eb7e58cc735ecf8c436
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Remove redundant hints.
Commit: 4e6546503c1a2739ccb7e3833abb83a96a7b245f
https://github.com/acl2/acl2/commit/4e6546503c1a2739ccb7e3833abb83a96a7b245f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Remove unnecessary hint.
Commit: ef3d6b4e76ce9f918b977775485fc9486a6257d1
https://github.com/acl2/acl2/commit/ef3d6b4e76ce9f918b977775485fc9486a6257d1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/std/util/defprojection.lisp
Log Message:
-----------
[Std/util] Fix doc.
Commit: c49e4f7673537e0fd68cf28a22f42317f351f787
https://github.com/acl2/acl2/commit/c49e4f7673537e0fd68cf28a22f42317f351f787
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/atc/generation.lisp
A books/kestrel/c/atc/limits.lisp
Log Message:
-----------
[ATC] Add a data structure for limits.
Commit: 78057776cd527f9ff91bd549f6b155d3f7232144
https://github.com/acl2/acl2/commit/78057776cd527f9ff91bd549f6b155d3f7232144
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Add some fixing theorems.
Commit: ba6d16df703a0a5601f552712f819ce70b799b01
https://github.com/acl2/acl2/commit/ba6d16df703a0a5601f552712f819ce70b799b01
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/proof-generation.lisp
Log Message:
-----------
[C2C] Extend some theorems.
Commit: 86abf8450679cbad5bb7fa3917bcfdac9a367922
https://github.com/acl2/acl2/commit/86abf8450679cbad5bb7fa3917bcfdac9a367922
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Simplify some code.
Commit: 6264a7c6db8e5e72cdc753a516c8505d00fa495f
https://github.com/acl2/acl2/commit/6264a7c6db8e5e72cdc753a516c8505d00fa495f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
Merge.
Commit: 268423724700e2858c032161a7313b574e285f24
https://github.com/acl2/acl2/commit/268423724700e2858c032161a7313b574e285f24
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/kestrel/c/atc/generation.lisp
A books/kestrel/c/atc/limits.lisp
M books/std/util/defprojection.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/4bbef68be50d...268423724700
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Jan 13, 2026, 2:06:02 PM (8 days ago) Jan 13
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: b16e9d4582284471bdb1101eeb3bc439b31d2d80
https://github.com/acl2/acl2/commit/b16e9d4582284471bdb1101eeb3bc439b31d2d80
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/atc/limits.lisp
Log Message:
-----------
[ATC] Fix XDOC link.
Compare: https://github.com/acl2/acl2/compare/634a57fd1ab0...b16e9d458228
Home: https://github.com/acl2/acl2
Commit: 270694db49be35512f0e1161334146c2fd2cc3b4
https://github.com/acl2/acl2/commit/270694db49be35512f0e1161334146c2fd2cc3b4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Reorder some code.
Put guard verification earlier, as soon as all the theorems it needs are proved.
Commit: 533c78c3c6fda4f453966df7149e446ad7448777
https://github.com/acl2/acl2/commit/533c78c3c6fda4f453966df7149e446ad7448777
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Fix some `defret-mutual` names.
Commit: 270694db49be35512f0e1161334146c2fd2cc3b4
https://github.com/acl2/acl2/commit/270694db49be35512f0e1161334146c2fd2cc3b4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Reorder some code.
Put guard verification earlier, as soon as all the theorems it needs are proved.
Commit: 533c78c3c6fda4f453966df7149e446ad7448777
https://github.com/acl2/acl2/commit/533c78c3c6fda4f453966df7149e446ad7448777
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Fix some `defret-mutual` names.
https://github.com/acl2/acl2/commit/b16e9d4582284471bdb1101eeb3bc439b31d2d80
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-13 (Tue, 13 Jan 2026)
Changed paths:
M books/kestrel/c/atc/limits.lisp
Log Message:
-----------
[ATC] Fix XDOC link.
Compare: https://github.com/acl2/acl2/compare/634a57fd1ab0...b16e9d458228
Alessandro Coglio
Jan 13, 2026, 2:06:38 PM (8 days ago) Jan 13
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Jan 13, 2026, 3:19:06 PM (8 days ago) Jan 13
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Compare: https://github.com/acl2/acl2/compare/4bbef68be50d...b16e9d458228
Home: https://github.com/acl2/acl2
Commit: 270694db49be35512f0e1161334146c2fd2cc3b4
https://github.com/acl2/acl2/commit/270694db49be35512f0e1161334146c2fd2cc3b4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Reorder some code.
Put guard verification earlier, as soon as all the theorems it needs are proved.
Commit: 533c78c3c6fda4f453966df7149e446ad7448777
https://github.com/acl2/acl2/commit/533c78c3c6fda4f453966df7149e446ad7448777
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Fix some `defret-mutual` names.
Commit: 270694db49be35512f0e1161334146c2fd2cc3b4
https://github.com/acl2/acl2/commit/270694db49be35512f0e1161334146c2fd2cc3b4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Reorder some code.
Put guard verification earlier, as soon as all the theorems it needs are proved.
Commit: 533c78c3c6fda4f453966df7149e446ad7448777
https://github.com/acl2/acl2/commit/533c78c3c6fda4f453966df7149e446ad7448777
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-01-08 (Thu, 08 Jan 2026)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
Log Message:
-----------
[C2C] Fix some `defret-mutual` names.
Commit: af47c9e42b336fb0ef3cf6eb158344e40aa1df22
https://github.com/acl2/acl2/commit/af47c9e42b336fb0ef3cf6eb158344e40aa1df22
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
https://github.com/acl2/acl2/commit/af47c9e42b336fb0ef3cf6eb158344e40aa1df22
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-01-09 (Fri, 09 Jan 2026)
Changed paths:
M acl2-init.lisp
Changed paths:
M acl2-init.lisp
Log Message:
-----------
Disable xref recording in SBCL.
This didn't noticeably affect "make regression-everything" time (using -j 20 on Linux):
;;; Previous (Jan. 7):
97642.058u 6791.411s 1:52:23.62 1548.6% 0+0k 4056816+11973888io 30pf+0w
;;; New:
97399.966u 6992.549s 1:51:44.33 1557.0% 0+0k 3353848+12250952io 31pf+0w
I added the following comment in acl2-init.lisp to explain the change,
which was contributed by Jim White (thanks!).
; The following was contributed by Jim White, who used Copilot on 1/8/2026 to
; suggest the following addition to prevent raw Lisp errors when certifying the
; following with SBCL 2.9.11 on ARM64 (Ubuntu 24.04.3 LTS running in Docker
; container): demos/congruent-stobjs-book, demos/brr-test-book,
; demos/refinement-failure-test-book, demos/brr-free-variables-book, and
; workshops/2023/kaufmann-moore/brr-book. If SBCL bug #2137765 is fixed
; (https://bugs.launchpad.net/sbcl/+bug/2137765), then we might remove this
; change sometime later.
-----------
Disable xref recording in SBCL.
This didn't noticeably affect "make regression-everything" time (using -j 20 on Linux):
;;; Previous (Jan. 7):
97642.058u 6791.411s 1:52:23.62 1548.6% 0+0k 4056816+11973888io 30pf+0w
;;; New:
97399.966u 6992.549s 1:51:44.33 1557.0% 0+0k 3353848+12250952io 31pf+0w
I added the following comment in acl2-init.lisp to explain the change,
which was contributed by Jim White (thanks!).
; The following was contributed by Jim White, who used Copilot on 1/8/2026 to
; suggest the following addition to prevent raw Lisp errors when certifying the
; following with SBCL 2.9.11 on ARM64 (Ubuntu 24.04.3 LTS running in Docker
; container): demos/congruent-stobjs-book, demos/brr-test-book,
; demos/refinement-failure-test-book, demos/brr-free-variables-book, and
; workshops/2023/kaufmann-moore/brr-book. If SBCL bug #2137765 is fixed
; (https://bugs.launchpad.net/sbcl/+bug/2137765), then we might remove this
; change sometime later.
Commit: 634a57fd1ab0c1d6f7033494101f4783a11fa5e3
https://github.com/acl2/acl2/commit/634a57fd1ab0c1d6f7033494101f4783a11fa5e3
Author: Matt Kaufmann <matthew.j...@gmail.com>
https://github.com/acl2/acl2/commit/634a57fd1ab0c1d6f7033494101f4783a11fa5e3
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-01-12 (Mon, 12 Jan 2026)
Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-top.lisp
Log Message:
-----------
Changed paths:
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-top.lisp
Log Message:
-----------
For hol-in-acl2 library: tweaked eval_poly example, and changed ex1 example to be much more interesting.
Thanks to Konrad Slind for running the translator to get this
extension of the ex1 example.
Thanks to Konrad Slind for running the translator to get this
extension of the ex1 example.
Reply all
Reply to author
Forward
0 new messages