Branch: refs/heads/testing-acl2s
Home:
https://github.com/acl2/acl2
Commit: 2e64636271d7c26aa2dada00c3043285bbcf3b0a
https://github.com/acl2/acl2/commit/2e64636271d7c26aa2dada00c3043285bbcf3b0a
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)
Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/risc-v/unroller.lisp
Log Message:
-----------
[axe] Improve packages.
Commit: 4291655cab84658009210d5b3cacebee8dedaced
https://github.com/acl2/acl2/commit/4291655cab84658009210d5b3cacebee8dedaced
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)
Changed paths:
M books/kestrel/axe/logops-rules-axe.lisp
M books/kestrel/axe/risc-v/lifter-rules.lisp
M books/kestrel/axe/risc-v/unroller.lisp
Log Message:
-----------
[axe] Move some rules.
Commit: 6828efda09466767d89c87434266b1b85f0fae44
https://github.com/acl2/acl2/commit/6828efda09466767d89c87434266b1b85f0fae44
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)
Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/x86/support-bv.lisp
Log Message:
-----------
[axe/x86] Add ash-constant-opener.
Commit: 6da6cfeee8704ad0cb9c79cfd9f008e6a59d8ba1
https://github.com/acl2/acl2/commit/6da6cfeee8704ad0cb9c79cfd9f008e6a59d8ba1
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-04 (Thu, 04 Dec 2025)
Changed paths:
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/known-booleans.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/bv/trim-intro-rules.lisp
A books/kestrel/c/atc/pure-expression-execution.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-call.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/atc/tutorial.lisp
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
M books/kestrel/c/language/execution-without-function-calls.lisp
M books/kestrel/c/language/object-type-preservation.lisp
R books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/read-and-write.lisp
Log Message:
-----------
Merge.
Commit: e206c13e1ae2abb31d19663c6b6d03104ca34781
https://github.com/acl2/acl2/commit/e206c13e1ae2abb31d19663c6b6d03104ca34781
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-05 (Fri, 05 Dec 2025)
Changed paths:
M books/kestrel/fty/fty-set.lisp
Log Message:
-----------
[FTY] Improve `defset`.
Make some generated proofs more robust.
Enable a function in two proofs, to avoid an apparent dependency on tau.
Commit: 631e4d43193177c7910aae2f1cc3296434b3561f
https://github.com/acl2/acl2/commit/631e4d43193177c7910aae2f1cc3296434b3561f
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-05 (Fri, 05 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/file-paths.lisp
M books/kestrel/c/syntax/files.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-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
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
Merge.
Commit: ebb5154ab13c6c133d83251e182b7c474314e6b4
https://github.com/acl2/acl2/commit/ebb5154ab13c6c133d83251e182b7c474314e6b4
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-05 (Fri, 05 Dec 2025)
Changed paths:
M books/kestrel/axe/arithmetic-rules-axe.lisp
M books/kestrel/axe/basic-rules.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
Log Message:
-----------
Merge.
Commit: 151f0fdf43876839b5e3680b5ca88ba57a3f7e14
https://github.com/acl2/acl2/commit/151f0fdf43876839b5e3680b5ca88ba57a3f7e14
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/axe/arithmetic-rules-axe.lisp
M books/kestrel/axe/basic-rules.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-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
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
Merge.
Commit: 5965f1165a25f6cb980a6fac7e7b9d32b63a0aa8
https://github.com/acl2/acl2/commit/5965f1165a25f6cb980a6fac7e7b9d32b63a0aa8
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/file-paths.lisp
Log Message:
-----------
[C$] Use controlled configuration.
Commit: 41257c092632eff9c3fdfa9663a5bd476db309c2
https://github.com/acl2/acl2/commit/41257c092632eff9c3fdfa9663a5bd476db309c2
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/files.lisp
Log Message:
-----------
[C$] Shorten some code.
Commit: 4bbd83044438a3e0691c09cec28b088ff0287244
https://github.com/acl2/acl2/commit/4bbd83044438a3e0691c09cec28b088ff0287244
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Include two more books nneded for local development.
Commit: 151d27321ca1adb9ed5e96635d683d4303dd727a
https://github.com/acl2/acl2/commit/151d27321ca1adb9ed5e96635d683d4303dd727a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Tweak for consistency.
Remove "historical" comment no longer needed.
Move certification-related form at the end of the "preamble".
Commit: 66e029b7c900484a8c90488b096e529459d4bf20
https://github.com/acl2/acl2/commit/66e029b7c900484a8c90488b096e529459d4bf20
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Remove book inclusion now redundant.
Commit: 6add17b208012eccb1c3c07ccba325ed35665f10
https://github.com/acl2/acl2/commit/6add17b208012eccb1c3c07ccba325ed35665f10
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Remove local theorem no longer needed.
Now that `fty::defset` has been improved to generate more robust proofs that do
not necessitate tau.
Commit: 744b4e7408f3995b879bf5ca9be97ddabeaed6ec
https://github.com/acl2/acl2/commit/744b4e7408f3995b879bf5ca9be97ddabeaed6ec
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Remove induction exception no longer needed.
Now the `fty` macros should generate the needed induction hints.
Commit: 702b7fe90517bd471f6dc5c3cd3cfa9b7e8ea0cc
https://github.com/acl2/acl2/commit/702b7fe90517bd471f6dc5c3cd3cfa9b7e8ea0cc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
Log Message:
-----------
[C$] Localize some hints.
Commit: e30a86b5dfb91c62132333fc3dcea039e27a710d
https://github.com/acl2/acl2/commit/e30a86b5dfb91c62132333fc3dcea039e27a710d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
Log Message:
-----------
[C$] Use controlled configuration.
Commit: 775f8129c0f51a0eb64a628be0f6f6e44299ad69
https://github.com/acl2/acl2/commit/775f8129c0f51a0eb64a628be0f6f6e44299ad69
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
Log Message:
-----------
[C$] Avoid redundant book inclusion.
Also reorder forms in preamble for consistency.
Commit: 7b076380542fcc68b542ab949b863cff27eb1de3
https://github.com/acl2/acl2/commit/7b076380542fcc68b542ab949b863cff27eb1de3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
Log Message:
-----------
[C$] Shorten some code.
Commit: 07cae5f2951da9ecc97119f7ced93b3828387eaf
https://github.com/acl2/acl2/commit/07cae5f2951da9ecc97119f7ced93b3828387eaf
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/code-ensembles.lisp
Log Message:
-----------
[C$] Remove redundant book inclusion.
Commit: 9479b9b6c911c8cad9b19e29112140a85ca90aa3
https://github.com/acl2/acl2/commit/9479b9b6c911c8cad9b19e29112140a85ca90aa3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/type-specifier-lists.lisp
Log Message:
-----------
[C$] Shorten some code.
Commit: 4b5d6e203f32350f80241aa32b96aff78e384073
https://github.com/acl2/acl2/commit/4b5d6e203f32350f80241aa32b96aff78e384073
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/storage-specifier-lists.lisp
Log Message:
-----------
[C$] Shorten some code.
Commit: f9693e8e4dc46fa6a9af3bf1cccd748021237a21
https://github.com/acl2/acl2/commit/f9693e8e4dc46fa6a9af3bf1cccd748021237a21
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstraction-mapping.lisp
Log Message:
-----------
[C$] Shorten some code.
Commit: fabd61e448f1627acc7853974bc59509efc71261
https://github.com/acl2/acl2/commit/fabd61e448f1627acc7853974bc59509efc71261
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/parser-states.lisp
Log Message:
-----------
[C$] Use controlled configuration.
Commit: a82e9a4ad54bd244876efa334b586bdcc141122a
https://github.com/acl2/acl2/commit/a82e9a4ad54bd244876efa334b586bdcc141122a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/parser-messages.lisp
Log Message:
-----------
[C$] Shorten some code.
Commit: 390785d395568da2db7f821b74f90c91b96dbfdb
https://github.com/acl2/acl2/commit/390785d395568da2db7f821b74f90c91b96dbfdb
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-06 (Sat, 06 Dec 2025)
Changed paths:
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp
Log Message:
-----------
[aleo] Update comment on GCL issue.
Commit: 0d5b816cc3265c08a45a94386b1f4340c5cced82
https://github.com/acl2/acl2/commit/0d5b816cc3265c08a45a94386b1f4340c5cced82
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-07 (Sun, 07 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/lexer.lisp
Log Message:
-----------
[C$] Tweak some fixing theorems.
Commit: 443210de6bfc80c65af9f42c3f441a30bc709f45
https://github.com/acl2/acl2/commit/443210de6bfc80c65af9f42c3f441a30bc709f45
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-07 (Sun, 07 Dec 2025)
Changed paths:
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp
Log Message:
-----------
Merge.
Commit: a7fcf343836d8d7e60bd389f0667d469dce7a96d
https://github.com/acl2/acl2/commit/a7fcf343836d8d7e60bd389f0667d469dce7a96d
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-07 (Sun, 07 Dec 2025)
Changed paths:
M books/kestrel/x86/support-bv.lisp
Log Message:
-----------
[x86] Comment out unneeded rules.
Commit: 7001770ad5a5b19f93fede6f3b2762ec598be2ed
https://github.com/acl2/acl2/commit/7001770ad5a5b19f93fede6f3b2762ec598be2ed
Author: Matt Kaufmann <
matthew.j...@gmail.com>
Date: 2025-12-07 (Sun, 07 Dec 2025)
Changed paths:
M apply.lisp
M axioms.lisp
M basis-a.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/projects/apply/semi-concrete-do-inductions-log.txt
M books/system/apply/loop-scions.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M translate.lisp
Log Message:
-----------
Multiple changes (discussed further below). (1) Modified swap-stobjs to cause error when exactly one argument is a live stobj. (2) Allow DO loop$ expressions with no WITH clauses. (3) Fixed stobj-returning do$ to handle measures in a single-threaded way. (4,7) Avoid errors for some other stobj-returning DO loop$ expressions. (5) Do more complete job of avoiding certain calls (including swap-stobj and return-last) in the top-level loop. (6) Restore prohibition of stobj creator calls except in non-evaluation contexts like theorems.
Thanks to J for collaboration on (many of) these changes.
(1) Quoting an existing item in :DOC note-8-7, except that the
"Technical Note" at the end is new; it describes a change to
swap-stobjs made with this commit.
Fixed a soundness bug based on the use of [swap-stobjs] on two
[stobj]s of which one is ``live''. See [live-stobj-in-proof].
Thanks to Sol Swords for reporting this bug, including an example
and analysis of possible fixes in his report. (Technical Note. We
have added code to check for live [stobj]s in proofs, which was
sufficient to fix the bug. But the situation described above is
caught by a change to swap-stobjs, which now signals an error in
the relevant case (exactly one live stobj input).)
Quoting :DOC note-8-7 (preceding each by a number, for reference above
and/or below):
(2)
DO [Loop$] expressions (see [do-loop$]) are now allowed that have no
WITH clauses. Formerly, an expression (loop$ do ...) caused an
error with a rather nonsensical message.
(3)
For a DO [loop$] expression returning a [stobj] that participates in
its measure, it was possible to get an inappropriate runtime
measure error. (An example appears in a comment in the definition
of [do$] in the ACL2 sources.) This bug has been fixed by
modifying the definition of [do$] to respect singled-threadedness.
(4)
A DO [loop$] expression returning a [stobj] could cause a confusing
error; see ACL2 source function chk-for-live-stobj for an example.
This bug has been fixed so that no error occurs.
(5)
ACL2 did an incomplete job of excluding certain forms from being
evaluated in the top-level loop, including calls of [swap-stobjs],
parallelism primitives ([pand], [por], [pargs], and [plet]) when
parallel evaluation is enabled (ACL2(p) only), and [return-last]
calls. For example, no error was signalled by the following, even
though the two stobjs were not swapped (as shown below).
(defstobj st1 (fld1))
(defstobj st2 (fld2) :congruent-to st1)
(update-fld1 1 st1)
(update-fld2 2 st2)
(assert-event (and (equal (fld1 st1) 1) (equal (fld2 st2) 2)))
; The following is equivalent to (swap-stobjs st1 st2), and it
; now causes an error but it did not cause an error in Version 8.6:
(mv-let (st1 st2) (swap-stobjs st1 st2) (mv st1 st2))
; The following succeeds, showing that st1 and st2 were not actually swapped:
(assert-event (and (equal (fld1 st1) 1) (equal (fld2 st2) 2)))
This bug has been fixed.
(6)
[Stobj] creators are once again disallowed in execution contexts (but
are still allowed in theorems). This requirement was relaxed
(perhaps inadvertently) in Version 8.5. The following example
shows a problem with relaxing that restriction, as these events are
accepted in Versions 8.5 and 8.6, but no longer.
(defstobj st fld)
; Admitted in Versions 8.5 and 8.6, but no longer:
(defun foo () (declare (xargs :guard t)) (create-st))
(update-fld 3 st)
(assert-event (equal (fld st) 3))
; Should not change global value of st:
(foo)
; But (fld st) has indeed changed:
(assert-event (equal (fld st) nil))
Regarding Item #6 just above on stobj creators:
An attempt to call a stobj creator in the top-level loop or a defun
body will now cause an error such as the one displayed below, which
explains how defun-nx and non-exec can be used to avoid the error.
Indeed, a couple of books failed certification after this change, but
I fixed that by wrapping two creator calls in (non-exec ...), which is
presumably harmless since these were in the :logic fields of mbe
calls.
ACL2 Error [Translate] in TOP-LEVEL: It is illegal to call CREATE-ST
in this context because it is a stobj creator. Calls of stobj creators
cannot appear in top-level loop inputs or in function bodies (unless
in the scope of defun-nx or non-exec), although they may be called
in theorems. Note: this error occurred in the context (CREATE-ST).
(7) The following caused a raw Lisp error in recent ACL2 github
versions (though not in ACL2 Version 8.6), but now succeeds.
(include-book "projects/apply/top" :dir :system)
(defstobj st fld)
(defwarrant stp)
(defwarrant fld)
(defwarrant update-fld)
(update-fld '(a b c d) st)
(loop$ with x = '(a b c)
do
:guard (stp st) ; needed for producing an error in recent versions
:values (st)
(cond ((atom x)
(return st))
(t (progn (setq x (cdr x))
(setq st
(update-fld (car x) st))))))
Commit: 4e8a5eefb0374b40b97e816fddbff56009ce5e6f
https://github.com/acl2/acl2/commit/4e8a5eefb0374b40b97e816fddbff56009ce5e6f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)
Changed paths:
M apply.lisp
M axioms.lisp
M basis-a.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/logops-rules-axe.lisp
M books/kestrel/axe/risc-v/lifter-rules.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/x86/support-bv.lisp
M books/projects/aleo/vm/circuits/axe/blake2s1round.old.lisp
M books/projects/apply/semi-concrete-do-inductions-log.txt
M books/system/apply/loop-scions.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M translate.lisp
Log Message:
-----------
Merge.
Commit: bc72cf0228c4a14206754558909888a9cab59a84
https://github.com/acl2/acl2/commit/bc72cf0228c4a14206754558909888a9cab59a84
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)
Changed paths:
A books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Refactor preprocessor.
Move preprocessor states to dedicated file and topic.
Commit: f5e194c04463b39178bfa048e1be98bbeafbe82d
https://github.com/acl2/acl2/commit/f5e194c04463b39178bfa048e1be98bbeafbe82d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)
Changed paths:
A books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Refactor preprocessor.
Put preprocessor messages into dedicated file and topic.
Commit: f9102d508746d8578bf147b7f83640372196212c
https://github.com/acl2/acl2/commit/f9102d508746d8578bf147b7f83640372196212c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Refactor preprocessor.
Put reader into dedicated file and topic.
Commit: 6ef28d4dfbd5d658c5e330294eba26be4c8b8ed3
https://github.com/acl2/acl2/commit/6ef28d4dfbd5d658c5e330294eba26be4c8b8ed3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)
Changed paths:
A books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Refactor preprocessor.
Put lexer component into dedicated file and topic.
Commit: 396e081039c2b004634986e651cea807b93bd4b8
https://github.com/acl2/acl2/commit/396e081039c2b004634986e651cea807b93bd4b8
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve preprocessor code.
Rename a function.
Remove some now-unnecessary book inclusions.
Remove some now-unnecessary local forms.
Commit: a84f250f95dface3097fcfcaf8680c18a3b67d5a
https://github.com/acl2/acl2/commit/a84f250f95dface3097fcfcaf8680c18a3b67d5a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)
Changed paths:
A books/kestrel/c/syntax/preprocessor-reader.lisp
Log Message:
-----------
[C$] Add forgotten file.
Commit: 739470fe045f7eabfa74f85e1d6a84372242fa2f
https://github.com/acl2/acl2/commit/739470fe045f7eabfa74f85e1d6a84372242fa2f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)
Changed paths:
A books/kestrel/c/syntax/tests/preprocessor-reader.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Refactor some preprocessor tests.
Put the preprocessor's reader tests in a separate file.
Commit: 57346b08f114c3b03dafa5e6921c1d84e8082588
https://github.com/acl2/acl2/commit/57346b08f114c3b03dafa5e6921c1d84e8082588
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)
Changed paths:
A books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
R books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Rename a preprocessor test file.
Commit: f4a9f407a1843ea98cf950c0c1745c81b7e77572
https://github.com/acl2/acl2/commit/f4a9f407a1843ea98cf950c0c1745c81b7e77572
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-08 (Mon, 08 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Fix capitalization in doc.
Commit: 1c0c49d86781185e81d2408456d06f9981f029b5
https://github.com/acl2/acl2/commit/1c0c49d86781185e81d2408456d06f9981f029b5
Author: Matt Kaufmann <
kauf...@cs.utexas.edu>
Date: 2025-12-08 (Mon, 08 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:
-----------
Incorporated small :DOC topic edits from J.
Commit: fd7f618d2ed2e141f8f518822daf00654a4a2377
https://github.com/acl2/acl2/commit/fd7f618d2ed2e141f8f518822daf00654a4a2377
Author: Matt Kaufmann <
kauf...@cs.utexas.edu>
Date: 2025-12-09 (Tue, 09 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:
-----------
Incorporated more :DOC topic improvements from J, especially regarding expressions (loop$ do ...).
Commit: 5a1033864c4c3fd8cd2521f3d1cf87baad6e739c
https://github.com/acl2/acl2/commit/5a1033864c4c3fd8cd2521f3d1cf87baad6e739c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 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:
-----------
Merge.
Commit: 56b65dffac4800bf58184ee45204b1b53c27d026
https://github.com/acl2/acl2/commit/56b65dffac4800bf58184ee45204b1b53c27d026
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: e0f5712f39f7db496258501e4858edc6dc540b1f
https://github.com/acl2/acl2/commit/e0f5712f39f7db496258501e4858edc6dc540b1f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 90e3d40cf6487ab38e0e3bd209b39e92c1052aa3
https://github.com/acl2/acl2/commit/90e3d40cf6487ab38e0e3bd209b39e92c1052aa3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 3632829920bf5398cd8b9b7031de58011c62d288
https://github.com/acl2/acl2/commit/3632829920bf5398cd8b9b7031de58011c62d288
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 2cd3cecf747cdcc7bc07be8e2f92f06fafad3462
https://github.com/acl2/acl2/commit/2cd3cecf747cdcc7bc07be8e2f92f06fafad3462
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 86c39f723f602e9414708fe45ea09ccaaf44900c
https://github.com/acl2/acl2/commit/86c39f723f602e9414708fe45ea09ccaaf44900c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
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/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation.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.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 535fb11fec14e5b7547cc26f2b90efc131b11770
https://github.com/acl2/acl2/commit/535fb11fec14e5b7547cc26f2b90efc131b11770
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
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/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 10e03fcc6d3e233a2c312ed658f19356178ddb7e
https://github.com/acl2/acl2/commit/10e03fcc6d3e233a2c312ed658f19356178ddb7e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
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/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.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.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 90bc353ea901b553cada229f6859a2cfb2d8ae4f
https://github.com/acl2/acl2/commit/90bc353ea901b553cada229f6859a2cfb2d8ae4f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Improve a predicate name.
Commit: 1f9e92a4c878f1b1f46039786d3be361f88a3d17
https://github.com/acl2/acl2/commit/1f9e92a4c878f1b1f46039786d3be361f88a3d17
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve some doc.
Commit: f37a2207fef6ad05db43084e62d1f954e78006ed
https://github.com/acl2/acl2/commit/f37a2207fef6ad05db43084e62d1f954e78006ed
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation.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.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: bb24e6b61b0768cdaebb167fc92d6d3074d5589d
https://github.com/acl2/acl2/commit/bb24e6b61b0768cdaebb167fc92d6d3074d5589d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 091b1379e5c1b4d950a9f916a2a20ecfe24732bc
https://github.com/acl2/acl2/commit/091b1379e5c1b4d950a9f916a2a20ecfe24732bc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
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/constant-propagation.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 5a2a272092287067f43820f51c9f6806a7efafbf
https://github.com/acl2/acl2/commit/5a2a272092287067f43820f51c9f6806a7efafbf
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 3c7605a2bb9ba653ff8bc79d9137a438db83b6be
https://github.com/acl2/acl2/commit/3c7605a2bb9ba653ff8bc79d9137a438db83b6be
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Add some predicates.
Commit: 9d525e0affa6be5dd854a4d513bf20f1726bd31b
https://github.com/acl2/acl2/commit/9d525e0affa6be5dd854a4d513bf20f1726bd31b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Add a function to read a token or newline.
Commit: 38c1c01746a28ac608bcc6e916451ec48704ba3e
https://github.com/acl2/acl2/commit/38c1c01746a28ac608bcc6e916451ec48704ba3e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
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/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 8d707f202755edf5f60cdb71766e289d860560a3
https://github.com/acl2/acl2/commit/8d707f202755edf5f60cdb71766e289d860560a3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-10 (Wed, 10 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 97c0745b1329c595a301fd3e584c333d2fb95f83
https://github.com/acl2/acl2/commit/97c0745b1329c595a301fd3e584c333d2fb95f83
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 8cd4be21666caaad328dd2b4d591030e6e4d9733
https://github.com/acl2/acl2/commit/8cd4be21666caaad328dd2b4d591030e6e4d9733
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 88c9f78da6d0115738455bd17ab28e213c647dc7
https://github.com/acl2/acl2/commit/88c9f78da6d0115738455bd17ab28e213c647dc7
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 818347cc89129f9e431e6a3ffc24575017a7cc05
https://github.com/acl2/acl2/commit/818347cc89129f9e431e6a3ffc24575017a7cc05
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/rename.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
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 9b5f9352497d621087e39fd1863e2c386cf23feb
https://github.com/acl2/acl2/commit/9b5f9352497d621087e39fd1863e2c386cf23feb
Author: Matt Kaufmann <
kauf...@cs.utexas.edu>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
A books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
Log Message:
-----------
Added "-exports" books showing the encapsulate generated by translation of HOL theories to ACL2(zfc)
Commit: 5c2bcedfa1802fdcba082ddfc164246369e59efd
https://github.com/acl2/acl2/commit/5c2bcedfa1802fdcba082ddfc164246369e59efd
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-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
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: e293cff483c5bbf5f2064a597147f597bea7df9f
https://github.com/acl2/acl2/commit/e293cff483c5bbf5f2064a597147f597bea7df9f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
A books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
A books/kestrel/c/syntax/tests/preprocessor-reader.lisp
R books/kestrel/c/syntax/tests/preprocessor.lisp
A books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
Log Message:
-----------
Merge.
Commit: 587b90bd8399d0416d89cd2c3126a14e5ae73d1b
https://github.com/acl2/acl2/commit/587b90bd8399d0416d89cd2c3126a14e5ae73d1b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Layout tweak.
Commit: 4c68fb056287be86e2fe713fbf7b950f3f327013
https://github.com/acl2/acl2/commit/4c68fb056287be86e2fe713fbf7b950f3f327013
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Expand some doc.
Commit: 4af0f2b37dcd0bdba811a5b0624947b36dda8131
https://github.com/acl2/acl2/commit/4af0f2b37dcd0bdba811a5b0624947b36dda8131
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/rename.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
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
A books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
A books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
Log Message:
-----------
Merge.
Commit: 790fe71c8cb5a30be64dabc18a32eb7dc4c2f204
https://github.com/acl2/acl2/commit/790fe71c8cb5a30be64dabc18a32eb7dc4c2f204
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Extend preprocessor states.
Add macro tables, which contain macro definitions.
Also add operations on macro tables.
Commit: 3e15f977f7cf360be8e8cd78eadb2eb87f69f684
https://github.com/acl2/acl2/commit/3e15f977f7cf360be8e8cd78eadb2eb87f69f684
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 9a611fe1e0dbc92835412e63db1c9acf98f11d7c
https://github.com/acl2/acl2/commit/9a611fe1e0dbc92835412e63db1c9acf98f11d7c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 08485a02137c5986de035b4be286f8b39362f876
https://github.com/acl2/acl2/commit/08485a02137c5986de035b4be286f8b39362f876
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 7cf591153f488e5a93fbcd56d3fc1404e41b3e75
https://github.com/acl2/acl2/commit/7cf591153f488e5a93fbcd56d3fc1404e41b3e75
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
Log Message:
-----------
[C$] Improve some AST names.
Commit: 3555bc225e953133a3bf9810d5bfe27369caab8c
https://github.com/acl2/acl2/commit/3555bc225e953133a3bf9810d5bfe27369caab8c
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Remove an operation not needed.
Commit: 354f05074254eb7dd32892cf235cc14f370204df
https://github.com/acl2/acl2/commit/354f05074254eb7dd32892cf235cc14f370204df
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Add top-level structures (with placeholders for code to be fleshed out).
Commit: f6bab48c56729581a327b595cd7b028454aaefd0
https://github.com/acl2/acl2/commit/f6bab48c56729581a327b595cd7b028454aaefd0
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
Log Message:
-----------
Merge.
Commit: 375fd4cb5a88437c75343c5faf632a9574a6f373
https://github.com/acl2/acl2/commit/375fd4cb5a88437c75343c5faf632a9574a6f373
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-11 (Thu, 11 Dec 2025)
Changed paths:
A books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Start printer component of preprocessor.
Use in top-level code of preprocessor.
Commit: 077c81ea93f4516caec17ef58047bc0419020dbc
https://github.com/acl2/acl2/commit/077c81ea93f4516caec17ef58047bc0419020dbc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-12 (Fri, 12 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Remove repeated word in doc.
Commit: d8b64199e432809f4a432c7d5d8870c73ffb8a27
https://github.com/acl2/acl2/commit/d8b64199e432809f4a432c7d5d8870c73ffb8a27
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-12 (Fri, 12 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Expand some doc.
Commit: 63039339c6e5eb38f145d5b4bc28e2a1523ed261
https://github.com/acl2/acl2/commit/63039339c6e5eb38f145d5b4bc28e2a1523ed261
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-12 (Fri, 12 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Make some AST names more consistent with others.
Commit: b7f27d8433ee39ba3fec254bf4b22d4de5252cfe
https://github.com/acl2/acl2/commit/b7f27d8433ee39ba3fec254bf4b22d4de5252cfe
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-12 (Fri, 12 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Log Message:
-----------
[C$] Remove redundant certification instruction.
Commit: e13ced9ab7658900f3b1dba8b42acfbe81743bcc
https://github.com/acl2/acl2/commit/e13ced9ab7658900f3b1dba8b42acfbe81743bcc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-12 (Fri, 12 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-printer.lisp
Log Message:
-----------
[C$] Finish preprocessor's printer.
Commit: efbfc290fe21127cbbf727232eb4cbf8d6b6c2e4
https://github.com/acl2/acl2/commit/efbfc290fe21127cbbf727232eb4cbf8d6b6c2e4
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-12 (Fri, 12 Dec 2025)
Changed paths:
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/statement-generation.lisp
Log Message:
-----------
[ATC] Slightly improve generated limit terms.
Use `+` instead of `binary-+`, which still satisfies `pseudo-termp`, although
the intention was for these to be translated terms. We should eventually move to
untranslated terms anyways, for better readability, and we should combine
constants.
Thanks to Eric Smith for suggesting this improvement.
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.
Commit: bb1a0795b0d3ff9f23a175bdc00222c6071a044c
https://github.com/acl2/acl2/commit/bb1a0795b0d3ff9f23a175bdc00222c6071a044c
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/axe/.sys/unguarde...@useless-runes.lsp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/bv-lists/.sys/bv-array-read...@useless-runes.lsp
M books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
M books/kestrel/x86/read-and-write2.lisp
Log Message:
-----------
[bv-lists] Disable the opener for bv-array-read-chunk-little.
Also remove a duplicate call of defopeners.
Commit: 695ff50fc88e83bc339361eb81f16f4665c4d3a6
https://github.com/acl2/acl2/commit/695ff50fc88e83bc339361eb81f16f4665c4d3a6
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/refine-assumptions.lisp
Log Message:
-----------
[axe] Improve comments.
Commit: eb76ca901700b22fb84ef9a2df6964c96ecf10fa
https://github.com/acl2/acl2/commit/eb76ca901700b22fb84ef9a2df6964c96ecf10fa
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/x86/read-and-write2.lisp
Log Message:
-----------
[axe] Clarify rules.
Commit: c4cd40f1b0decacf2a891dbc13bf3c6ab67b731b
https://github.com/acl2/acl2/commit/c4cd40f1b0decacf2a891dbc13bf3c6ab67b731b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/lexer.lisp
Log Message:
-----------
[C$] Remove some unnecessary hints.
Commit: c6663108855825388fac5dd8e9481ad00dba4540
https://github.com/acl2/acl2/commit/c6663108855825388fac5dd8e9481ad00dba4540
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/lexer.lisp
Log Message:
-----------
[C$] Remove some unnecessary hints, using library theorems.
Commit: f2f255cde35f9b3961446efe7ceb3431c4365215
https://github.com/acl2/acl2/commit/f2f255cde35f9b3961446efe7ceb3431c4365215
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/x86/read-and-write2.lisp
Log Message:
-----------
[axe/x86] Add a rule variant.
Commit: 4de6ff3a5dc5f904015bacd93b56f5d78d0ce656
https://github.com/acl2/acl2/commit/4de6ff3a5dc5f904015bacd93b56f5d78d0ce656
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M apply-prim.lisp
M axioms.lisp
M books/demos/floating-point-log.txt
M books/kestrel/c/syntax/external-preprocessing.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
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
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: 53831c8b283d401338063cd2490a9cd9c4ae9a48
https://github.com/acl2/acl2/commit/53831c8b283d401338063cd2490a9cd9c4ae9a48
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Add code to unread (i.e. put back) tokens.
Add and call (stub) function to preprocess text lines.
Commit: 9a97d72e365bfb4a28e90bac96858699b5b9fd9d
https://github.com/acl2/acl2/commit/9a97d72e365bfb4a28e90bac96858699b5b9fd9d
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Add some clarifying doc.
Commit: b1954183a6527cb0bad4fd2bac4dc280a838f8cc
https://github.com/acl2/acl2/commit/b1954183a6527cb0bad4fd2bac4dc280a838f8cc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve preprocessor.
Pass whitespace and comments before hashes to the dedicated preprocessing
functions.
Commit: 4ffd00409a55b7bf364cd84f0a66ae314eb79fb1
https://github.com/acl2/acl2/commit/4ffd00409a55b7bf364cd84f0a66ae314eb79fb1
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/compilation-db.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Make terminology in doc more consistent.
In documentation (not necessarily code), we consistently say 'white space'
(instead of 'whitespace') and 'new line' (instead of 'newline'), as in the C
standard. We hyphenate when the role is attributive (e.g. 'new-line character').
Commit: 73f1122c5aafa43d5b30389435a809d25f7117a9
https://github.com/acl2/acl2/commit/73f1122c5aafa43d5b30389435a809d25f7117a9
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/grammar/all.abnf
Log Message:
-----------
[C$] Tweak some doc comments in the grammar.
Commit: f93e46c2176b843fe1ca2ed0ffa8211336660b4e
https://github.com/acl2/acl2/commit/f93e46c2176b843fe1ca2ed0ffa8211336660b4e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Shorten some variable names.
Commit: e5e392bbec251d4e4375006be9b20c6262ac758a
https://github.com/acl2/acl2/commit/e5e392bbec251d4e4375006be9b20c6262ac758a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Add support for the null directive.
Commit: e29e1b18be210898a76672c68be4c41e77ae607e
https://github.com/acl2/acl2/commit/e29e1b18be210898a76672c68be4c41e77ae607e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
A books/kestrel/c/syntax/tests/empty.c
A books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/whitespace.c
Log Message:
-----------
[C$] Start adding preprocessor tests.
Commit: d43af4887708304168d0a32f682b119152ebfa3b
https://github.com/acl2/acl2/commit/d43af4887708304168d0a32f682b119152ebfa3b
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/grammar/all.abnf
Log Message:
-----------
[C$] Make a grammar rule more precise.
Commit: aa2455c5b48d6099dd19897b17edb26fc38778de
https://github.com/acl2/acl2/commit/aa2455c5b48d6099dd19897b17edb26fc38778de
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Fix bug in preprocessor uncovered by testing.
We need to check for new lines and line comments.
Commit: 9b76c92bf78345a38633c6bd5d6c90ded083230f
https://github.com/acl2/acl2/commit/9b76c92bf78345a38633c6bd5d6c90ded083230f
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor.lisp
M books/kestrel/c/syntax/tests/whitespace.c
Log Message:
-----------
[C$] Slightly extend a preprocessor test.
Commit: 9f58f8dae3c5ec9ae93af18c3012715e6104c0e9
https://github.com/acl2/acl2/commit/9f58f8dae3c5ec9ae93af18c3012715e6104c0e9
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
Log Message:
-----------
[C$] Improve preprocessor lexer.
Keep track of the exact new lines that terminate line comments, so they can be
printed out properly after preprocessing.
Commit: c8ad27551a6ad3d902417761703ebe38b0bab5a3
https://github.com/acl2/acl2/commit/c8ad27551a6ad3d902417761703ebe38b0bab5a3
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
A books/kestrel/c/syntax/tests/comments.c
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Add a preprocessor test.
Commit: b73b7b2173d855e80fe2529c20889be7989aa6ad
https://github.com/acl2/acl2/commit/b73b7b2173d855e80fe2529c20889be7989aa6ad
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve preprocessor.
Handle null directive more uniformly when terminated by line comment.
Commit: 357b139c8863a7d242ba9098787c6f3f14ca49ce
https://github.com/acl2/acl2/commit/357b139c8863a7d242ba9098787c6f3f14ca49ce
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Add preprocessor tests for null directives.
Commit: c338a7a9786c9b04a5fdfb81645bf225ec48df32
https://github.com/acl2/acl2/commit/c338a7a9786c9b04a5fdfb81645bf225ec48df32
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor-messages.lisp
Log Message:
-----------
[C$] Improve error messages.
Refine the mapping of identifiers to messages in the preprocessor. This is
motivated by the fact that we need to distinguish different identifiers as names
of directives.
Commit: 72b7d1ef6aaae4f153117ab2e1c9bdcea5bb5f0e
https://github.com/acl2/acl2/commit/72b7d1ef6aaae4f153117ab2e1c9bdcea5bb5f0e
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Start fleshing out the handling of the different directives.
Commit: 4e1bb9edd8c0915ba2022471367e7a9957201598
https://github.com/acl2/acl2/commit/4e1bb9edd8c0915ba2022471367e7a9957201598
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast.lisp
M books/kestrel/c/transformation/tests/simpadd0/file-scope.lisp
M books/kestrel/c/transformation/tests/simpadd0/global.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/unary.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-fn-when/split-fn-when.lisp
M books/kestrel/c/transformation/tests/split-fn/split-fn.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
M books/kestrel/c/transformation/tests/wrap-fn/wrap-fn.lisp
Log Message:
-----------
[C$] Improve printer.
Print a blank line between external declarations, as the documentation of the
printing function already said in fact (but apparently the code failed to
fulfill that).
Commit: 14bb5557cece91b2fb961ef5e07413bc3bf788bb
https://github.com/acl2/acl2/commit/14bb5557cece91b2fb961ef5e07413bc3bf788bb
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Simplify preprocessor.
Discard white space and comments preceding directives.
Commit: 3c2c5578561c0d40a2c797e180aa09f6f3256111
https://github.com/acl2/acl2/commit/3c2c5578561c0d40a2c797e180aa09f6f3256111
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Advance preprocessor.
Start handling `#include` directives.
Commit: 10d7f1bfc882b7e7ce06b5a62af67f299cba5026
https://github.com/acl2/acl2/commit/10d7f1bfc882b7e7ce06b5a62af67f299cba5026
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
Log Message:
-----------
[C$] Extend AST of translation units.
Add an optional line comment at the beginning of the translation unit.
Extend the printer to handle that.
Commit: 3da8ff662ea5a387d0e02e1f469e9431d6efd886
https://github.com/acl2/acl2/commit/3da8ff662ea5a387d0e02e1f469e9431d6efd886
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-multi.lisp
M books/kestrel/c/transformation/tests/simpadd0/bin.lisp
M books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast.lisp
M books/kestrel/c/transformation/tests/simpadd0/constant.lisp
M books/kestrel/c/transformation/tests/simpadd0/decl.lisp
M books/kestrel/c/transformation/tests/simpadd0/dowhile.lisp
M books/kestrel/c/transformation/tests/simpadd0/file-scope.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/global.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-const.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-param.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-return.lisp
M books/kestrel/c/transformation/tests/simpadd0/noninteger.lisp
M books/kestrel/c/transformation/tests/simpadd0/paren.lisp
M books/kestrel/c/transformation/tests/simpadd0/pure-expr-stmt.lisp
M books/kestrel/c/transformation/tests/simpadd0/return-void.lisp
M books/kestrel/c/transformation/tests/simpadd0/stmt-null.lisp
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/unary.lisp
M books/kestrel/c/transformation/tests/simpadd0/variable.lisp
M books/kestrel/c/transformation/tests/simpadd0/while.lisp
Log Message:
-----------
[C2C] Improve `simpadd0`.
Generate a comment at the beginning of each generate file saying that the file
is generated by this transformation.
Adjust test expectations.
Commit: 734f40d6222a9cb2f65bd1cd55683b2f8b1d887a
https://github.com/acl2/acl2/commit/734f40d6222a9cb2f65bd1cd55683b2f8b1d887a
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Expand some doc.
Commit: 086abc06614b5855e0cc9ed2c7e4ac066c8fb4cc
https://github.com/acl2/acl2/commit/086abc06614b5855e0cc9ed2c7e4ac066c8fb4cc
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-multi.lisp
M books/kestrel/c/transformation/tests/simpadd0/bin.lisp
M books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast.lisp
M books/kestrel/c/transformation/tests/simpadd0/constant.lisp
M books/kestrel/c/transformation/tests/simpadd0/decl.lisp
M books/kestrel/c/transformation/tests/simpadd0/dowhile.lisp
M books/kestrel/c/transformation/tests/simpadd0/file-scope.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/global.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-const.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-param.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-return.lisp
M books/kestrel/c/transformation/tests/simpadd0/noninteger.lisp
M books/kestrel/c/transformation/tests/simpadd0/paren.lisp
M books/kestrel/c/transformation/tests/simpadd0/pure-expr-stmt.lisp
M books/kestrel/c/transformation/tests/simpadd0/return-void.lisp
M books/kestrel/c/transformation/tests/simpadd0/stmt-null.lisp
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/unary.lisp
M books/kestrel/c/transformation/tests/simpadd0/variable.lisp
M books/kestrel/c/transformation/tests/simpadd0/while.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-fn-when/split-fn-when.lisp
M books/kestrel/c/transformation/tests/split-fn/split-fn.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
M books/kestrel/c/transformation/tests/wrap-fn/wrap-fn.lisp
Log Message:
-----------
Merge.
Commit: 1b72d7353a49bb447c40840f8dff101649556831
https://github.com/acl2/acl2/commit/1b72d7353a49bb447c40840f8dff101649556831
Author: Alessandro Coglio <
em...@alessandrocoglio.info>
Date: 2025-12-16 (Tue, 16 Dec 2025)
Changed paths:
A books/kestrel/c/syntax/tests/null-directive.c
Log Message:
-----------
[C$] Add forgotten test file.
Commit: d1aca16d553d7d8093f66ed715efe177822f1385
https://github.com/acl2/acl2/commit/d1aca16d553d7d8093f66ed715efe177822f1385
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-17 (Wed, 17 Dec 2025)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/compilation-db.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
A books/kestrel/c/syntax/tests/comments.c
A books/kestrel/c/syntax/tests/empty.c
A books/kestrel/c/syntax/tests/null-directive.c
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
A books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/whitespace.c
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/asg-multi.lisp
M books/kestrel/c/transformation/tests/simpadd0/bin.lisp
M books/kestrel/c/transformation/tests/simpadd0/blocks.lisp
M books/kestrel/c/transformation/tests/simpadd0/cast.lisp
M books/kestrel/c/transformation/tests/simpadd0/constant.lisp
M books/kestrel/c/transformation/tests/simpadd0/decl.lisp
M books/kestrel/c/transformation/tests/simpadd0/dowhile.lisp
M books/kestrel/c/transformation/tests/simpadd0/file-scope.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/global.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-const.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-param.lisp
M books/kestrel/c/transformation/tests/simpadd0/nonint-return.lisp
M books/kestrel/c/transformation/tests/simpadd0/noninteger.lisp
M books/kestrel/c/transformation/tests/simpadd0/paren.lisp
M books/kestrel/c/transformation/tests/simpadd0/pure-expr-stmt.lisp
M books/kestrel/c/transformation/tests/simpadd0/return-void.lisp
M books/kestrel/c/transformation/tests/simpadd0/stmt-null.lisp
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/unary.lisp
M books/kestrel/c/transformation/tests/simpadd0/variable.lisp
M books/kestrel/c/transformation/tests/simpadd0/while.lisp
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-fn-when/split-fn-when.lisp
M books/kestrel/c/transformation/tests/split-fn/split-fn.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
M books/kestrel/c/transformation/tests/wrap-fn/wrap-fn.lisp
Log Message:
-----------
Merge.
Commit: 4fa527c1c538abf7b306fabf402cd516bcd556fc
https://github.com/acl2/acl2/commit/4fa527c1c538abf7b306fabf402cd516bcd556fc
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-17 (Wed, 17 Dec 2025)
Changed paths:
M books/kestrel/c/atc/expression-generation.lisp
Log Message:
-----------
[ATC] Fix doc typo.
Commit: 2c51ae7fedd14da919355b41a9e655e59c7b20cf
https://github.com/acl2/acl2/commit/2c51ae7fedd14da919355b41a9e655e59c7b20cf
Author: Eric Smith <
ews...@gmail.com>
Date: 2025-12-17 (Wed, 17 Dec 2025)
Changed paths:
M books/kestrel/c/atc/generation-contexts.lisp
M books/kestrel/event-macros/applicability-conditions.lisp
Log Message:
-----------
[kestrel] Fix 2 typos found by Gemini.
Commit: d383dbb668357ba4ac99e5a16ef8c417af2294b0
https://github.com/acl2/acl2/commit/d383dbb668357ba4ac99e5a16ef8c417af2294b0
Author: Matt Kaufmann <
kauf...@cs.utexas.edu>
Date: 2025-12-18 (Thu, 18 Dec 2025)
Changed paths:
M basis-a.lisp
M books/centaur/4v-sexpr/.sys/nse...@useless-runes.lsp
M books/centaur/4v-sexpr/.sys/sexpr-lo...@useless-runes.lsp
M books/centaur/4v-sexpr/.sys/sexpr...@useless-runes.lsp
M books/centaur/aig/.sys/aig-...@useless-runes.lsp
M books/centaur/aig/.sys/mi...@useless-runes.lsp
M books/centaur/aignet/.sys/from-h...@useless-runes.lsp
M books/centaur/aignet/.sys/internal-obser...@useless-runes.lsp
M books/centaur/bitops/.sys/congr...@useless-runes.lsp
M books/centaur/bitops/.sys/ihsext...@useless-runes.lsp
M books/centaur/bitops/.sys/limited...@useless-runes.lsp
M books/centaur/bitops/.sys/rational...@useless-runes.lsp
M books/centaur/esim/occform/.sys/t...@useless-runes.lsp
M books/centaur/esim/vcd/.sys/vcd-...@useless-runes.lsp
M books/centaur/esim/vltoe/.sys/add-res...@useless-runes.lsp
M books/centaur/esim/vltoe/.sys/preli...@useless-runes.lsp
M books/centaur/esim/vltoe/.sys/t...@useless-runes.lsp
M books/centaur/esim/vltoe/.sys/zdri...@useless-runes.lsp
M books/centaur/fty/.sys/vis...@useless-runes.lsp
M books/centaur/gl/.sys/b...@useless-runes.lsp
M books/centaur/gl/.sys/rewr...@useless-runes.lsp
M books/centaur/glmc/.sys/bfr-m...@useless-runes.lsp
M books/centaur/glmc/.sys/glmc-gene...@useless-runes.lsp
M books/centaur/meta/.sys/world...@useless-runes.lsp
M books/centaur/misc/.sys/alist-can...@useless-runes.lsp
A books/centaur/misc/.sys/dfs-seen...@useless-runes.lsp
M books/centaur/misc/.sys/evaluator-m...@useless-runes.lsp
M books/centaur/misc/.sys/hons-alpho...@useless-runes.lsp
M books/centaur/misc/.sys/osets-wi...@useless-runes.lsp
M books/centaur/misc/.sys/tar...@useless-runes.lsp
M books/centaur/sv/svex/.sys/override-s...@useless-runes.lsp
M books/centaur/sv/svex/.sys/overrid...@useless-runes.lsp
M books/centaur/sv/svex/.sys/over...@useless-runes.lsp
M books/centaur/sv/svex/.sys/rewrit...@useless-runes.lsp
M books/centaur/sv/svex/.sys/rsh-c...@useless-runes.lsp
M books/centaur/sv/svex/.sys/symb...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/d...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/pro...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-fs...@useless-runes.lsp
M books/centaur/sv/vl/.sys/mo...@useless-runes.lsp
M books/centaur/sv/vl/.sys/svstmt-...@useless-runes.lsp
M books/centaur/sv/vl/.sys/t...@useless-runes.lsp
M books/centaur/sv/vl/.sys/vl-s...@useless-runes.lsp
M books/centaur/vl/kit/.sys/li...@useless-runes.lsp
M books/centaur/vl/kit/.sys/prog...@useless-runes.lsp
M books/centaur/vl/lint/.sys/check...@useless-runes.lsp
M books/centaur/vl/lint/.sys/check-n...@useless-runes.lsp
M books/centaur/vl/lint/.sys/drop-missin...@useless-runes.lsp
M books/centaur/vl/lint/.sys/drop-user-...@useless-runes.lsp
M books/centaur/vl/lint/.sys/ifdef-...@useless-runes.lsp
M books/centaur/vl/lint/.sys/left...@useless-runes.lsp
M books/centaur/vl/lint/.sys/lu...@useless-runes.lsp
M books/centaur/vl/lint/.sys/odd...@useless-runes.lsp
M books/centaur/vl/lint/.sys/selfa...@useless-runes.lsp
M books/centaur/vl/lint/.sys/skip-...@useless-runes.lsp
M books/centaur/vl/lint/.sys/typo-...@useless-runes.lsp
M books/centaur/vl/lint/.sys/use-set...@useless-runes.lsp
M books/centaur/vl/loader/.sys/inject-...@useless-runes.lsp
M books/centaur/vl/loader/.sys/t...@useless-runes.lsp
M books/centaur/vl/loader/parser/.sys/ud...@useless-runes.lsp
M books/centaur/vl/loader/preprocessor/.sys/def...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/hid-...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/hier...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/imm...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/modnam...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/port-...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/print-w...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/remov...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/scope...@useless-runes.lsp
M books/centaur/vl/transforms/annotate/.sys/argre...@useless-runes.lsp
M books/centaur/vl/transforms/annotate/.sys/basic...@useless-runes.lsp
M books/centaur/vl/transforms/annotate/.sys/bi...@useless-runes.lsp
M books/centaur/vl/transforms/annotate/.sys/make-impl...@useless-runes.lsp
M books/centaur/vl/transforms/annotate/.sys/portde...@useless-runes.lsp
M books/centaur/vl/transforms/annotate/.sys/shado...@useless-runes.lsp
M books/centaur/vl/transforms/unparam/.sys/lin...@useless-runes.lsp
M books/centaur/vl/transforms/unparam/.sys/t...@useless-runes.lsp
M books/centaur/vl/util/.sys/os...@useless-runes.lsp
M books/centaur/vl/util/.sys/string...@useless-runes.lsp
M books/centaur/vl2014/.sys/wf-reas...@useless-runes.lsp
M books/centaur/vl2014/kit/.sys/li...@useless-runes.lsp
M books/centaur/vl2014/kit/.sys/prog...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/check...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/check-n...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/drop-missin...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/drop-user-...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/left...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/lu...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/multidri...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/port...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/selfa...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/skip-...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/typo-...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/use-set...@useless-runes.lsp
M books/centaur/vl2014/lint/.sys/use...@useless-runes.lsp
M books/centaur/vl2014/loader/.sys/inject-...@useless-runes.lsp
M books/centaur/vl2014/loader/.sys/t...@useless-runes.lsp
M books/centaur/vl2014/loader/parser/.sys/ud...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/hier...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/imm...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/modnam...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/port-...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/print-w...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/remov...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/scope...@useless-runes.lsp
M books/centaur/vl2014/server/.sys/file-...@useless-runes.lsp
M books/centaur/vl2014/transforms/.sys/delay...@useless-runes.lsp
M books/centaur/vl2014/transforms/.sys/expand-f...@useless-runes.lsp
M books/centaur/vl2014/transforms/.sys/gate...@useless-runes.lsp
M books/centaur/vl2014/transforms/.sys/prop...@useless-runes.lsp
M books/centaur/vl2014/transforms/.sys/replica...@useless-runes.lsp
M books/centaur/vl2014/transforms/.sys/unuse...@useless-runes.lsp
M books/centaur/vl2014/transforms/.sys/weirdi...@useless-runes.lsp
M books/centaur/vl2014/transforms/always/.sys/combin...@useless-runes.lsp
M books/centaur/vl2014/transforms/always/.sys/edge...@useless-runes.lsp
M books/centaur/vl2014/transforms/always/.sys/edge...@useless-runes.lsp
M books/centaur/vl2014/transforms/always/.sys/latc...@useless-runes.lsp
M books/centaur/vl2014/transforms/always/.sys/latch...@useless-runes.lsp
M books/centaur/vl2014/transforms/always/.sys/ut...@useless-runes.lsp
M books/centaur/vl2014/transforms/annotate/.sys/argre...@useless-runes.lsp
M books/centaur/vl2014/transforms/annotate/.sys/make-impl...@useless-runes.lsp
M books/centaur/vl2014/transforms/annotate/.sys/portde...@useless-runes.lsp
M books/centaur/vl2014/transforms/annotate/.sys/shado...@useless-runes.lsp
M books/centaur/vl2014/transforms/unparam/.sys/lin...@useless-runes.lsp
M books/centaur/vl2014/util/.sys/os...@useless-runes.lsp
M books/centaur/vl2014/util/.sys/string...@useless-runes.lsp
M books/clause-processors/.sys/meta-ext...@useless-runes.lsp
R books/clause-processors/SULFA/books/sat/.sys/sulfa-d...@useless-runes.lsp
M books/coi/dtrees/.sys/ba...@useless-runes.lsp
M books/coi/dtrees/.sys/ch...@useless-runes.lsp
M books/coi/dtrees/.sys/de...@useless-runes.lsp
M books/coi/dtrees/.sys/eq...@useless-runes.lsp
M books/coi/dtrees/.sys/er...@useless-runes.lsp
M books/coi/dtrees/.sys/le...@useless-runes.lsp
M books/coi/dtrees/.sys/r...@useless-runes.lsp
M books/coi/dtrees/.sys/roy...@useless-runes.lsp
M books/coi/dtrees/.sys/s...@useless-runes.lsp
M books/coi/maps/.sys/ma...@useless-runes.lsp
M books/coi/maps/.sys/typed...@useless-runes.lsp
M books/coi/osets/.sys/conve...@useless-runes.lsp
M books/coi/osets/.sys/ext...@useless-runes.lsp
M books/coi/osets/.sys/list...@useless-runes.lsp
M books/coi/osets/.sys/multi...@useless-runes.lsp
M books/coi/osets/.sys/mult...@useless-runes.lsp
M books/coi/osets/.sys/ou...@useless-runes.lsp
M books/coi/osets/.sys/primi...@useless-runes.lsp
M books/coi/osets/.sys/set-pr...@useless-runes.lsp
M books/coi/osets/.sys/so...@useless-runes.lsp
M books/coi/paths/.sys/cp-...@useless-runes.lsp
M books/coi/records/.sys/mem-d...@useless-runes.lsp
M books/hints/.sys/basic...@useless-runes.lsp
M books/hints/.sys/use...@useless-runes.lsp
M books/ihs/.sys/basic-de...@useless-runes.lsp
M books/intel/svtv-to-sva/.sys/svtv-to-...@useless-runes.lsp
M books/kestrel/.sys/top...@useless-runes.lsp
M books/kestrel/.sys/t...@useless-runes.lsp
M books/kestrel/acl2pl/.sys/func...@useless-runes.lsp
M books/kestrel/acl2pl/.sys/val...@useless-runes.lsp
M books/kestrel/alists-light/.sys/lookup...@useless-runes.lsp
M books/kestrel/alists-light/.sys/map-look...@useless-runes.lsp
M books/kestrel/apt/.sys/drop-irrele...@useless-runes.lsp
M books/kestrel/apt/.sys/rename...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/a...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/ceilin...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/cei...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/div...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/ex...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/floor-a...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/floor-m...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/flo...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/fl...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/integer...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/lo...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/mo...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/m...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/nonnegative-in...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/pl...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/r...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/ti...@useless-runes.lsp
A books/kestrel/arm/.sys/ar...@useless-runes.lsp
A books/kestrel/arm/.sys/decode...@useless-runes.lsp
A books/kestrel/arm/.sys/dec...@useless-runes.lsp
A books/kestrel/arm/.sys/mem...@useless-runes.lsp
A books/kestrel/arm/.sys/portc...@useless-runes.lsp
A books/kestrel/arm/.sys/pseud...@useless-runes.lsp
A books/kestrel/arm/.sys/st...@useless-runes.lsp
M books/kestrel/axe/.sys/arithmetic...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-clause...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntax-...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntax...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntaxp-e...@useless-runes.lsp
M books/kestrel/axe/.sys/basic...@useless-runes.lsp
M books/kestrel/axe/.sys/bitops...@useless-runes.lsp
M books/kestrel/axe/.sys/boolean-...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-array-...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-intr...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-list-...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/concretize-w...@useless-runes.lsp
M books/kestrel/axe/.sys/conjunctions-a...@useless-runes.lsp
M books/kestrel/axe/.sys/cont...@useless-runes.lsp
M books/kestrel/axe/.sys/convert-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-arr...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-const...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-si...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-varia...@useless-runes.lsp
M books/kestrel/axe/.sys/dag...@useless-runes.lsp
M books/kestrel/axe/.sys/da...@useless-runes.lsp
M books/kestrel/axe/.sys/el...@useless-runes.lsp
M books/kestrel/axe/.sys/equality-assu...@useless-runes.lsp
M books/kestrel/axe/.sys/equivalence-c...@useless-runes.lsp
M books/kestrel/axe/.sys/equivalen...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluat...@useless-runes.lsp
M books/kestrel/axe/.sys/eval...@useless-runes.lsp
M books/kestrel/axe/.sys/find-probable...@useless-runes.lsp
A books/kestrel/axe/.sys/imported...@useless-runes.lsp
M books/kestrel/axe/.sys/lifter...@useless-runes.lsp
M books/kestrel/axe/.sys/logops-r...@useless-runes.lsp
M books/kestrel/axe/.sys/make-ax...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-syntaxp...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-synt...@useless-runes.lsp
M books/kestrel/axe/.sys/make-evalu...@useless-runes.lsp
M books/kestrel/axe/.sys/make-ev...@useless-runes.lsp
M books/kestrel/axe/.sys/make-rewri...@useless-runes.lsp
M books/kestrel/axe/.sys/memoi...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-term-into...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replacement-...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replac...@useless-runes.lsp
M books/kestrel/axe/.sys/normali...@useless-runes.lsp
M books/kestrel/axe/.sys/possibly-neg...@useless-runes.lsp
M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
M books/kestrel/axe/.sys/prover...@useless-runes.lsp
M books/kestrel/axe/.sys/prover...@useless-runes.lsp
M books/kestrel/axe/.sys/prover-st...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-dag-a...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-dag...@useless-runes.lsp
M books/kestrel/axe/.sys/prune...@useless-runes.lsp
M books/kestrel/axe/.sys/refined-assum...@useless-runes.lsp
M books/kestrel/axe/.sys/refined-assu...@useless-runes.lsp
M books/kestrel/axe/.sys/renumber...@useless-runes.lsp
M books/kestrel/axe/.sys/result-ar...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/.sys/rewriter-...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rul...@useless-runes.lsp
M books/kestrel/axe/.sys/stp-count...@useless-runes.lsp
M books/kestrel/axe/.sys/sweep-and-m...@useless-runes.lsp
M books/kestrel/axe/.sys/tactic...@useless-runes.lsp
M books/kestrel/axe/.sys/test-...@useless-runes.lsp
A books/kestrel/axe/.sys/tester...@useless-runes.lsp
M books/kestrel/axe/.sys/translate-...@useless-runes.lsp
M books/kestrel/axe/.sys/trim-intro...@useless-runes.lsp
M books/kestrel/axe/.sys/unguarde...@useless-runes.lsp
M books/kestrel/axe/.sys/unroll-s...@useless-runes.lsp
M books/kestrel/axe/examples/.sys/aes-blas...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntaxp-...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/evalua...@useless-runes.lsp
R books/kestrel/axe/jvm/.sys/formal-unit...@useless-runes.lsp
R books/kestrel/axe/jvm/.sys/formal-un...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/jvm-ru...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lifter-u...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lif...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/output-i...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/rewrit...@useless-runes.lsp
A books/kestrel/axe/jvm/.sys/teste...@useless-runes.lsp
A books/kestrel/axe/jvm/.sys/tes...@useless-runes.lsp
R books/kestrel/axe/jvm/.sys/unroll-java...@useless-runes.lsp
R books/kestrel/axe/jvm/.sys/unroll-j...@useless-runes.lsp
R books/kestrel/axe/jvm/.sys/unroll-j...@useless-runes.lsp
A books/kestrel/axe/jvm/.sys/unrolle...@useless-runes.lsp
A books/kestrel/axe/jvm/.sys/unro...@useless-runes.lsp
A books/kestrel/axe/jvm/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-evalu...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-pro...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-syntaxp-e...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/lift-r1...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/assum...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/eval...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/lifter...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/read-an...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/read-over-...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/regi...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/rewr...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/risc-v...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/run-unti...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/sup...@useless-runes.lsp
R books/kestrel/axe/risc-v/.sys/syntax-e...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/syntaxp-...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/t...@useless-runes.lsp
R books/kestrel/axe/risc-v/.sys/unr...@useless-runes.lsp
A books/kestrel/axe/risc-v/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/write-over-...@useless-runes.lsp
M books/kestrel/axe/risc-v/examples/add/.sys/add-n...@useless-runes.lsp
A books/kestrel/axe/risc-v/examples/add/.sys/add-position...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/evalua...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/loop-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/prove-eq...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/syntaxp-ev...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/tester-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/tes...@useless-runes.lsp
R books/kestrel/axe/x86/.sys/unroll-...@useless-runes.lsp
A books/kestrel/axe/x86/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/x86-...@useless-runes.lsp
A books/kestrel/axe/x86/examples/switch/.sys/sup...@useless-runes.lsp
M books/kestrel/bitcoin/.sys/bi...@useless-runes.lsp
M books/kestrel/bitcoin/.sys/bip39...@useless-runes.lsp
M books/kestrel/bitcoin/.sys/bi...@useless-runes.lsp
M books/kestrel/booleans/.sys/bool...@useless-runes.lsp
A books/kestrel/booleans/.sys/booli...@useless-runes.lsp
M books/kestrel/booleans/.sys/boo...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/all-unsig...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/append...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/array-p...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bits-to-byte...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-con...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-ar...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arr...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-a...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-a...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-list-read...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvnot...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvxor...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/byte-t...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bytes-...@useless-runes.lsp
A books/kestrel/bv-lists/.sys/map-bvp...@useless-runes.lsp
A books/kestrel/bv-lists/.sys/map-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-pack...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-p...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-un...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv-an...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packb...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pac...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbvs...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pac...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pack...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pac...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/unpa...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/unsigned-...@useless-runes.lsp
M books/kestrel/bv/.sys/ad...@useless-runes.lsp
M books/kestrel/bv/.sys/ar...@useless-runes.lsp
M books/kestrel/bv/.sys/a...@useless-runes.lsp
M books/kestrel/bv/.sys/b...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bi...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bv-s...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bva...@useless-runes.lsp
M books/kestrel/bv/.sys/bvcat...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvc...@useless-runes.lsp
M books/kestrel/bv/.sys/bvc...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvminu...@useless-runes.lsp
M books/kestrel/bv/.sys/bvm...@useless-runes.lsp
M books/kestrel/bv/.sys/bvm...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvsx-...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvum...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/convert-t...@useless-runes.lsp
M books/kestrel/bv/.sys/floor-m...@useless-runes.lsp
M books/kestrel/bv/.sys/getbit...@useless-runes.lsp
M books/kestrel/bv/.sys/get...@useless-runes.lsp
M books/kestrel/bv/.sys/if-becomes...@useless-runes.lsp
M books/kestrel/bv/.sys/in...@useless-runes.lsp
M books/kestrel/bv/.sys/leftrota...@useless-runes.lsp
M books/kestrel/bv/.sys/leftro...@useless-runes.lsp
M books/kestrel/bv/.sys/leftr...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/ones-co...@useless-runes.lsp
M books/kestrel/bv/.sys/overflow-an...@useless-runes.lsp
M books/kestrel/bv/.sys/pick-...@useless-runes.lsp
M books/kestrel/bv/.sys/put...@useless-runes.lsp
M books/kestrel/bv/.sys/right...@useless-runes.lsp
M books/kestrel/bv/.sys/rot...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/ru...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvdiv...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvdivdo...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvlt...@useless-runes.lsp
M books/kestrel/bv/.sys/sb...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvmo...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvrem...@useless-runes.lsp
M books/kestrel/bv/.sys/singl...@useless-runes.lsp
M books/kestrel/bv/.sys/sl...@useless-runes.lsp
M books/kestrel/bv/.sys/trim-elim...@useless-runes.lsp
M books/kestrel/bv/.sys/trim-elim-r...@useless-runes.lsp
M books/kestrel/bv/.sys/trim-int...@useless-runes.lsp
M books/kestrel/bv/.sys/unsigned-byte-...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/adjus...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/apco...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/arr...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/convert-in...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-str...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-str...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-str...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-binary-s...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-...@useless-runes.lsp
R books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-e...@useless-runes.lsp
R books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-expr-...@useless-runes.lsp
R books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-expr-c...@useless-runes.lsp
R books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-ex...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-ex...@useless-runes.lsp
A books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-expr...@useless-runes.lsp
A books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-expr...@useless-runes.lsp
A books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-expr...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/flexible-a...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/inte...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/not-...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/object-de...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/promot...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/type-o...@useless-runes.lsp
M books/kestrel/c/language/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/c/language/.sys/abstrac...@useless-runes.lsp
M books/kestrel/c/language/.sys/arithmetic...@useless-runes.lsp
M books/kestrel/c/language/.sys/array-op...@useless-runes.lsp
M books/kestrel/c/language/.sys/computati...@useless-runes.lsp
M books/kestrel/c/language/.sys/dynamic-...@useless-runes.lsp
M books/kestrel/c/language/.sys/err...@useless-runes.lsp
A books/kestrel/c/language/.sys/execution-limi...@useless-runes.lsp
A books/kestrel/c/language/.sys/execution-withou...@useless-runes.lsp
M books/kestrel/c/language/.sys/flexible-array...@useless-runes.lsp
A books/kestrel/c/language/.sys/frame-and-s...@useless-runes.lsp
M books/kestrel/c/language/.sys/function-e...@useless-runes.lsp
M books/kestrel/c/language/.sys/gra...@useless-runes.lsp
M books/kestrel/c/language/.sys/ident...@useless-runes.lsp
M books/kestrel/c/language/.sys/integer-o...@useless-runes.lsp
M books/kestrel/c/language/.sys/integer...@useless-runes.lsp
M books/kestrel/c/language/.sys/keyw...@useless-runes.lsp
M books/kestrel/c/language/.sys/object-de...@useless-runes.lsp
A books/kestrel/c/language/.sys/object-type-...@useless-runes.lsp
M books/kestrel/c/language/.sys/opera...@useless-runes.lsp
M books/kestrel/c/language/.sys/pointer-o...@useless-runes.lsp
M books/kestrel/c/language/.sys/portable-asci...@useless-runes.lsp
M books/kestrel/c/language/.sys/real-op...@useless-runes.lsp
M books/kestrel/c/language/.sys/scalar-o...@useless-runes.lsp
M books/kestrel/c/language/.sys/static-s...@useless-runes.lsp
M books/kestrel/c/language/.sys/structure-...@useless-runes.lsp
M books/kestrel/c/language/.sys/tag-envi...@useless-runes.lsp
M books/kestrel/c/language/.sys/ty...@useless-runes.lsp
M books/kestrel/c/language/.sys/val...@useless-runes.lsp
A books/kestrel/c/language/.sys/variable-resolut...@useless-runes.lsp
A books/kestrel/c/language/.sys/variable-visibil...@useless-runes.lsp
A books/kestrel/c/language/implementation-environments/.sys/bool-f...@useless-runes.lsp
M books/kestrel/c/language/implementation-environments/.sys/char-f...@useless-runes.lsp
M books/kestrel/c/language/implementation-environments/.sys/integer-form...@useless-runes.lsp
M books/kestrel/c/language/implementation-environments/.sys/integer...@useless-runes.lsp
M books/kestrel/c/language/implementation-environments/.sys/schar-...@useless-runes.lsp
M books/kestrel/c/language/implementation-environments/.sys/signed-...@useless-runes.lsp
M books/kestrel/c/language/implementation-environments/.sys/t...@useless-runes.lsp
M books/kestrel/c/language/implementation-environments/.sys/uchar-...@useless-runes.lsp
A books/kestrel/c/language/implementation-environments/.sys/vers...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-syn...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-s...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstracti...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/ascii-id...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/code-en...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/compila...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/disambi...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/disamb...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/external-pr...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/file-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/fi...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/forma...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/gra...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/implementatio...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/input...@useless-runes.lsp
R books/kestrel/c/syntax/.sys/keyw...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/langdef...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/le...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/parser-...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/parser...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/par...@useless-runes.lsp
R books/kestrel/c/syntax/.sys/preproc...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/prepro...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/prepro...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/pri...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/prin...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/pur...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/rea...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/stan...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/storage-spe...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/type-speci...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/unamb...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/validation-...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/valid...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/vali...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/compila...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/le...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/parser...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/preproces...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/preproces...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/prepro...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/rea...@useless-runes.lsp
M books/kestrel/c/syntax/tests/.sys/vali...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/constant-p...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/cop...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/input-pr...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/proof-genera...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/proof-ge...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/ren...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/simp...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/speci...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/split-...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/split-...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/spli...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/split-...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/spli...@useless-runes.lsp
R books/kestrel/c/transformation/.sys/splitg...@useless-runes.lsp
R books/kestrel/c/transformation/.sys/spli...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/variables-in-co...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/wrap-...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/wra...@useless-runes.lsp
M books/kestrel/c/transformation/command-line/.sys/wrap...@useless-runes.lsp
M books/kestrel/c/transformation/tests/free-vars/.sys/free...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/asg...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/asg-...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/b...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/blo...@useless-runes.lsp
R books/kestrel/c/transformation/tests/simpadd0/.sys/cast-int...@useless-runes.lsp
R books/kestrel/c/transformation/tests/simpadd0/.sys/cast-lon...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/ca...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/cons...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/de...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/dow...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/file-...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/g...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/glo...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/i...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/ife...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/log...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/lo...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
R books/kestrel/c/transformation/tests/simpadd0/.sys/nosim...@useless-runes.lsp
R books/kestrel/c/transformation/tests/simpadd0/.sys/nosimp...@useless-runes.lsp
R books/kestrel/c/transformation/tests/simpadd0/.sys/nosimp...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/pa...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/pure-ex...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/retur...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/stmt...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/terna...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/un...@useless-runes.lsp
R books/kestrel/c/transformation/tests/simpadd0/.sys/v...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/vari...@useless-runes.lsp
A books/kestrel/c/transformation/tests/simpadd0/.sys/wh...@useless-runes.lsp
A books/kestrel/c/transformation/tests/split-gso/.sys/spli...@useless-runes.lsp
R books/kestrel/c/transformation/tests/split-gso/.sys/spli...@useless-runes.lsp
M books/kestrel/c/transformation/tests/subst-free/.sys/subst...@useless-runes.lsp
A books/kestrel/c/transformation/tests/wrap-fn/.sys/wra...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/call-...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/collect...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/free...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/fresh...@useless-runes.lsp
A books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/subst...@useless-runes.lsp
M books/kestrel/clause-processors/.sys/simple-su...@useless-runes.lsp
M books/kestrel/clause-processors/.sys/subst...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blak...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake-c...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake-c...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/bla...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake2s-exten...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/bla...@useless-runes.lsp
M books/kestrel/crypto/ecdsa/.sys/deterministic-ecdsa-...@useless-runes.lsp
M books/kestrel/crypto/ecdsa/.sys/deterministic-ecd...@useless-runes.lsp
M books/kestrel/crypto/ecdsa/.sys/deterministic-...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/secp256k1-dom...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/secp256...@useless-runes.lsp
M books/kestrel/crypto/keccak/.sys/keccak-t...@useless-runes.lsp
M books/kestrel/crypto/keccak/.sys/kec...@useless-runes.lsp
M books/kestrel/crypto/mimc/.sys/mimcs...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/baby-jubjub-s...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/bls12-3...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/bn-254-gr...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/ed25519-b...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/ed25519-g...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/goldilocks-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/jubjub-sub...@useless-runes.lsp
A books/kestrel/crypto/primes/.sys/koala...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/nist-p-256...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/nist-p-256-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/secp256k1-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/secp256k1-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/t...@useless-runes.lsp
M books/kestrel/crypto/r1cs/.sys/valua...@useless-runes.lsp
M books/kestrel/crypto/r1cs/dense/.sys/constrain...@useless-runes.lsp
M books/kestrel/crypto/r1cs/dense/.sys/example-c...@useless-runes.lsp
M books/kestrel/crypto/r1cs/dense/.sys/example...@useless-runes.lsp
M books/kestrel/crypto/r1cs/dense/.sys/r1...@useless-runes.lsp
M books/kestrel/crypto/r1cs/dense/.sys/te...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/.sys/p1...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/na...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/non...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/range...@useless-runes.lsp
M books/kestrel/crypto/r1cs/tools/.sys/filter-and-combi...@useless-runes.lsp
M books/kestrel/crypto/salsa/.sys/salsa2...@useless-runes.lsp
M books/kestrel/crypto/salsa/.sys/sal...@useless-runes.lsp
M books/kestrel/crypto/sha-2/.sys/sha...@useless-runes.lsp
M books/kestrel/crypto/sha-2/.sys/sha...@useless-runes.lsp
M books/kestrel/crypto/sha-3/.sys/sh...@useless-runes.lsp
A books/kestrel/crypto/tea/.sys/inve...@useless-runes.lsp
M books/kestrel/crypto/tea/.sys/tea-...@useless-runes.lsp
M books/kestrel/crypto/tea/.sys/t...@useless-runes.lsp
M books/kestrel/ethereum/.sys/t...@useless-runes.lsp
M books/kestrel/ethereum/evm/.sys/e...@useless-runes.lsp
M books/kestrel/ethereum/evm/.sys/sup...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/baby-...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/blake2s-mi...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/edwards2mont...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/montgomery2e...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/montgomer...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/montgomeryd...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/multimux...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/multimux...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/r1cs-pro...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/read-file-into...@useless-runes.lsp
M books/kestrel/floats/.sys/ieee-floa...@useless-runes.lsp
M books/kestrel/floats/.sys/ieee-floats...@useless-runes.lsp
M books/kestrel/floats/.sys/ieee-...@useless-runes.lsp
M books/kestrel/floats/.sys/ro...@useless-runes.lsp
M books/kestrel/floats/.sys/r...@useless-runes.lsp
A books/kestrel/fty/.sys/any-n...@useless-runes.lsp
A books/kestrel/fty/.sys/characte...@useless-runes.lsp
A books/kestrel/fty/.sys/charac...@useless-runes.lsp
M books/kestrel/fty/.sys/deffixtype-...@useless-runes.lsp
M books/kestrel/fty/.sys/defset...@useless-runes.lsp
M books/kestrel/fty/.sys/nat...@useless-runes.lsp
M books/kestrel/fty/.sys/pos...@useless-runes.lsp
M books/kestrel/fty/.sys/s...@useless-runes.lsp
M books/kestrel/fty/.sys/strin...@useless-runes.lsp
A books/kestrel/fty/.sys/string-str...@useless-runes.lsp
M books/kestrel/fty/.sys/symbo...@useless-runes.lsp
M books/kestrel/java/language/.sys/gra...@useless-runes.lsp
M books/kestrel/java/language/.sys/ident...@useless-runes.lsp
M books/kestrel/java/language/.sys/keywords-...@useless-runes.lsp
M books/kestrel/java/language/.sys/keyw...@useless-runes.lsp
M books/kestrel/java/language/.sys/unicode-c...@useless-runes.lsp
M books/kestrel/json-parser/.sys/parse...@useless-runes.lsp
M books/kestrel/jvm/.sys/ad...@useless-runes.lsp
M books/kestrel/jvm/.sys/a...@useless-runes.lsp
M books/kestrel/jvm/.sys/arr...@useless-runes.lsp
M books/kestrel/jvm/.sys/class-fi...@useless-runes.lsp
M books/kestrel/jvm/.sys/cla...@useless-runes.lsp
M books/kestrel/jvm/.sys/do-ins...@useless-runes.lsp
M books/kestrel/jvm/.sys/intern...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-f...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-r...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-...@useless-runes.lsp
M books/kestrel/jvm/.sys/j...@useless-runes.lsp
M books/kestrel/jvm/.sys/met...@useless-runes.lsp
M books/kestrel/jvm/.sys/util...@useless-runes.lsp
M books/kestrel/lists-light/.sys/evens-a...@useless-runes.lsp
M books/kestrel/lists-light/.sys/group...@useless-runes.lsp
M books/kestrel/lists-light/.sys/gr...@useless-runes.lsp
M books/kestrel/lists-light/.sys/intersect...@useless-runes.lsp
M books/kestrel/lists-light/.sys/list...@useless-runes.lsp
M books/kestrel/lists-light/.sys/member...@useless-runes.lsp
M books/kestrel/lists-light/.sys/no-duplica...@useless-runes.lsp
M books/kestrel/lists-light/.sys/pe...@useless-runes.lsp
M books/kestrel/lists-light/.sys/reva...@useless-runes.lsp
M books/kestrel/lists-light/.sys/rev...@useless-runes.lsp
M books/kestrel/lists-light/.sys/subset...@useless-runes.lsp
M books/kestrel/lists-light/.sys/ung...@useless-runes.lsp
M books/kestrel/memory/.sys/make-memory-re...@useless-runes.lsp
M books/kestrel/memory/.sys/memory-...@useless-runes.lsp
M books/kestrel/memory/.sys/memo...@useless-runes.lsp
M books/kestrel/memory/.sys/memo...@useless-runes.lsp
M books/kestrel/memory/.sys/memo...@useless-runes.lsp
M books/kestrel/number-theory/.sys/defprim...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/bv-rul...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/bv-r...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/equal-of-add-c...@useless-runes.lsp
M books/kestrel/risc-v/executable/.sys/decoding-...@useless-runes.lsp
M books/kestrel/risc-v/executable/.sys/execution-...@useless-runes.lsp
M books/kestrel/risc-v/optimized/.sys/state...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/execu...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/execu...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/feat...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/rv3...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/rv6...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/seman...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/seman...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/stat...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/sta...@useless-runes.lsp
R books/kestrel/risc-v/specialized/.sys/suppor...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv32im-le/.sys/exec...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv32im-le/.sys/feat...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv32im-le/.sys/portc...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv32im-le/.sys/sema...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv32im-le/.sys/sta...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv32im-le/.sys/suppor...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv32im-le/.sys/t...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv64im-le/.sys/exec...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv64im-le/.sys/feat...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv64im-le/.sys/portc...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv64im-le/.sys/sema...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv64im-le/.sys/sta...@useless-runes.lsp
A books/kestrel/risc-v/specialized/rv64im-le/.sys/t...@useless-runes.lsp
M books/kestrel/risc-v/specification/.sys/deco...@useless-runes.lsp
M books/kestrel/risc-v/specification/.sys/enco...@useless-runes.lsp
M books/kestrel/risc-v/specification/.sys/exec...@useless-runes.lsp
M books/kestrel/risc-v/specification/.sys/feat...@useless-runes.lsp
M books/kestrel/risc-v/specification/.sys/instru...@useless-runes.lsp
M books/kestrel/risc-v/specification/.sys/reads-ov...@useless-runes.lsp
M books/kestrel/risc-v/specification/.sys/semantics-e...@useless-runes.lsp
M books/kestrel/risc-v/specification/.sys/sema...@useless-runes.lsp
M books/kestrel/risc-v/specification/.sys/sta...@useless-runes.lsp
M books/kestrel/sets/.sys/se...@useless-runes.lsp
A books/kestrel/smt-lib/.sys/fixed-size-...@useless-runes.lsp
A books/kestrel/smt-lib/.sys/in...@useless-runes.lsp
M books/kestrel/syntheto/language/.sys/abstrac...@useless-runes.lsp
M books/kestrel/syntheto/language/.sys/deep-to...@useless-runes.lsp
M books/kestrel/syntheto/shallow/.sys/te...@useless-runes.lsp
M books/kestrel/terms-light/.sys/classify-la...@useless-runes.lsp
M books/kestrel/terms-light/.sys/empty-eva...@useless-runes.lsp
M books/kestrel/terms-light/.sys/hel...@useless-runes.lsp
M books/kestrel/terms-light/.sys/subst-var-...@useless-runes.lsp
M books/kestrel/terms-light/.sys/subst-var-...@useless-runes.lsp
M books/kestrel/terms-light/.sys/substitute-constant...@useless-runes.lsp
M books/kestrel/terms-light/.sys/substitute-l...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/appen...@useless-runes.lsp
A books/kestrel/typed-lists-light/.sys/integer...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/intege...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/keywor...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/map-str...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/pseudo-t...@useless-runes.lsp
M books/kestrel/utilities/.sys/array...@useless-runes.lsp
M books/kestrel/utilities/.sys/conjuncts-an...@useless-runes.lsp
M books/kestrel/utilities/.sys/conjuncts-a...@useless-runes.lsp
M books/kestrel/utilities/.sys/defstobj-...@useless-runes.lsp
M books/kestrel/utilities/.sys/extend-path...@useless-runes.lsp
M books/kestrel/utilities/.sys/fast-al...@useless-runes.lsp
M books/kestrel/utilities/.sys/make...@useless-runes.lsp
M books/kestrel/utilities/.sys/os...@useless-runes.lsp
M books/kestrel/utilities/.sys/temp...@useless-runes.lsp
M books/kestrel/utilities/.sys/te...@useless-runes.lsp
A books/kestrel/utilities/.sys/untranslate...@useless-runes.lsp
M books/kestrel/wasm/.sys/parse-...@useless-runes.lsp
M books/kestrel/x86/.sys/alt-...@useless-runes.lsp
M books/kestrel/x86/.sys/assumptions...@useless-runes.lsp
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/.sys/assum...@useless-runes.lsp
M books/kestrel/x86/.sys/bytes-...@useless-runes.lsp
M books/kestrel/x86/.sys/canonical...@useless-runes.lsp
M books/kestrel/x86/.sys/condi...@useless-runes.lsp
M books/kestrel/x86/.sys/fl...@useless-runes.lsp
M books/kestrel/x86/.sys/flo...@useless-runes.lsp
M books/kestrel/x86/.sys/linear...@useless-runes.lsp
M books/kestrel/x86/.sys/memo...@useless-runes.lsp
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/.sys/read-bytes-an...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-...@useless-runes.lsp
M books/kestrel/x86/.sys/readers-an...@useless-runes.lsp
M books/kestrel/x86/.sys/register-reader...@useless-runes.lsp
M books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
M books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
M books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
M books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
M books/kestrel/x86/.sys/suppo...@useless-runes.lsp
M books/kestrel/x86/.sys/suppo...@useless-runes.lsp
M books/kestrel/x86/.sys/supp...@useless-runes.lsp
M books/kestrel/x86/.sys/supp...@useless-runes.lsp
A books/kestrel/x86/.sys/supp...@useless-runes.lsp
M books/kestrel/x86/.sys/sup...@useless-runes.lsp
M books/kestrel/x86/.sys/write-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/write-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/x86-c...@useless-runes.lsp
M books/kestrel/x86/.sys/z...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/elf-...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/mach-o...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/parse-e...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/parse-ma...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/parse-...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/parsed-exec...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/parser...@useless-runes.lsp
M books/kestrel/x86/parsers/.sys/pe-t...@useless-runes.lsp
M books/kestrel/x86/tools/.sys/unroll-x8...@useless-runes.lsp
A books/kestrel/xml/.sys/build-book-...@useless-runes.lsp
M books/kestrel/xml/.sys/xml-p...@useless-runes.lsp
A books/kestrel/xml/.sys/x...@useless-runes.lsp
M books/kestrel/yul/language/.sys/abstrac...@useless-runes.lsp
M books/kestrel/yul/language/.sys/dynamic-...@useless-runes.lsp
M books/kestrel/yul/language/.sys/mo...@useless-runes.lsp
M books/kestrel/yul/language/.sys/static-shado...@useless-runes.lsp
M books/kestrel/yul/language/.sys/static-s...@useless-runes.lsp
M books/kestrel/yul/library-extensions/.sys/os...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/renaming-var...@useless-runes.lsp
M books/kestrel/zcash/.sys/jub...@useless-runes.lsp
M books/kestrel/zcash/.sys/pedersen-hash-inje...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-1-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zip/.sys/un...@useless-runes.lsp
M books/projects/abnf/notation/.sys/abstrac...@useless-runes.lsp
M books/projects/abnf/notation/.sys/sema...@useless-runes.lsp
M books/projects/abnf/operations/.sys/numeric-ran...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/certif...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/mess...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/successor-predece...@useless-runes.lsp
M books/projects/aleo/leo/early-version/tests/.sys/parse-l...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/blake2s1...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/blake2...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/sup...@useless-runes.lsp
M books/projects/aleo/vm/circuits/samples/.sys/boo...@useless-runes.lsp
M books/projects/apply-model-2/.sys/apply...@useless-runes.lsp
M books/projects/apply-model/.sys/apply...@useless-runes.lsp
M books/projects/apply/.sys/ba...@useless-runes.lsp
M books/projects/bls12-377-curves/primes/.sys/bls12-377-...@useless-runes.lsp
M books/projects/bls12-377-curves/primes/.sys/bls12-3...@useless-runes.lsp
M books/projects/bls12-377-curves/primes/.sys/edwards-bls12-37...@useless-runes.lsp
M books/projects/bls12-377-curves/primes/.sys/t...@useless-runes.lsp
M books/projects/hol-in-acl2/acl2/.sys/lem...@useless-runes.lsp
M books/projects/hol-in-acl2/acl2/.sys/theo...@useless-runes.lsp
A books/projects/hol-in-acl2/acl2/.sys/t...@useless-runes.lsp
A books/projects/hol-in-acl2/examples/.sys/eval-po...@useless-runes.lsp
A books/projects/hol-in-acl2/examples/.sys/eval-pol...@useless-runes.lsp
A books/projects/hol-in-acl2/examples/.sys/eval-poly-...@useless-runes.lsp
A books/projects/hol-in-acl2/examples/.sys/eval-p...@useless-runes.lsp
A books/projects/hol-in-acl2/examples/.sys/ex1-thy...@useless-runes.lsp
M books/projects/pfcs/.sys/abstract-synt...@useless-runes.lsp
M books/projects/pfcs/.sys/abstract-s...@useless-runes.lsp
M books/projects/poseidon/.sys/ingonya...@useless-runes.lsp
M books/projects/poseidon/.sys/instant...@useless-runes.lsp
M books/projects/set-theory/.sys/prove...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/linear...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/three-byte-op...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/vex-opcode...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/b...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/move...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/move...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/mo...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/subro...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/x...@useless-runes.lsp
M books/projects/x86isa/proofs/dataCopy/.sys/data...@useless-runes.lsp
M books/projects/x86isa/proofs/powOfTwo/.sys/powO...@useless-runes.lsp
M books/std/bitsets/.sys/bit...@useless-runes.lsp
M books/std/bitsets/.sys/sbit...@useless-runes.lsp
M books/std/omaps/.sys/co...@useless-runes.lsp
M books/std/osets/.sys/cardi...@useless-runes.lsp
M books/std/osets/.sys/del...@useless-runes.lsp
M books/std/osets/.sys/diffe...@useless-runes.lsp
M books/std/osets/.sys/elemen...@useless-runes.lsp
M books/std/osets/.sys/inte...@useless-runes.lsp
M books/std/osets/.sys/m...@useless-runes.lsp
M books/std/osets/.sys/membe...@useless-runes.lsp
M books/std/osets/.sys/ou...@useless-runes.lsp
M books/std/osets/.sys/primi...@useless-runes.lsp
M books/std/osets/.sys/quan...@useless-runes.lsp
M books/std/osets/.sys/so...@useless-runes.lsp
M books/std/osets/.sys/t...@useless-runes.lsp
M books/std/osets/.sys/under-s...@useless-runes.lsp
M books/std/osets/.sys/un...@useless-runes.lsp
A books/std/strings/.sys/ascii...@useless-runes.lsp
A books/std/strings/.sys/letter-us...@useless-runes.lsp
M books/std/util/.sys/add-io-pairs...@useless-runes.lsp
M books/std/util/.sys/add-io-pairs...@useless-runes.lsp
M books/std/util/.sys/add-io-pair...@useless-runes.lsp
M books/std/util/.sys/add-io-pa...@useless-runes.lsp
M books/std/util/.sys/def...@useless-runes.lsp
M books/system/.sys/pseudo-go...@useless-runes.lsp
M books/system/apply/.sys/apply...@useless-runes.lsp
M books/system/doc/acl2-doc.lisp
M history-management.lisp
M induct.lisp
M interface-raw.lisp
M other-events.lisp
M rewrite.lisp
M translate.lisp
Log Message:
-----------
Updated useless-runes files. Fixed typos in comments.
Thanks to Eric Smith for pointing out (using Gemini) that there were
occurrences of "to to" and "the the" in comments and :DOC -- those are
the typos I fixed.
Commit: 7456a760b3f0fdf680276aba9c5acf810ab50efe
https://github.com/acl2/acl2/commit/7456a760b3f0fdf680276aba9c5acf810ab50efe
Author: Matt Kaufmann <
kauf...@cs.utexas.edu>
Date: 2025-12-18 (Thu, 18 Dec 2025)
Changed paths:
M books/kestrel/c/atc/generation-contexts.lisp
M books/kestrel/event-macros/applicability-conditions.lisp
Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/master'
Compare:
https://github.com/acl2/acl2/compare/fe9c90f01bc2...7456a760b3f0
To unsubscribe from these emails, change your notification settings at
https://github.com/acl2/acl2/settings/notifications