[acl2/acl2] 02c5bb: Add:define's and defrule's

0 views
Skip to first unread message

Grant Jurgensen

unread,
Jun 18, 2026, 3:34:04 PM (5 days ago) Jun 18
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 02c5bb349a96d63971514c2e2a147048d514cd31
https://github.com/acl2/acl2/commit/02c5bb349a96d63971514c2e2a147048d514cd31
Author: Quan Luu <quan...@Quans-MacBook-Air.local>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
A books/std/omaps/extension-tmp.lisp

Log Message:
-----------
Add:define's and defrule's


Commit: 7f383a64403bade3f9690918764cad1935cdbe30
https://github.com/acl2/acl2/commit/7f383a64403bade3f9690918764cad1935cdbe30
Author: Quan Luu <quan...@Quans-MacBook-Air.local>
Date: 2026-05-07 (Thu, 07 May 2026)

Changed paths:
M books/std/omaps/extension-tmp.lisp

Log Message:
-----------
Done: compose identityp injectivep restrict-values closedp WIP: compatiblep inverse


Commit: 3881f4dc48b9d57842caa4ccbea4f7e90e02d7f9
https://github.com/acl2/acl2/commit/3881f4dc48b9d57842caa4ccbea4f7e90e02d7f9
Author: Quan Luu <quan...@Quans-MacBook-Air.local>
Date: 2026-05-08 (Fri, 08 May 2026)

Changed paths:
M books/std/omaps/extension-tmp.lisp

Log Message:
-----------
Add: assoc-of-inverse-when-assoc and necessary lemmas


Commit: 85afc4bf82b4b8f3aed736ff5d07d5167e34bcaf
https://github.com/acl2/acl2/commit/85afc4bf82b4b8f3aed736ff5d07d5167e34bcaf
Author: Quan Luu <quan...@Quans-MacBook-Air.local>
Date: 2026-05-11 (Mon, 11 May 2026)

Changed paths:
M books/std/omaps/extension-tmp.lisp

Log Message:
-----------
Add:resolved some skip-proofs


Commit: 44f6e5e0a421cd9f593d6f5df968708ccbde2055
https://github.com/acl2/acl2/commit/44f6e5e0a421cd9f593d6f5df968708ccbde2055
Author: Quan Luu <quan...@Quans-MacBook-Air.local>
Date: 2026-05-12 (Tue, 12 May 2026)

Changed paths:
M books/std/omaps/extension-tmp.lisp

Log Message:
-----------
Add:resolved some skip-proofs and added a way to prove identityp via skolem


Commit: edb92b25ab5e80ab4803bdab77ac230931be2e19
https://github.com/acl2/acl2/commit/edb92b25ab5e80ab4803bdab77ac230931be2e19
Author: ltmquan <41107477...@users.noreply.github.com>
Date: 2026-05-12 (Tue, 12 May 2026)

Changed paths:
M books/doc/practices.lisp
M books/kestrel/apt/drop-irrelevant-params.lisp
A books/kestrel/apt/remove-nesting-tests.lisp
A books/kestrel/apt/remove-nesting.lisp
M books/kestrel/apt/top.lisp
M books/kestrel/apt/utilities/def-equality-transformation-tests.lisp
M books/kestrel/apt/utilities/def-equality-transformation.lisp
M books/kestrel/apt/utilities/defun-variant.lisp
M books/kestrel/apt/wrap-output.lisp
M books/kestrel/axe/arm/assumptions.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/def-dag-builder-theorems.lisp
M books/kestrel/axe/get-disjuncts-tests.lisp
M books/kestrel/axe/get-disjuncts.lisp
M books/kestrel/axe/identical-xor-nests.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules1.lisp
M books/kestrel/axe/rules2.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/x86/examples/switch/.sys/sup...@useless-runes.lsp
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv/adder.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bvcat-rules.lisp
M books/kestrel/bv/bvcat.lisp
M books/kestrel/bv/bvcount.lisp
M books/kestrel/bv/bvdiv.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/getbit-rules.lisp
M books/kestrel/bv/getbit.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/logapp.lisp
A books/kestrel/bv/logbitp.lisp
M books/kestrel/bv/logext.lisp
M books/kestrel/bv/logtail.lisp
M books/kestrel/bv/ones-complement.lisp
M books/kestrel/bv/overflow-and-underflow.lisp
M books/kestrel/bv/padding.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/rules12.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules4.lisp
M books/kestrel/bv/rules6.lisp
M books/kestrel/bv/rules8.lisp
M books/kestrel/bv/rules9.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/single-bit.lisp
M books/kestrel/bv/slice.lisp
M books/kestrel/bv/top.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/encoding-prefixes.abnf
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/identifier-lists.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c17.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c23.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives.abnf
A books/kestrel/c/syntax/grammar/preprocessing-expressions-c17.abnf
A books/kestrel/c/syntax/grammar/preprocessing-expressions-c23.abnf
A books/kestrel/c/syntax/grammar/preprocessing-expressions.abnf
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
A books/kestrel/error-checking/ensure-function-known-measure.lisp
M books/kestrel/executable-parsers/elf-tools.lisp
M books/kestrel/executable-parsers/parse-elf-file.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce.lisp
M books/kestrel/fty/defresult.lisp
A books/kestrel/fty/nat-list-list-result.lisp
A books/kestrel/fty/nat-list-list.lisp
A books/kestrel/fty/string-nat-list-map.lisp
A books/kestrel/fty/string-nat-map.lisp
A books/kestrel/fty/string-string-map-pair-result.lisp
A books/kestrel/fty/string-string-map-pair.lisp
A books/kestrel/fty/string-string-map-quadruple-result.lisp
A books/kestrel/fty/string-string-map-quadruple.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/jvm/compile-file-if-needed-core.sh
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/cert.acl2
M books/kestrel/remora/character-literal-codes.lisp
A books/kestrel/remora/concrete-syntax-trees.lisp
A books/kestrel/remora/concrete-syntax.lisp
M books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/dynamic-semantics.lisp
A books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/frame-flattening.lisp
A books/kestrel/remora/fresh-variables.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/grammar.lisp
M books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
A books/kestrel/remora/parsing-and-printing.acl2
A books/kestrel/remora/parsing-and-printing.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
R books/kestrel/remora/values.lisp
M books/kestrel/utilities/error-checking/top.lisp
A books/kestrel/utilities/flatten-ands-in-lit.lisp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/projects/abnf/notation/semantics.lisp
M books/projects/pfcs/proof-support.lisp
M books/projects/pfcs/semantics.lisp
M books/projects/x86isa/machine/decoding-and-spec-utils.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/utils/fp-structures.lisp
M books/std/omaps/core.lisp
M books/system/doc/acl2-doc.lisp
M books/system/doc/developers-guide.lisp
M books/xdoc/fancy/xdoc.js
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Merge branch 'acl2:master' into master


Commit: 60cd617478e3c411dc5d41f0cde0353b674b4ea7
https://github.com/acl2/acl2/commit/60cd617478e3c411dc5d41f0cde0353b674b4ea7
Author: Quan Luu <quan...@mac.mynetworksettings.com>
Date: 2026-05-12 (Tue, 12 May 2026)

Changed paths:
M books/std/omaps/extension-tmp.lisp

Log Message:
-----------
Add:resolved all skip-proofs


Commit: 1ca893215d03903b0dfb433111843e146bbdd0ff
https://github.com/acl2/acl2/commit/1ca893215d03903b0dfb433111843e146bbdd0ff
Author: ltmquan <41107477...@users.noreply.github.com>
Date: 2026-05-19 (Tue, 19 May 2026)

Changed paths:
M acl2.lisp
M axioms.lisp
M books/acl2s/aspf/interface/top.lisp
M books/doc/more-topics.lisp
M books/doc/top.lisp
M books/kestrel/arm/memory.lisp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/axe/arm/assumptions.lisp
M books/kestrel/axe/arm/axe-rules.lisp
A books/kestrel/axe/arm/clear-writes.lisp
M books/kestrel/axe/arm/doc.lisp
M books/kestrel/axe/arm/examples/add/add-with-stop-pcs.lisp
M books/kestrel/axe/arm/examples/add/add.lisp
A books/kestrel/axe/arm/examples/popcount/acl2-customization.lsp
A books/kestrel/axe/arm/examples/popcount/cert.acl2
A books/kestrel/axe/arm/examples/popcount/compile.sh
A books/kestrel/axe/arm/examples/popcount/popcount-32-proof.lisp
A books/kestrel/axe/arm/examples/popcount/popcount-64-proof.lisp
A books/kestrel/axe/arm/examples/popcount/popcount.arm32.elf32
A books/kestrel/axe/arm/examples/popcount/popcount.c
A books/kestrel/axe/arm/examples/tea/acl2-customization.lsp
A books/kestrel/axe/arm/examples/tea/compile.sh
A books/kestrel/axe/arm/examples/tea/wiki.acl2
A books/kestrel/axe/arm/examples/tea/wiki.arm32.elf32
A books/kestrel/axe/arm/examples/tea/wiki.c
A books/kestrel/axe/arm/examples/tea/wiki.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/run-until-return.lisp
M books/kestrel/axe/arm/support.lisp
A books/kestrel/axe/arm/syntax-functions.lisp
M books/kestrel/axe/arm/syntaxp-evaluator.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/dag-size-sparse.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/merge-sort-by-cdr-greater.lisp
M books/kestrel/axe/merge-sort-less-than-rules.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/rules1.lisp
M books/kestrel/axe/rules2.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/sweep-and-merge-support.lisp
M books/kestrel/axe/translation-array.lisp
M books/kestrel/axe/x86/tester-rules-bv.lisp
M books/kestrel/bv/intro.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/trim-elim-rules-bv.lisp
M books/kestrel/ethereum/semaphore/r1cs-proof-rules.lisp
M books/kestrel/jvm/ads2.lisp
M books/kestrel/jvm/arrays.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/heap0.lisp
M books/kestrel/jvm/jvm-rules.lisp
M books/kestrel/lists-light/append-with-key.lisp
M books/kestrel/lists-light/finalcdr.lisp
M books/kestrel/lists-light/group.lisp
M books/kestrel/lists-light/rules2.lisp
M books/kestrel/lists-light/take2.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
M books/kestrel/utilities/declares0.lisp
M books/kestrel/utilities/legal-variablep.lisp
M books/kestrel/x86/read-over-write-rules.lisp
M books/projects/abnf/package.lsp
M books/projects/abnf/top.lisp
A books/projects/filesystems/utilities/cpp-syntax/acl2-customization.lsp
A books/projects/filesystems/utilities/cpp-syntax/cert.acl2
A books/projects/filesystems/utilities/cpp-syntax/cpp-abstract-syntax.lisp
A books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
A books/projects/filesystems/utilities/cpp-syntax/cpp-keywords.lisp
A books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp
A books/projects/filesystems/utilities/cpp-syntax/cpp-token-utilities.lisp
A books/projects/filesystems/utilities/cpp-syntax/package.lsp
A books/projects/filesystems/utilities/cpp-syntax/portcullis.acl2
A books/projects/filesystems/utilities/cpp-syntax/portcullis.lisp
A books/projects/filesystems/utilities/cpp-syntax/top.lisp
M books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
A books/projects/omp/acl2-customization.lsp
A books/projects/omp/cert.acl2
A books/projects/omp/dictionary.lisp
A books/projects/omp/gen-top-doc.lsp
A books/projects/omp/package.lsp
A books/projects/omp/portcullis.acl2
A books/projects/omp/portcullis.lisp
A books/projects/omp/sparse-approximation.lisp
A books/projects/omp/top-doc.lisp
A books/projects/omp/top.lisp
M books/system/doc/acl2-doc.lisp
A books/system/report-timings.lsp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M float-raw.lisp
M history-management.lisp
M interface-raw.lisp
M other-events.lisp

Log Message:
-----------
Merge branch 'acl2:master' into master


Commit: e7c55374a1209f490d2da513e67517d3eafef6ef
https://github.com/acl2/acl2/commit/e7c55374a1209f490d2da513e67517d3eafef6ef
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-19 (Tue, 19 May 2026)

Changed paths:
M books/std/omaps/extension-tmp.lisp

Log Message:
-----------
Edit: the big proof removed the subgoal hint


Commit: 5ab2062983fe5043e36c13b74fecce1756be8584
https://github.com/acl2/acl2/commit/5ab2062983fe5043e36c13b74fecce1756be8584
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-21 (Thu, 21 May 2026)

Changed paths:
M books/std/omaps/extension-tmp.lisp

Log Message:
-----------
Add: changes to extension-tmp.lisp


Commit: cf0e05e898f47cda2989df6879e0015c4e2bebca
https://github.com/acl2/acl2/commit/cf0e05e898f47cda2989df6879e0015c4e2bebca
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/std/omaps/extension-tmp.lisp

Log Message:
-----------
Add:comments + xdoc


Commit: 5f6cda57f78fd3148bec581299861ee1d11f86d3
https://github.com/acl2/acl2/commit/5f6cda57f78fd3148bec581299861ee1d11f86d3
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-26 (Tue, 26 May 2026)

Changed paths:
M books/std/omaps/extension-tmp.lisp

Log Message:
-----------
Add:fixed all skip-proofs


Commit: 1f35f657aac3aacfabf8629231ece72b880ee518
https://github.com/acl2/acl2/commit/1f35f657aac3aacfabf8629231ece72b880ee518
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-27 (Wed, 27 May 2026)

Changed paths:
M books/std/omaps/assoc.lisp
A books/std/omaps/closedp.lisp
A books/std/omaps/compose.lisp
M books/std/omaps/core.lisp
R books/std/omaps/extension-tmp.lisp
A books/std/omaps/identityp.lisp
A books/std/omaps/injectivep.lisp
A books/std/omaps/inverse.lisp
A books/std/omaps/restrict-values.lisp
A books/std/omaps/restrict.lisp

Log Message:
-----------
Add:independent files for each function


Commit: c31e3cf24124365a2a179a08017af1009a516f91
https://github.com/acl2/acl2/commit/c31e3cf24124365a2a179a08017af1009a516f91
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-27 (Wed, 27 May 2026)

Changed paths:
M books/std/omaps/closedp.lisp
M books/std/omaps/compose.lisp
M books/std/omaps/identityp.lisp
M books/std/omaps/injectivep.lisp
M books/std/omaps/inverse.lisp
M books/std/omaps/restrict-values.lisp
M books/std/omaps/restrict.lisp

Log Message:
-----------
Add:copyright headers


Commit: df5677439e8ccd9c8214fbaacc5771a12a33f21c
https://github.com/acl2/acl2/commit/df5677439e8ccd9c8214fbaacc5771a12a33f21c
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-27 (Wed, 27 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/compress11.lisp
M books/kestrel/apt/utilities/def-equality-transformation-tests.lisp
M books/kestrel/apt/utilities/def-equality-transformation.lisp
M books/kestrel/arithmetic-light/floor2.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/add-and-normalize-expr.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/axe-rules-mixed.lisp
M books/kestrel/axe/axe-trees.lisp
M books/kestrel/axe/axe-types.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/bv-array-rules.lisp
M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/choose-rules.lisp
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/dag-array-builders.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/dagify0.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/darg-trees.lisp
M books/kestrel/axe/elim.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter-utilities3.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/jvm/tester.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/make-axe-rules.lisp
M books/kestrel/axe/make-instantiation-code-simple-free-vars.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-dag-into-dag-quick.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp
M books/kestrel/axe/node-replacement-alist-for-context.lisp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prover-common.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/prover2.lisp
M books/kestrel/axe/prune-dag-precisely.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/r1cs/lift-r1cs-rules.lisp
M books/kestrel/axe/r1cs/lift-r1cs.lisp
M books/kestrel/axe/refined-assumption-alists2.lisp
M books/kestrel/axe/replace-node.lisp
M books/kestrel/axe/replace-using-assumptions.lisp
M books/kestrel/axe/rewriter-alt-tests.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules1.lisp
M books/kestrel/axe/rules2.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/specialize.lisp
M books/kestrel/axe/splitting.lisp
M books/kestrel/axe/step-increments.lisp
M books/kestrel/axe/substitute-vars.lisp
M books/kestrel/axe/substitute-vars2.lisp
M books/kestrel/axe/supporting-nodes.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/tailtohead.lisp
M books/kestrel/axe/unify-term-and-dag-with-name.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester-rules-bv.lisp
A books/kestrel/axe/x86/tests/kestrel/assembly/README.md
A books/kestrel/axe/x86/tests/kestrel/assembly/acl2-customization.lsp
A books/kestrel/axe/x86/tests/kestrel/assembly/add.asm
A books/kestrel/axe/x86/tests/kestrel/assembly/add.elf64
A books/kestrel/axe/x86/tests/kestrel/assembly/add.lisp
A books/kestrel/axe/x86/tests/kestrel/assembly/cert.acl2
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/bv-arrays/bv-array-clear.lisp
M books/kestrel/bv-arrays/bv-arrays.lisp
M books/kestrel/bv-lists/bv-list-read-chunk-little.lisp
M books/kestrel/bv-lists/byte-to-bits.lisp
M books/kestrel/bv-lists/bytes-to-bits.lisp
M books/kestrel/bv-lists/map-packbv.lisp
M books/kestrel/bv/adder.lisp
M books/kestrel/bv/bitnot.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/bvcat-rules.lisp
M books/kestrel/bv/bvchop.lisp
M books/kestrel/bv/bvcount.lisp
M books/kestrel/bv/bvlt.lisp
M books/kestrel/bv/bvminus-rules.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvmult-rules.lisp
M books/kestrel/bv/bvplus.lisp
M books/kestrel/bv/bvshl.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/bvxor.lisp
M books/kestrel/bv/getbit.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/logext.lisp
M books/kestrel/bv/logior-b.lisp
M books/kestrel/bv/logxor-b.lisp
M books/kestrel/bv/rotate.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/rules10.lisp
M books/kestrel/bv/rules12.lisp
M books/kestrel/bv/rules2.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules4.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/sbvdivdown-rules.lisp
M books/kestrel/bv/single-bit.lisp
M books/kestrel/bv/slice2.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/syntax/built-in.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/evaluation.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/lexemes.abnf
A books/kestrel/c/syntax/grammar/standard-pragmas-c17.abnf
A books/kestrel/c/syntax/grammar/standard-pragmas-c23.abnf
A books/kestrel/c/syntax/grammar/standard-pragmas.abnf
A books/kestrel/c/syntax/grammar/tokens.abnf
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-options.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/tests/disambiguator-trans-units.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/clause-processors/simplify-after-using-conjunction.lisp
M books/kestrel/ethereum/evm/evm.lisp
M books/kestrel/ethereum/semaphore/blake2s-mixing-proof.lisp
M books/kestrel/fty/deffold-reduce.lisp
A books/kestrel/fty/integer-list-result.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/helpers/linter.lisp
M books/kestrel/jvm/ads.lisp
M books/kestrel/jvm/ads2.lisp
M books/kestrel/jvm/adstop.lisp
M books/kestrel/jvm/arrays-2d.lisp
M books/kestrel/jvm/arrays.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/class-tables.lisp
M books/kestrel/jvm/heap-clearing.lisp
M books/kestrel/jvm/heap0.lisp
M books/kestrel/jvm/instructions.lisp
M books/kestrel/jvm/jvm-facts0.lisp
M books/kestrel/jvm/jvm-rules.lisp
M books/kestrel/jvm/jvm.lisp
M books/kestrel/jvm/utilities2.lisp
M books/kestrel/lists-light/rules2.lisp
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/check-keywords.lisp
M books/kestrel/remora/concrete-syntax.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/dynamic-semantics.lisp
M books/kestrel/remora/dynamic-values.lisp
A books/kestrel/remora/evaluation.lisp
A books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/fresh-variables.lisp
M books/kestrel/remora/grammar.abnf
A books/kestrel/remora/integer-list-operations.lisp
R books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/ispace-equivalence.lisp
A books/kestrel/remora/library-extensions.lisp
A books/kestrel/remora/nat-list-operations.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/terms-light/simplify-ors-proofs.lisp
M books/kestrel/typed-lists-light/decreasingp.lisp
M books/kestrel/x86/alt-defs.lisp
M books/kestrel/x86/conditions.lisp
M books/kestrel/x86/flags.lisp
M books/kestrel/x86/package.lsp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-over-write-rules32.lisp
M books/kestrel/x86/support.lisp
M books/kestrel/x86/support32.lisp
M books/kestrel/zcash/gadgets/a-3-3-6-proof.lisp
A books/projects/fields/README
A books/projects/fields/embeddings.lisp
A books/projects/fields/extensions.lisp
A books/projects/fields/galois.lisp
A books/projects/fields/support/embeddings.lisp
A books/projects/fields/support/extensions.lisp
A books/projects/fields/support/galois.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-abstract-syntax.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-keywords.lisp
A books/projects/filesystems/utilities/cpp-syntax/cpp-member-full.lisp
A books/projects/filesystems/utilities/cpp-syntax/cpp-parser-tests.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-token-utilities.lisp
A books/projects/filesystems/utilities/cpp-syntax/cpp-top-level-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/top.lisp
R books/projects/groups/.sys/abe...@useless-runes.lsp
R books/projects/groups/.sys/act...@useless-runes.lsp
R books/projects/groups/.sys/cau...@useless-runes.lsp
R books/projects/groups/.sys/gro...@useless-runes.lsp
R books/projects/groups/.sys/li...@useless-runes.lsp
R books/projects/groups/.sys/ma...@useless-runes.lsp
R books/projects/groups/.sys/prod...@useless-runes.lsp
R books/projects/groups/.sys/quot...@useless-runes.lsp
R books/projects/groups/.sys/sim...@useless-runes.lsp
R books/projects/groups/.sys/sy...@useless-runes.lsp
R books/projects/groups/.sys/symm...@useless-runes.lsp
R books/projects/groups/README
M books/projects/groups/abelian.lisp
M books/projects/groups/actions.lisp
M books/projects/groups/cauchy.lisp
M books/projects/groups/groups.lisp
M books/projects/groups/maps.lisp
M books/projects/groups/quotients.lisp
R books/projects/groups/support/.sys/a...@useless-runes.lsp
R books/projects/groups/support/.sys/abe...@useless-runes.lsp
R books/projects/groups/support/.sys/act...@useless-runes.lsp
R books/projects/groups/support/.sys/al...@useless-runes.lsp
R books/projects/groups/support/.sys/a...@useless-runes.lsp
R books/projects/groups/support/.sys/dihe...@useless-runes.lsp
R books/projects/groups/support/.sys/gro...@useless-runes.lsp
R books/projects/groups/support/.sys/li...@useless-runes.lsp
R books/projects/groups/support/.sys/ma...@useless-runes.lsp
R books/projects/groups/support/.sys/pe...@useless-runes.lsp
R books/projects/groups/support/.sys/per...@useless-runes.lsp
R books/projects/groups/support/.sys/prod...@useless-runes.lsp
R books/projects/groups/support/.sys/sim...@useless-runes.lsp
R books/projects/groups/support/.sys/sy...@useless-runes.lsp
R books/projects/groups/support/.sys/s...@useless-runes.lsp
R books/projects/groups/support/.sys/tot...@useless-runes.lsp
R books/projects/groups/support/.sys/transpo...@useless-runes.lsp
M books/projects/groups/support/abelian.lisp
M books/projects/groups/support/actions.lisp
M books/projects/groups/support/alt5.lisp
M books/projects/groups/support/groups.lisp
M books/projects/groups/support/maps.lisp
R books/projects/groups/support/maxine/.sys/dihe...@useless-runes.lsp
M books/projects/groups/support/products.lisp
R books/projects/groups/support/support/.sys/gro...@useless-runes.lsp
M books/projects/groups/support/support/groups.lisp
M books/projects/groups/support/sylow.lisp
M books/projects/groups/support/totient.lisp
M books/projects/groups/sylow.lisp
M books/projects/linear/README
M books/projects/linear/fdet.lisp
M books/projects/linear/rational.lisp
M books/projects/linear/rdet.lisp
M books/projects/linear/reduction.lisp
M books/projects/linear/support/cramer.lisp
M books/projects/linear/support/fdet.lisp
M books/projects/linear/support/rdet.lisp
M books/projects/linear/support/reduction.lisp
A books/projects/linear/support/vectors.lisp
A books/projects/linear/vectors.lisp
M books/projects/rac/Makefile
R books/projects/rac/examples/imul/proof.lisp
M books/projects/set-theory/base.lisp
M books/projects/set-theory/doc.lisp
M books/projects/set-theory/logic.txt
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/proofs/utilities/sys-view/paging/gather-paging-structures.lisp
M books/projects/x86isa/utils/paging-structures.lisp
M books/projects/x86isa/utils/records-0.lisp
M books/projects/x86isa/utils/utilities.lisp
M books/rtl/rel11/lib/gl.lisp
M books/rtl/rel11/support/gl.lisp
M books/xdoc/parse-xml.lisp
M doc/home-page.html

Log Message:
-----------
Merge upstream/testing-kestrel


Commit: d673720d6e915e157dc07db884424f39f2b0fb15
https://github.com/acl2/acl2/commit/d673720d6e915e157dc07db884424f39f2b0fb15
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)

Changed paths:
M books/std/omaps/assoc.lisp
M books/std/omaps/closedp.lisp
M books/std/omaps/compose.lisp
M books/std/omaps/identityp.lisp
M books/std/omaps/injectivep.lisp
M books/std/omaps/inverse.lisp
M books/std/omaps/restrict-values.lisp
M books/std/omaps/restrict.lisp
M books/std/omaps/top.lisp
M books/std/omaps/update.lisp

Log Message:
-----------
[OMAP] clean up added files and add to top.lisp


Commit: 5b615f9a7c01782163c32c9363c0d4209ed26732
https://github.com/acl2/acl2/commit/5b615f9a7c01782163c32c9363c0d4209ed26732
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)

Changed paths:
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/axe/arm/axe-rules.lisp
M books/kestrel/axe/arm/package.lsp
M books/kestrel/axe/arm/rule-lists.lisp
A books/kestrel/axe/arm/run-until-return-with-tracing.lisp
M books/kestrel/axe/arm/run-until-return.lisp
M books/kestrel/axe/arm/unroller.lisp
A books/kestrel/c/examples/strcpy-safe-induction-support.lisp
M books/kestrel/c/examples/strcpy-safe.lisp
M books/kestrel/c/language/array-operations.lisp
M books/kestrel/c/language/computation-states.lisp
M books/kestrel/c/language/implementation-environments/dialects.lisp
M books/kestrel/c/language/structure-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/grammar.lisp
A books/kestrel/c/syntax/grammar/expressions-ext.abnf
A books/kestrel/c/syntax/grammar/expressions-std.abnf
A books/kestrel/c/syntax/grammar/expressions.abnf
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/reader.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/unicode-characters.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/fty/fty-set.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/extra-grammatical-restrictions.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[OMAP] merge from testing-kestrel


Commit: de5ebe0280063ac2ab67bd99927c98cd33e96ead
https://github.com/acl2/acl2/commit/de5ebe0280063ac2ab67bd99927c98cd33e96ead
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-29 (Fri, 29 May 2026)

Changed paths:
M books/kestrel/apt/doc.lisp
M books/kestrel/arm/def-inst.lisp
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/memory.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/arm/step.lisp
M books/kestrel/arm/tests/simple.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/run-until-return.lisp

Log Message:
-----------
[OMAP] merge from testing-kestrel


Commit: 280502fc7de02e7d0f67a1a3a1882ea9d612bdf6
https://github.com/acl2/acl2/commit/280502fc7de02e7d0f67a1a3a1882ea9d612bdf6
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-29 (Fri, 29 May 2026)

Changed paths:
M books/centaur/fty/bitstruct.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
A books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
A books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/uid.lisp
A books/kestrel/c/syntax/validation-annotations.lisp
R books/kestrel/c/syntax/validation-information.lisp
A books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validation.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/input-processing.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-all-gso-doc.lisp
M books/kestrel/c/transformation/split-gso-doc.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn-doc.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
M books/projects/acl2-in-hol/.acl2holrc.bash
A books/projects/hol-in-acl2/LICENSE

Log Message:
-----------
[OMAP] merge from master branch


Commit: 57d176689ef24aa57185615c64678185a99d3856
https://github.com/acl2/acl2/commit/57d176689ef24aa57185615c64678185a99d3856
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-05-29 (Fri, 29 May 2026)

Changed paths:
M books/std/omaps/closedp.lisp
M books/std/omaps/identityp.lisp

Log Message:
-----------
[OMAP] fixed doc issues for closedp and identityp


Commit: 173f83b6ace9d30673198dc3bbaeb905923751b3
https://github.com/acl2/acl2/commit/173f83b6ace9d30673198dc3bbaeb905923751b3
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-01 (Mon, 01 Jun 2026)

Changed paths:
A books/kestrel/jsonrpc/temp.lisp

Log Message:
-----------
[JSONRPC] create new book


Commit: 31bc793348f555f63f4826b216c8df00b4162393
https://github.com/acl2/acl2/commit/31bc793348f555f63f4826b216c8df00b4162393
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-01 (Mon, 01 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/temp.lisp

Log Message:
-----------
[JSONRPC] Add parsing, dispatching, and file read/write


Commit: 6d5cfffc6248542e9adddccea1f6dc7fa096fbe2
https://github.com/acl2/acl2/commit/6d5cfffc6248542e9adddccea1f6dc7fa096fbe2
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-03 (Wed, 03 Jun 2026)

Changed paths:
A books/kestrel/jsonrpc/acl2-customization.lsp
A books/kestrel/jsonrpc/cert.acl2
A books/kestrel/jsonrpc/json-request.txt
A books/kestrel/jsonrpc/json-response.txt
A books/kestrel/jsonrpc/package.lsp
A books/kestrel/jsonrpc/portcullis.acl2
A books/kestrel/jsonrpc/portcullis.lisp
M books/kestrel/jsonrpc/temp.lisp
A books/kestrel/jsonrpc/test.lisp

Log Message:
-----------
[JSONRPC] add test files


Commit: e49179c417ad99b71cf4fc8b84df8b1afede44e9
https://github.com/acl2/acl2/commit/e49179c417ad99b71cf4fc8b84df8b1afede44e9
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-03 (Wed, 03 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/temp.lisp

Log Message:
-----------
[JSONRPC] added structured fty


Commit: 5800db08cba2cbd6d70269af6e63678651aae12d
https://github.com/acl2/acl2/commit/5800db08cba2cbd6d70269af6e63678651aae12d
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-04 (Thu, 04 Jun 2026)

Changed paths:
A books/kestrel/apt/annotate-c-locals.lisp
R books/kestrel/apt/casesplit-tests.lisp
M books/kestrel/apt/doc.lisp
R books/kestrel/apt/drop-irrelevant-params-tests.lisp
R books/kestrel/apt/expdata-tests.lisp
R books/kestrel/apt/finite-difference-tests.lisp
R books/kestrel/apt/isodata-tests.lisp
R books/kestrel/apt/lift-iso-tests.lisp
R books/kestrel/apt/parteval-tests.lisp
R books/kestrel/apt/remove-nesting-tests.lisp
R books/kestrel/apt/rename-calls-tests.lisp
R books/kestrel/apt/rename-params-tests.lisp
R books/kestrel/apt/restrict-tests.lisp
R books/kestrel/apt/schemalg-concrete-tests.lisp
R books/kestrel/apt/schemalg-divconq-list-0-1-template-tests.lisp
R books/kestrel/apt/schemalg-divconq-oset-0-1-template-tests.lisp
R books/kestrel/apt/simplify-conjunctions-tests.lisp
R books/kestrel/apt/simplify-defun-sk-tests.lisp
R books/kestrel/apt/simplify-defun-tests.lisp
R books/kestrel/apt/simplify-defun-with-cgen-tests.acl2
R books/kestrel/apt/simplify-defun-with-cgen-tests.lisp
R books/kestrel/apt/simplify-term-tests.lisp
R books/kestrel/apt/simplify-tests.lisp
R books/kestrel/apt/tailrec-tests.lisp
A books/kestrel/apt/tests/annotate-c-locals-tests.lisp
A books/kestrel/apt/tests/casesplit-tests.lisp
A books/kestrel/apt/tests/cert.acl2
A books/kestrel/apt/tests/drop-irrelevant-params-tests.lisp
A books/kestrel/apt/tests/expdata-tests.lisp
A books/kestrel/apt/tests/finite-difference-tests.lisp
A books/kestrel/apt/tests/isodata-tests.lisp
A books/kestrel/apt/tests/lift-iso-tests.lisp
A books/kestrel/apt/tests/parteval-tests.lisp
A books/kestrel/apt/tests/remove-nesting-tests.lisp
A books/kestrel/apt/tests/rename-calls-tests.lisp
A books/kestrel/apt/tests/rename-params-tests.lisp
A books/kestrel/apt/tests/restrict-tests.lisp
A books/kestrel/apt/tests/schemalg-concrete-tests.lisp
A books/kestrel/apt/tests/schemalg-divconq-list-0-1-template-tests.lisp
A books/kestrel/apt/tests/schemalg-divconq-oset-0-1-template-tests.lisp
A books/kestrel/apt/tests/simplify-conjunctions-tests.lisp
A books/kestrel/apt/tests/simplify-defun-sk-tests.lisp
A books/kestrel/apt/tests/simplify-defun-tests.lisp
A books/kestrel/apt/tests/simplify-defun-with-cgen-tests.acl2
A books/kestrel/apt/tests/simplify-defun-with-cgen-tests.lisp
A books/kestrel/apt/tests/simplify-term-tests.lisp
A books/kestrel/apt/tests/simplify-tests.lisp
A books/kestrel/apt/tests/tailrec-tests.lisp
A books/kestrel/apt/tests/top.lisp
A books/kestrel/apt/tests/wrap-output-tests.lisp
M books/kestrel/apt/top.lisp
R books/kestrel/apt/wrap-output-tests.lisp
M books/kestrel/arithmetic-light/types.lisp
M books/kestrel/axe/x86/tests/kestrel/assembly/README.md
A books/kestrel/axe/x86/tests/kestrel/assembly/add.elf32
A books/kestrel/axe/x86/tests/kestrel/assembly/add.o32
A books/kestrel/axe/x86/tests/kestrel/assembly/add32.lisp
A books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
A books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
A books/kestrel/c/syntax/abstract-syntax-formal-subset.lisp
R books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/character-constants-c17.abnf
M books/kestrel/c/syntax/grammar/character-constants-c23.abnf
M books/kestrel/c/syntax/grammar/character-constants.abnf
M books/kestrel/c/syntax/grammar/characters-c17.abnf
M books/kestrel/c/syntax/grammar/characters-c23.abnf
M books/kestrel/c/syntax/grammar/characters.abnf
M books/kestrel/c/syntax/grammar/comments.abnf
M books/kestrel/c/syntax/grammar/constants-c17.abnf
M books/kestrel/c/syntax/grammar/constants-c23.abnf
M books/kestrel/c/syntax/grammar/encoding-prefixes.abnf
M books/kestrel/c/syntax/grammar/enumeration-constants.abnf
A books/kestrel/c/syntax/grammar/expressions-c17-ext.abnf
A books/kestrel/c/syntax/grammar/expressions-c17-noext.abnf
A books/kestrel/c/syntax/grammar/expressions-c17.abnf
A books/kestrel/c/syntax/grammar/expressions-c23-ext.abnf
A books/kestrel/c/syntax/grammar/expressions-c23-noext.abnf
A books/kestrel/c/syntax/grammar/expressions-c23.abnf
M books/kestrel/c/syntax/grammar/expressions-ext.abnf
R books/kestrel/c/syntax/grammar/expressions-std.abnf
M books/kestrel/c/syntax/grammar/expressions.abnf
M books/kestrel/c/syntax/grammar/floating-constants-c17-gcc.abnf
M books/kestrel/c/syntax/grammar/floating-constants-c17-nogcc.abnf
M books/kestrel/c/syntax/grammar/floating-constants-c17.abnf
M books/kestrel/c/syntax/grammar/floating-constants-c23-gcc.abnf
M books/kestrel/c/syntax/grammar/floating-constants-c23-nogcc.abnf
M books/kestrel/c/syntax/grammar/floating-constants-c23.abnf
M books/kestrel/c/syntax/grammar/floating-constants.abnf
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
M books/kestrel/c/syntax/grammar/header-names.abnf
M books/kestrel/c/syntax/grammar/identifier-lists.abnf
M books/kestrel/c/syntax/grammar/identifiers-c17.abnf
M books/kestrel/c/syntax/grammar/identifiers-c23.abnf
M books/kestrel/c/syntax/grammar/identifiers.abnf
M books/kestrel/c/syntax/grammar/integer-constants-c17.abnf
M books/kestrel/c/syntax/grammar/integer-constants-c23.abnf
M books/kestrel/c/syntax/grammar/integer-constants.abnf
M books/kestrel/c/syntax/grammar/keywords-c17-clang-cheri.abnf
A books/kestrel/c/syntax/grammar/keywords-c17-clang-nocheri.abnf
R books/kestrel/c/syntax/grammar/keywords-c17-clang.abnf
M books/kestrel/c/syntax/grammar/keywords-c17-gcc.abnf
A books/kestrel/c/syntax/grammar/keywords-c17-noext.abnf
M books/kestrel/c/syntax/grammar/keywords-c17.abnf
M books/kestrel/c/syntax/grammar/keywords-c23-clang-cheri.abnf
A books/kestrel/c/syntax/grammar/keywords-c23-clang-nocheri.abnf
R books/kestrel/c/syntax/grammar/keywords-c23-clang.abnf
M books/kestrel/c/syntax/grammar/keywords-c23-gcc.abnf
A books/kestrel/c/syntax/grammar/keywords-c23-noext.abnf
M books/kestrel/c/syntax/grammar/keywords-c23.abnf
A books/kestrel/c/syntax/grammar/keywords-cheri.abnf
A books/kestrel/c/syntax/grammar/keywords-clang.abnf
A books/kestrel/c/syntax/grammar/keywords-gcc-clang.abnf
A books/kestrel/c/syntax/grammar/keywords-gcc.abnf
R books/kestrel/c/syntax/grammar/keywords.abnf
M books/kestrel/c/syntax/grammar/lexemes.abnf
M books/kestrel/c/syntax/grammar/preprocessing-directives-c17.abnf
M books/kestrel/c/syntax/grammar/preprocessing-directives-c23.abnf
M books/kestrel/c/syntax/grammar/preprocessing-directives.abnf
M books/kestrel/c/syntax/grammar/preprocessing-expressions-c17.abnf
M books/kestrel/c/syntax/grammar/preprocessing-expressions-c23.abnf
M books/kestrel/c/syntax/grammar/preprocessing-expressions.abnf
M books/kestrel/c/syntax/grammar/preprocessing-lexemes.abnf
M books/kestrel/c/syntax/grammar/preprocessing-numbers-c17.abnf
M books/kestrel/c/syntax/grammar/preprocessing-numbers-c23.abnf
M books/kestrel/c/syntax/grammar/preprocessing-tokens-c17.abnf
M books/kestrel/c/syntax/grammar/preprocessing-tokens-c23.abnf
M books/kestrel/c/syntax/grammar/punctuators-c17.abnf
M books/kestrel/c/syntax/grammar/punctuators-c23.abnf
M books/kestrel/c/syntax/grammar/simple-escapes-ext.abnf
M books/kestrel/c/syntax/grammar/simple-escapes-std.abnf
M books/kestrel/c/syntax/grammar/standard-pragmas-c17.abnf
M books/kestrel/c/syntax/grammar/standard-pragmas-c23.abnf
M books/kestrel/c/syntax/grammar/standard-pragmas.abnf
M books/kestrel/c/syntax/grammar/string-literals-c17.abnf
M books/kestrel/c/syntax/grammar/string-literals-c23.abnf
M books/kestrel/c/syntax/grammar/tokens.abnf
M books/kestrel/c/syntax/grammar/universal-character-names.abnf
M books/kestrel/c/syntax/implementation-environments.lisp
R books/kestrel/c/syntax/langdef-mapping-inverse.lisp
R books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/fty/string-set.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/dynamic-semantics.lisp
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/library-extensions.lisp
A books/kestrel/remora/list-theorems.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
A books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/x86/assumptions32.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-abstract-syntax.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser-tests.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-top-level-parser.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
R books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/utils/paging-structures.lisp
M books/projects/x86isa/utils/segmentation-structures.lisp
M books/projects/x86isa/utils/utilities.lisp
M books/std/omaps/closedp.lisp
M books/std/omaps/compose.lisp
M books/std/omaps/identityp.lisp
M books/std/omaps/injectivep.lisp
M books/std/omaps/inverse.lisp
M books/std/omaps/restrict-values.lisp
M books/std/omaps/update.lisp
M books/system/doc/acl2-doc.lisp
M books/unicode/uchar.lisp
M books/unicode/utf8-decode.lisp
M books/unicode/utf8-encode.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M tau.lisp

Log Message:
-----------
[OMAP] Merge upstream/testing-kestrel


Commit: 54361ac5d3f2fde5681ec0398055f136bbb32e87
https://github.com/acl2/acl2/commit/54361ac5d3f2fde5681ec0398055f136bbb32e87
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-04 (Thu, 04 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/acl2-customization.lsp
M books/kestrel/jsonrpc/json-request.txt
M books/kestrel/jsonrpc/json-response.txt
M books/kestrel/jsonrpc/package.lsp
M books/kestrel/jsonrpc/temp.lisp
M books/kestrel/jsonrpc/test.lisp

Log Message:
-----------
[JSONRPC] fixed package issues and ran first tests


Commit: 170ce7953699f71fb479c341f27a035098db4478
https://github.com/acl2/acl2/commit/170ce7953699f71fb479c341f27a035098db4478
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-05 (Fri, 05 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/cert.acl2
M books/kestrel/jsonrpc/json-request.txt
M books/kestrel/jsonrpc/json-response.txt
A books/kestrel/jsonrpc/json-to-string.lisp
M books/kestrel/jsonrpc/package.lsp
A books/kestrel/jsonrpc/parse-rpc.lisp
M books/kestrel/jsonrpc/portcullis.acl2
A books/kestrel/jsonrpc/process-rpc.lisp
A books/kestrel/jsonrpc/response.lisp
R books/kestrel/jsonrpc/temp.lisp
M books/kestrel/jsonrpc/test.lisp
A books/kestrel/jsonrpc/top.lisp
A books/kestrel/jsonrpc/types.lisp

Log Message:
-----------
[JSONRPC] split temp into separate files


Commit: 6e95ba3414823faa547b1273ccb57b0ef9d1d3fa
https://github.com/acl2/acl2/commit/6e95ba3414823faa547b1273ccb57b0ef9d1d3fa
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-08 (Mon, 08 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/json-request.txt
M books/kestrel/jsonrpc/json-response.txt
M books/kestrel/jsonrpc/parse-rpc.lisp
M books/kestrel/jsonrpc/process-rpc.lisp
M books/kestrel/jsonrpc/test.lisp

Log Message:
-----------
[JSONRPC] small fixes; passed all JSON-RPC tests


Commit: 6180767ddf9682810f957bbce8512f14b1d09092
https://github.com/acl2/acl2/commit/6180767ddf9682810f957bbce8512f14b1d09092
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-09 (Tue, 09 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/cert.acl2
M books/kestrel/jsonrpc/json-request.txt
M books/kestrel/jsonrpc/json-response.txt
M books/kestrel/jsonrpc/package.lsp
M books/kestrel/jsonrpc/process-rpc.lisp
A books/kestrel/jsonrpc/socket-raw.lsp
A books/kestrel/jsonrpc/socket-tests.lisp
A books/kestrel/jsonrpc/socket.lisp
M books/kestrel/jsonrpc/top.lisp

Log Message:
-----------
[JSONRPC] add sockets via hunchentoot


Commit: 298fcca580c5425b311b286d93013e28df77ab21
https://github.com/acl2/acl2/commit/298fcca580c5425b311b286d93013e28df77ab21
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-10 (Wed, 10 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/socket-raw.lsp

Log Message:
-----------
[JSONRPC] switch from using EOF delimiter to newline delimiter in socket-raw.lsp


Commit: ef1b913861ef892f44fe59164db5c06e5ec0625f
https://github.com/acl2/acl2/commit/ef1b913861ef892f44fe59164db5c06e5ec0625f
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/json-request.txt
M books/kestrel/jsonrpc/json-response.txt
A books/kestrel/jsonrpc/json-test.lisp
A books/kestrel/jsonrpc/socket-example.lisp
M books/kestrel/jsonrpc/socket-raw.lsp
R books/kestrel/jsonrpc/socket-tests.lisp
M books/kestrel/jsonrpc/socket.lisp
A books/kestrel/jsonrpc/subtract-example.lisp
R books/kestrel/jsonrpc/test.lisp
M books/kestrel/jsonrpc/top.lisp

Log Message:
-----------
[JSONRPC] fixed raw Lisp code issues


Commit: e8a7ccacd4905ba3757379c3cf00f24c54254351
https://github.com/acl2/acl2/commit/e8a7ccacd4905ba3757379c3cf00f24c54254351
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M axioms.lisp
M books/acl2s/ccg/ccg.lisp
M books/doc/top.lisp
M books/kestrel/acl2pl/grammar.lisp
A books/kestrel/apt/add-return-values.lisp
A books/kestrel/apt/arrange-ifs-and-mbts.lisp
M books/kestrel/apt/doc.lisp
M books/kestrel/apt/parteval.lisp
A books/kestrel/apt/tests/add-return-values-tests.lisp
A books/kestrel/apt/tests/arrange-ifs-and-mbts-tests.lisp
M books/kestrel/apt/tests/top.lisp
M books/kestrel/apt/top.lisp
M books/kestrel/apt/utilities/defun-variant.lisp
M books/kestrel/arm/.sys/mem...@useless-runes.lsp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/memory.lisp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/doc.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/examples/README.md
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/x86/doc.lisp
M books/kestrel/axe/x86/examples/formal-unit-tests/sbox/sbox.c
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/c/atc/arrays.lisp
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/examples/add-uints.lisp
M books/kestrel/c/examples/strcpy-safe-induction.lisp
M books/kestrel/c/examples/strcpy-safe.lisp
M books/kestrel/c/language/grammar.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
A books/kestrel/c/syntax/abstract-syntax-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-subset.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-structurals.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/abstract-syntax.lisp
R books/kestrel/c/syntax/built-in.lisp
A books/kestrel/c/syntax/built-ins.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/grammar.lisp
A books/kestrel/c/syntax/grammar/assembly.abnf
A books/kestrel/c/syntax/grammar/attributes.abnf
M books/kestrel/c/syntax/grammar/expressions-c17-ext.abnf
M books/kestrel/c/syntax/grammar/expressions-c17-noext.abnf
M books/kestrel/c/syntax/grammar/expressions-c23-ext.abnf
M books/kestrel/c/syntax/grammar/expressions-c23-noext.abnf
M books/kestrel/c/syntax/grammar/expressions-ext.abnf
M books/kestrel/c/syntax/grammar/expressions.abnf
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/reader.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/top.lisp
A books/kestrel/c/syntax/types-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/unicode-characters.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation.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/split-gso.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/defmake-self-doc.lisp
M books/kestrel/fty/defmake-self-tests.lisp
M books/kestrel/fty/defmake-self.lisp
A books/kestrel/fty/nat-list-list-list.lisp
M books/kestrel/fty/nat-list-list.lisp
M books/kestrel/fty/top.lisp
A books/kestrel/hacking/acl2-repl-star-history.lsp
M books/kestrel/java/language/grammar.lisp
M books/kestrel/json/grammar.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
R books/kestrel/remora/abstract-syntax-structural-operations.lisp
A books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/arithmetic.lisp
A books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/check-keywords.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/frame-flattening.lisp
A books/kestrel/remora/fresh-variable-operations.lisp
R books/kestrel/remora/fresh-variables.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/grammar.lisp
R books/kestrel/remora/integer-list-operations.lisp
A books/kestrel/remora/integer-lists.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/library-extensions.lisp
R books/kestrel/remora/list-theorems.lisp
A books/kestrel/remora/lists.lisp
R books/kestrel/remora/nat-list-operations.lisp
A books/kestrel/remora/nat-lists.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parser-interface.lisp
A books/kestrel/remora/parser-tests.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
A books/kestrel/remora/variable-renaming-operations.lisp
A books/kestrel/remora/variable-substitution-alpha-operations.lisp
A books/kestrel/remora/variable-substitution-operations.lisp
M books/kestrel/typed-lists-light/string-listp.lisp
M books/kestrel/yul/language/grammar-old.lisp
M books/kestrel/yul/language/grammar.lisp
M books/projects/abnf/examples/http.lisp
M books/projects/abnf/examples/imap.lisp
M books/projects/abnf/examples/imf.lisp
M books/projects/abnf/examples/smtp.lisp
M books/projects/abnf/examples/top.lisp
M books/projects/abnf/examples/uri.lisp
M books/projects/abnf/grammar-definer/defgrammar-doc.lisp
M books/projects/abnf/grammar-definer/defgrammar.lisp
M books/projects/abnf/grammar-definer/deftreeops.lisp
M books/projects/abnf/grammar-definer/top.lisp
A books/projects/abnf/grammar-operations/.sys/ambi...@useless-runes.lsp
A books/projects/abnf/grammar-operations/.sys/character-va...@useless-runes.lsp
A books/projects/abnf/grammar-operations/.sys/clo...@useless-runes.lsp
A books/projects/abnf/grammar-operations/.sys/in-term...@useless-runes.lsp
A books/projects/abnf/grammar-operations/.sys/numeric-ran...@useless-runes.lsp
A books/projects/abnf/grammar-operations/.sys/plug...@useless-runes.lsp
A books/projects/abnf/grammar-operations/.sys/rem...@useless-runes.lsp
A books/projects/abnf/grammar-operations/.sys/rena...@useless-runes.lsp
A books/projects/abnf/grammar-operations/.sys/rule-ut...@useless-runes.lsp
A books/projects/abnf/grammar-operations/.sys/t...@useless-runes.lsp
A books/projects/abnf/grammar-operations/.sys/well-fo...@useless-runes.lsp
A books/projects/abnf/grammar-operations/acl2-customization.lsp
A books/projects/abnf/grammar-operations/ambiguity.lisp
A books/projects/abnf/grammar-operations/cert.acl2
A books/projects/abnf/grammar-operations/character-value-retrieval.lisp
A books/projects/abnf/grammar-operations/closure.lisp
A books/projects/abnf/grammar-operations/in-terminal-set.lisp
A books/projects/abnf/grammar-operations/numeric-range-retrieval.lisp
A books/projects/abnf/grammar-operations/plugging.lisp
A books/projects/abnf/grammar-operations/removal.lisp
A books/projects/abnf/grammar-operations/renaming.lisp
A books/projects/abnf/grammar-operations/rule-utilities.lisp
A books/projects/abnf/grammar-operations/top.lisp
A books/projects/abnf/grammar-operations/well-formedness.lisp
M books/projects/abnf/grammar-parser/executable.lisp
M books/projects/abnf/grammar-parser/top.lisp
M books/projects/abnf/grammar-parser/verification.lisp
M books/projects/abnf/grammar-printer/executable.lisp
M books/projects/abnf/grammar-printer/top.lisp
M books/projects/abnf/notation/abstract-syntax.lisp
M books/projects/abnf/notation/concrete-syntax-rules-validation.lisp
M books/projects/abnf/notation/concrete-syntax-rules.lisp
M books/projects/abnf/notation/concrete-syntax-validation.lisp
M books/projects/abnf/notation/concrete-syntax.lisp
M books/projects/abnf/notation/convenience-constructors.lisp
M books/projects/abnf/notation/core-rules-validation.lisp
M books/projects/abnf/notation/core-rules.lisp
M books/projects/abnf/notation/meta-circular-validation.lisp
M books/projects/abnf/notation/syntax-abstraction.lisp
M books/projects/abnf/notation/top.lisp
R books/projects/abnf/operations/.sys/ambi...@useless-runes.lsp
R books/projects/abnf/operations/.sys/character-va...@useless-runes.lsp
R books/projects/abnf/operations/.sys/clo...@useless-runes.lsp
R books/projects/abnf/operations/.sys/in-term...@useless-runes.lsp
R books/projects/abnf/operations/.sys/numeric-ran...@useless-runes.lsp
R books/projects/abnf/operations/.sys/plug...@useless-runes.lsp
R books/projects/abnf/operations/.sys/rem...@useless-runes.lsp
R books/projects/abnf/operations/.sys/rena...@useless-runes.lsp
R books/projects/abnf/operations/.sys/rule-ut...@useless-runes.lsp
R books/projects/abnf/operations/.sys/t...@useless-runes.lsp
R books/projects/abnf/operations/.sys/well-fo...@useless-runes.lsp
R books/projects/abnf/operations/acl2-customization.lsp
R books/projects/abnf/operations/ambiguity.lisp
R books/projects/abnf/operations/cert.acl2
R books/projects/abnf/operations/character-value-retrieval.lisp
R books/projects/abnf/operations/closure.lisp
R books/projects/abnf/operations/in-terminal-set.lisp
R books/projects/abnf/operations/numeric-range-retrieval.lisp
R books/projects/abnf/operations/plugging.lisp
R books/projects/abnf/operations/removal.lisp
R books/projects/abnf/operations/renaming.lisp
R books/projects/abnf/operations/rule-utilities.lisp
R books/projects/abnf/operations/top.lisp
R books/projects/abnf/operations/well-formedness.lisp
M books/projects/abnf/parsing-tools/defdefparse-doc.lisp
M books/projects/abnf/parsing-tools/primitives-defresult.lisp
M books/projects/abnf/parsing-tools/primitives-seq.lisp
M books/projects/abnf/parsing-tools/top.lisp
M books/projects/abnf/portcullis.lisp
M books/projects/abnf/top.lisp
M books/projects/aleo/leo/early-version/definition/grammar.lisp
M books/projects/aleo/leo/grammar.lisp
M books/projects/aleo/vm/language/early-version/grammar.lisp
M books/projects/aleo/vm/language/grammar.lisp
M books/projects/pfcs/grammar.lisp
M books/system/doc/acl2-doc.lisp
A books/system/tests/encap-defs-ht-book.acl2
A books/system/tests/encap-defs-ht-book.lisp
A books/system/tests/encap-defs-ht-input.lsp
A books/system/tests/encap-defs-ht-log.txt
A books/system/tests/encap-defs-ht-sub.lisp
A books/unicode/doc.lisp
M defuns.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp
M other-events.lisp

Log Message:
-----------
Merge remote-tracking branch 'upstream/testing-kestrel'


Commit: d2518a23b61d949739d4eeccd5c69feee8ca38a2
https://github.com/acl2/acl2/commit/d2518a23b61d949739d4eeccd5c69feee8ca38a2
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
R books/kestrel/jsonrpc/json-test.lisp

Log Message:
-----------
[JSONRPC] small fix


Commit: 6265e79d5e8bd68850d636715aa10ef7a50192d0
https://github.com/acl2/acl2/commit/6265e79d5e8bd68850d636715aa10ef7a50192d0
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/json-request.txt
M books/kestrel/jsonrpc/json-response.txt
M books/kestrel/jsonrpc/json-to-string.lisp
M books/kestrel/jsonrpc/package.lsp
M books/kestrel/jsonrpc/parse-rpc.lisp
M books/kestrel/jsonrpc/process-rpc.lisp
M books/kestrel/jsonrpc/response.lisp
R books/kestrel/jsonrpc/socket-example.lisp
M books/kestrel/jsonrpc/socket-raw.lsp
M books/kestrel/jsonrpc/socket.lisp
M books/kestrel/jsonrpc/subtract-example.lisp
M books/kestrel/jsonrpc/top.lisp
M books/kestrel/jsonrpc/types.lisp

Log Message:
-----------
[JSONRPC] added allowed-methods, added customizable network interface, and fixed doc issues


Commit: 8ec2031157cd76a8f5f6659b43602d235a7a4089
https://github.com/acl2/acl2/commit/8ec2031157cd76a8f5f6659b43602d235a7a4089
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M bin/new-useless-runes-files.sh
M books/centaur/aignet/.sys/constr...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-ge...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-to-...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-...@useless-runes.lsp
M books/centaur/truth/.sys/dsd4-...@useless-runes.lsp
A books/clause-processors/SULFA/books/sat/.sys/sulfa-d...@useless-runes.lsp
M books/defsort/.sys/remov...@useless-runes.lsp
M books/demos/.sys/stobj-tabl...@useless-runes.lsp
M books/hints/.sys/basic...@useless-runes.lsp
M books/kestrel/.sys/top...@useless-runes.lsp
M books/kestrel/.sys/t...@useless-runes.lsp
M books/kestrel/abstract-domains/intervals/.sys/arith...@useless-runes.lsp
M books/kestrel/abstract-domains/intervals/.sys/subint...@useless-runes.lsp
M books/kestrel/abstract-domains/many-valued-logics/.sys/3...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/acl2-...@useless-runes.lsp
A books/kestrel/acl2-arrays/.sys/alist-to-arr...@useless-runes.lsp
A books/kestrel/acl2-arrays/.sys/alist-t...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/aref1...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/aset1...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/bounded-n...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/comp...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/copy-ar...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/expandab...@useless-runes.lsp
R books/kestrel/acl2-arrays/.sys/make-into-ar...@useless-runes.lsp
R books/kestrel/acl2-arrays/.sys/make-in...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/new-a...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/typed-acl2-...@useless-runes.lsp
M books/kestrel/acl2pl/.sys/equiv...@useless-runes.lsp
M books/kestrel/acl2pl/.sys/evaluati...@useless-runes.lsp
M books/kestrel/acl2pl/.sys/evalu...@useless-runes.lsp
A books/kestrel/acl2pl/.sys/gra...@useless-runes.lsp
A books/kestrel/acl2pl/.sys/reader...@useless-runes.lsp
A books/kestrel/acl2pl/.sys/sharp-dot-...@useless-runes.lsp
M books/kestrel/air/model-0/air/.sys/corre...@useless-runes.lsp
M books/kestrel/air/model-0/air/.sys/pfcs-con...@useless-runes.lsp
M books/kestrel/alists-light/.sys/alists-...@useless-runes.lsp
M books/kestrel/alists-light/.sys/keep-...@useless-runes.lsp
M books/kestrel/alists-light/.sys/lookup-e...@useless-runes.lsp
M books/kestrel/alists-light/.sys/looku...@useless-runes.lsp
M books/kestrel/alists-light/.sys/pairlis...@useless-runes.lsp
M books/kestrel/alists-light/.sys/strip...@useless-runes.lsp
M books/kestrel/alists-light/.sys/uniquify...@useless-runes.lsp
A books/kestrel/apt/.sys/add-retu...@useless-runes.lsp
A books/kestrel/apt/.sys/annotate...@useless-runes.lsp
A books/kestrel/apt/.sys/arrange-if...@useless-runes.lsp
R books/kestrel/apt/.sys/casespl...@useless-runes.lsp
R books/kestrel/apt/.sys/drop-irrelevan...@useless-runes.lsp
R books/kestrel/apt/.sys/expdat...@useless-runes.lsp
R books/kestrel/apt/.sys/finite-diff...@useless-runes.lsp
R books/kestrel/apt/.sys/isodat...@useless-runes.lsp
R books/kestrel/apt/.sys/lift-is...@useless-runes.lsp
R books/kestrel/apt/.sys/parteva...@useless-runes.lsp
A books/kestrel/apt/.sys/remove-...@useless-runes.lsp
R books/kestrel/apt/.sys/rename-ca...@useless-runes.lsp
R books/kestrel/apt/.sys/rename-pa...@useless-runes.lsp
M books/kestrel/apt/.sys/rename...@useless-runes.lsp
R books/kestrel/apt/.sys/restric...@useless-runes.lsp
R books/kestrel/apt/.sys/schemalg-co...@useless-runes.lsp
R books/kestrel/apt/.sys/schemalg-divconq-lis...@useless-runes.lsp
R books/kestrel/apt/.sys/schemalg-divconq-ose...@useless-runes.lsp
R books/kestrel/apt/.sys/simplify-conj...@useless-runes.lsp
R books/kestrel/apt/.sys/simplify-de...@useless-runes.lsp
R books/kestrel/apt/.sys/simplify-d...@useless-runes.lsp
R books/kestrel/apt/.sys/simplify-defun-...@useless-runes.lsp
R books/kestrel/apt/.sys/simplify-...@useless-runes.lsp
R books/kestrel/apt/.sys/simplif...@useless-runes.lsp
R books/kestrel/apt/.sys/tailre...@useless-runes.lsp
R books/kestrel/apt/.sys/wrap-out...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/add-return-...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/annotate-c-...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/arrange-ifs-a...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/casespl...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/drop-irrelevan...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/expdat...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/finite-diff...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/isodat...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/lift-is...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/parteva...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/remove-nes...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/rename-ca...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/rename-pa...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/restric...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/schemalg-co...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/schemalg-divconq-lis...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/schemalg-divconq-ose...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/simplify-conj...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/simplify-de...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/simplify-d...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/simplify-defun-...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/simplify-...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/simplif...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/tailre...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/t...@useless-runes.lsp
A books/kestrel/apt/tests/.sys/wrap-out...@useless-runes.lsp
M books/kestrel/apt/utilities/.sys/def-equality-...@useless-runes.lsp
M books/kestrel/apt/utilities/.sys/deftrans...@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/ex...@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/if...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/integer...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/l...@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/power...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/r...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/trun...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/ty...@useless-runes.lsp
M books/kestrel/arm/.sys/dec...@useless-runes.lsp
M books/kestrel/arm/.sys/enco...@useless-runes.lsp
M books/kestrel/arm/.sys/instru...@useless-runes.lsp
M books/kestrel/arm/.sys/memo...@useless-runes.lsp
M books/kestrel/arm/.sys/mem...@useless-runes.lsp
M books/kestrel/arm/.sys/pseud...@useless-runes.lsp
M books/kestrel/arm/.sys/ru...@useless-runes.lsp
M books/kestrel/arm/.sys/st...@useless-runes.lsp
M books/kestrel/arm/.sys/st...@useless-runes.lsp
M books/kestrel/arrays-2d/.sys/arra...@useless-runes.lsp
M books/kestrel/axe/.sys/add-and-nor...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bitxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bitxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/add-t...@useless-runes.lsp
M books/kestrel/axe/.sys/alist-suitab...@useless-runes.lsp
M books/kestrel/axe/.sys/arrays-o...@useless-runes.lsp
M books/kestrel/axe/.sys/assumpti...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-bind-free-...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-...@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/axe-...@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/bounded-dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/bounded-d...@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-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/cars-decre...@useless-runes.lsp
M books/kestrel/axe/.sys/cars-incre...@useless-runes.lsp
M books/kestrel/axe/.sys/concretize-w...@useless-runes.lsp
M books/kestrel/axe/.sys/conjoin-te...@useless-runes.lsp
M books/kestrel/axe/.sys/conjunctions-a...@useless-runes.lsp
M books/kestrel/axe/.sys/consec...@useless-runes.lsp
M books/kestrel/axe/.sys/cont...@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/count-b...@useless-runes.lsp
M books/kestrel/axe/.sys/crunc...@useless-runes.lsp
M books/kestrel/axe/.sys/crunc...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-arr...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-a...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-parent-ar...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-pare...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-pare...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-pr...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-siz...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-si...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-siz...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-to-ter...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-t...@useless-runes.lsp
M books/kestrel/axe/.sys/dag...@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/da...@useless-runes.lsp
M books/kestrel/axe/.sys/darg-...@useless-runes.lsp
M books/kestrel/axe/.sys/def-sim...@useless-runes.lsp
M books/kestrel/axe/.sys/defthm-axe-...@useless-runes.lsp
M books/kestrel/axe/.sys/defthm-a...@useless-runes.lsp
M books/kestrel/axe/.sys/defth...@useless-runes.lsp
M books/kestrel/axe/.sys/depth...@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/equality-a...@useless-runes.lsp
M books/kestrel/axe/.sys/equivalen...@useless-runes.lsp
M books/kestrel/axe/.sys/equival...@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
M books/kestrel/axe/.sys/find-probable...@useless-runes.lsp
M books/kestrel/axe/.sys/find-prob...@useless-runes.lsp
M books/kestrel/axe/.sys/fixup-...@useless-runes.lsp
M books/kestrel/axe/.sys/get-args...@useless-runes.lsp
M books/kestrel/axe/.sys/get-di...@useless-runes.lsp
M books/kestrel/axe/.sys/grou...@useless-runes.lsp
M books/kestrel/axe/.sys/hit-c...@useless-runes.lsp
M books/kestrel/axe/.sys/identical...@useless-runes.lsp
M books/kestrel/axe/.sys/instantiat...@useless-runes.lsp
M books/kestrel/axe/.sys/instant...@useless-runes.lsp
M books/kestrel/axe/.sys/lifter...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-bind-...@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-dag-co...@useless-runes.lsp
M books/kestrel/axe/.sys/make-dag...@useless-runes.lsp
M books/kestrel/axe/.sys/make-dag-va...@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-impli...@useless-runes.lsp
M books/kestrel/axe/.sys/make-node-rep...@useless-runes.lsp
M books/kestrel/axe/.sys/make-prov...@useless-runes.lsp
M books/kestrel/axe/.sys/make-rewri...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-in...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-in...@useless-runes.lsp
M books/kestrel/axe/.sys/match-hyp-with-node...@useless-runes.lsp
M books/kestrel/axe/.sys/memoi...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-dag-in...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-nodes-i...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-sort-b...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-term-into...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-tree-into...@useless-runes.lsp
M books/kestrel/axe/.sys/node...@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/nodenum-t...@useless-runes.lsp
M books/kestrel/axe/.sys/normali...@useless-runes.lsp
M books/kestrel/axe/.sys/numeri...@useless-runes.lsp
A books/kestrel/axe/.sys/pre-st...@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/pro...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-dag-a...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-with-c...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-wit...@useless-runes.lsp
M books/kestrel/axe/.sys/pure-da...@useless-runes.lsp
M books/kestrel/axe/.sys/pure...@useless-runes.lsp
M books/kestrel/axe/.sys/rationa...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuild-...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuild...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuil...@useless-runes.lsp
M books/kestrel/axe/.sys/refine-as...@useless-runes.lsp
M books/kestrel/axe/.sys/refined-assum...@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/remov...@useless-runes.lsp
M books/kestrel/axe/.sys/renamin...@useless-runes.lsp
M books/kestrel/axe/.sys/replace-usin...@useless-runes.lsp
M books/kestrel/axe/.sys/result...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewriter-...@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/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/.sys/rul...@useless-runes.lsp
M books/kestrel/axe/.sys/rul...@useless-runes.lsp
M books/kestrel/axe/.sys/speci...@useless-runes.lsp
M books/kestrel/axe/.sys/spli...@useless-runes.lsp
M books/kestrel/axe/.sys/stored...@useless-runes.lsp
M books/kestrel/axe/.sys/stp-clause...@useless-runes.lsp
M books/kestrel/axe/.sys/stp-count...@useless-runes.lsp
M books/kestrel/axe/.sys/sublis-va...@useless-runes.lsp
M books/kestrel/axe/.sys/substitu...@useless-runes.lsp
M books/kestrel/axe/.sys/substit...@useless-runes.lsp
M books/kestrel/axe/.sys/supporti...@useless-runes.lsp
M books/kestrel/axe/.sys/support...@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/term-eq...@useless-runes.lsp
M books/kestrel/axe/.sys/translate-...@useless-runes.lsp
M books/kestrel/axe/.sys/translat...@useless-runes.lsp
M books/kestrel/axe/.sys/type-in...@useless-runes.lsp
M books/kestrel/axe/.sys/unguarde...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-and-...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-and...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-ter...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-tre...@useless-runes.lsp
M books/kestrel/axe/.sys/unroll-s...@useless-runes.lsp
M books/kestrel/axe/.sys/wf-...@useless-runes.lsp
M books/kestrel/axe/.sys/worklis...@useless-runes.lsp
M books/kestrel/axe/arm/.sys/assum...@useless-runes.lsp
M books/kestrel/axe/arm/.sys/axe-...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/clear-...@useless-runes.lsp
M books/kestrel/axe/arm/.sys/eval...@useless-runes.lsp
M books/kestrel/axe/arm/.sys/rewr...@useless-runes.lsp
M books/kestrel/axe/arm/.sys/rule-...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/run-until-retu...@useless-runes.lsp
M books/kestrel/axe/arm/.sys/run-unti...@useless-runes.lsp
M books/kestrel/axe/arm/.sys/sup...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/syntax-f...@useless-runes.lsp
M books/kestrel/axe/arm/.sys/syntaxp-...@useless-runes.lsp
M books/kestrel/axe/arm/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-bind-free...@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
M books/kestrel/axe/jvm/.sys/jvm-rul...@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/lifter-u...@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/nice-output...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/output-i...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/symbolic-exe...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/tes...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/unrolle...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/unro...@useless-runes.lsp
M 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-r1c...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/lift-r1...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/lift...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/eval...@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/rewr...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/sup...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/syntaxp-...@useless-runes.lsp
M 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
M books/kestrel/axe/x86/.sys/bind-free-e...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/evalua...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/lifter-...@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/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
M books/kestrel/axe/x86/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/x86-...@useless-runes.lsp
M books/kestrel/booleans/.sys/boo...@useless-runes.lsp
M books/kestrel/booleans/.sys/bool...@useless-runes.lsp
M books/kestrel/booleans/.sys/boo...@useless-runes.lsp
M books/kestrel/booleans/.sys/i...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/append...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/array-o...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/array-p...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-array-c...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-arra...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-array-con...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-array-conv...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-array-c...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-array-c...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-ar...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-array-read...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-array-...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-arr...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-arra...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-a...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/bv-a...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/test...@useless-runes.lsp
A books/kestrel/bv-arrays/.sys/t...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/all-unsign...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/append...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/array-o...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/array-p...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-arra...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-array-con...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-array-conv...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-ar...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-array-read...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-array-...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-arr...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-arra...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-a...@useless-runes.lsp
R books/kestrel/bv-lists/.sys/bv-a...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/byte-t...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bytes-to-b...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bytes-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/len-mul...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-bvp...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pac...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pac...@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/bit-t...@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/bv...@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/bvequa...@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/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvmult...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
A books/kestrel/bv/.sys/bvor...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvp...@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/bvum...@useless-runes.lsp
A books/kestrel/bv/.sys/bvxo...@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/getbi...@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/idi...@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/leftr...@useless-runes.lsp
M books/kestrel/bv/.sys/loga...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
A books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/logi...@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/logx...@useless-runes.lsp
M books/kestrel/bv/.sys/overflow-an...@useless-runes.lsp
M books/kestrel/bv/.sys/pad...@useless-runes.lsp
M books/kestrel/bv/.sys/repea...@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/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/sbvmo...@useless-runes.lsp
M books/kestrel/bv/.sys/signed...@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/c/atc/.sys/gener...@useless-runes.lsp
M books/kestrel/c/atc/.sys/input-pr...@useless-runes.lsp
M books/kestrel/c/atc/.sys/pretty-...@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...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-ex...@useless-runes.lsp
M 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/init-...@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/ret...@useless-runes.lsp
R books/kestrel/c/atc/symbolic-execution-rules/.sys/syn...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/uaconver...@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/array-op...@useless-runes.lsp
M books/kestrel/c/language/.sys/computati...@useless-runes.lsp
M books/kestrel/c/language/.sys/decimal-0-...@useless-runes.lsp
M books/kestrel/c/language/.sys/dynamic-...@useless-runes.lsp
M 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/integer...@useless-runes.lsp
M books/kestrel/c/language/.sys/keyw...@useless-runes.lsp
M books/kestrel/c/language/.sys/punct...@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/implementation-environments/.sys/dial...@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/t...@useless-runes.lsp
M books/kestrel/c/language/implementation-environments/.sys/uchar-...@useless-runes.lsp
R books/kestrel/c/language/implementation-environments/.sys/vers...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/exec-expr-pur...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/exec-expr-p...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/syntaxp-fo...@useless-runes.lsp
M books/kestrel/c/representation/.sys/integer-c...@useless-runes.lsp
M books/kestrel/c/representation/.sys/integer-o...@useless-runes.lsp
M books/kestrel/c/representation/.sys/inte...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/abstract-syntax-fo...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/abstract-syntax-for...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/abstract-syntax-form...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/abstract-synta...@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-synt...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-s...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/ascii-id...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/buil...@useless-runes.lsp
R books/kestrel/c/syntax/.sys/bui...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/code-en...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/compila...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/disamb...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/evalu...@useless-runes.lsp
M 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
R books/kestrel/c/syntax/.sys/forma...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/grammar-c...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/grammar-o...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/gra...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/hash-conditio...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/implementatio...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/infer...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/initializer...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/input...@useless-runes.lsp
R books/kestrel/c/syntax/.sys/langdef-map...@useless-runes.lsp
R books/kestrel/c/syntax/.sys/langdef...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/le...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/macro-...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/null-pointe...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/output...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/parser-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/parser...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/par...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/posi...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preprocesso...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/prepro...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/pri...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/pur...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/rea...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/sp...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/stan...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/string...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/token-con...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/translation-u...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/types-formal-su...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/u...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/unamb...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/unicode-c...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/validation-...@useless-runes.lsp
R books/kestrel/c/syntax/.sys/validation-...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/validati...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/vali...@useless-runes.lsp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
A books/kestrel/c/syntax/tests/.sys/disambiguator-...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/disambiguato...@useless-runes.lsp
R books/kestrel/c/syntax/tests/.sys/disamb...@useless-runes.lsp
M books/kestrel/c/syntax/tests/.sys/preprocessor-...@useless-runes.lsp
M books/kestrel/c/syntax/tests/.sys/vali...@useless-runes.lsp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/.sys/add-sect...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/constant-p...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/cop...@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
M books/kestrel/c/transformation/.sys/spli...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/variables-in-co...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/wra...@useless-runes.lsp
M books/kestrel/c/transformation/cert.acl2
M books/kestrel/c/transformation/command-line/.sys/wrap...@useless-runes.lsp
M books/kestrel/c/transformation/split-gso.lisp
A books/kestrel/c/transformation/struct-type-split-doc.lisp
A books/kestrel/c/transformation/struct-type-split.lisp
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
M books/kestrel/c/transformation/tests/simpadd0/.sys/asg-...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/b...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/blo...@useless-runes.lsp
M 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
M books/kestrel/c/transformation/tests/simpadd0/.sys/dow...@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
M books/kestrel/c/transformation/tests/simpadd0/.sys/pa...@useless-runes.lsp
M 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
M books/kestrel/c/transformation/tests/simpadd0/.sys/un...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/vari...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/wh...@useless-runes.lsp
A books/kestrel/c/transformation/tests/struct-type-split/.gitignore
A books/kestrel/c/transformation/tests/struct-type-split/acl2-customization.lsp
A books/kestrel/c/transformation/tests/struct-type-split/anon-member.c
A books/kestrel/c/transformation/tests/struct-type-split/array.c
A books/kestrel/c/transformation/tests/struct-type-split/cert.acl2
A books/kestrel/c/transformation/tests/struct-type-split/fn-param.c
A books/kestrel/c/transformation/tests/struct-type-split/fn-proto.c
A books/kestrel/c/transformation/tests/struct-type-split/impure-init.c
A books/kestrel/c/transformation/tests/struct-type-split/member.c
A books/kestrel/c/transformation/tests/struct-type-split/mixed-init.c
A books/kestrel/c/transformation/tests/struct-type-split/multi1.c
A books/kestrel/c/transformation/tests/struct-type-split/multi2.c
A books/kestrel/c/transformation/tests/struct-type-split/positional-init.c
A books/kestrel/c/transformation/tests/struct-type-split/ptr-member.c
A books/kestrel/c/transformation/tests/struct-type-split/ret-struct.c
A books/kestrel/c/transformation/tests/struct-type-split/self-ref.c
A books/kestrel/c/transformation/tests/struct-type-split/sizeof.c
A books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/test1.c
A books/kestrel/c/transformation/tests/struct-type-split/test2.c
A books/kestrel/c/transformation/tests/struct-type-split/typedef-chain.c
A books/kestrel/c/transformation/tests/struct-type-split/typedef-ptr.c
A books/kestrel/c/transformation/tests/struct-type-split/typedef.c
A books/kestrel/c/transformation/tests/struct-type-split/union-member.c
A books/kestrel/c/transformation/tests/struct-type-split/union.c
M books/kestrel/c/transformation/tests/subst-free/.sys/subst...@useless-runes.lsp
M books/kestrel/c/transformation/top.lisp
M books/kestrel/c/transformation/utilities/.sys/add-att...@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
M books/kestrel/c/transformation/utilities/.sys/qualifi...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/subst...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/cert.acl2
A books/kestrel/c/transformation/utilities/context-msg.lisp
A books/kestrel/c/transformation/utilities/print-to-str.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
M books/kestrel/clause-processors/.sys/simplify-after-u...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake-25...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blak...@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/chacha/.sys/chac...@useless-runes.lsp
M books/kestrel/crypto/ecdsa/.sys/deterministic-...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/prime-fi...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/secp256k1-dom...@useless-runes.lsp
M books/kestrel/crypto/hmac/.sys/hmac-s...@useless-runes.lsp
M books/kestrel/crypto/hmac/.sys/hmac-s...@useless-runes.lsp
M books/kestrel/crypto/kdf/.sys/pbkdf2-hm...@useless-runes.lsp
M books/kestrel/crypto/keccak/.sys/keccak-t...@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
M 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/sparse/.sys/p1...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/range-ch...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/range...@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-2/.sys/sha...@useless-runes.lsp
M books/kestrel/crypto/sha-2/.sys/sha...@useless-runes.lsp
M books/kestrel/crypto/sha-3/.sys/sha-3-va...@useless-runes.lsp
M books/kestrel/crypto/sha-3/.sys/sh...@useless-runes.lsp
M books/kestrel/crypto/tea/.sys/inve...@useless-runes.lsp
M books/kestrel/csv/.sys/pars...@useless-runes.lsp
M books/kestrel/data/hash/.sys/jen...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/de...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/delet...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/del...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/d...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/extensi...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/in-...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/i...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/keys...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/ke...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/looku...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/loo...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/map-...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/m...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/min-ma...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/min...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/portc...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/restri...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/rest...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/rlooku...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/rlo...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/size...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/si...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/subma...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/to-oma...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/to-...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/t...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/updat...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/update-s...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/updat...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/upd...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/value...@useless-runes.lsp
A books/kestrel/data/treemap/.sys/val...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/antisy...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/bst-...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/b...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/count...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/co...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/delet...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/del...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/d...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/heap...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/he...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/in-ord...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/in-o...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/join...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/jo...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/keys...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/ke...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/looku...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/loo...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/min-ma...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/min...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/restri...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/rest...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/rlooku...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/rlo...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/rotat...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/rot...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/split...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/sp...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/subma...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/tree...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/tr...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/updat...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/update-s...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/updat...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/upd...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/value...@useless-runes.lsp
A books/kestrel/data/treemap/internal/.sys/val...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/del...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/di...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/extensi...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/generi...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/indu...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/ins...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/inte...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/it...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/min...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/s...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/sub...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/un...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/antisy...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/b...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/del...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/di...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/he...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/in-o...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/i...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/ins...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/inte...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/it...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/jo...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/min...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/rot...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/sp...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/sub...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/tr...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/un...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/al...@useless-runes.lsp
R books/kestrel/data/utilities/.sys/list...@useless-runes.lsp
R books/kestrel/data/utilities/.sys/li...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/omap...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/om...@useless-runes.lsp
M books/kestrel/data/utilities/.sys/os...@useless-runes.lsp
A books/kestrel/data/utilities/lists/.sys/de...@useless-runes.lsp
A books/kestrel/data/utilities/lists/.sys/eq...@useless-runes.lsp
A books/kestrel/data/utilities/lists/.sys/rev...@useless-runes.lsp
A books/kestrel/error-checking/.sys/ensure-functio...@useless-runes.lsp
M books/kestrel/ethereum/.sys/data...@useless-runes.lsp
M books/kestrel/ethereum/.sys/mmp-...@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/rlp/.sys/decoda...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/baby-...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/r1cs-pro...@useless-runes.lsp
M books/kestrel/evaluators/.sys/defevaluato...@useless-runes.lsp
M books/kestrel/evaluators/.sys/defevaluator-...@useless-runes.lsp
M books/kestrel/evaluators/.sys/empty...@useless-runes.lsp
M books/kestrel/evaluators/.sys/equali...@useless-runes.lsp
M books/kestrel/evaluators/.sys/if-and-...@useless-runes.lsp
M books/kestrel/evaluators/.sys/if-...@useless-runes.lsp
M books/kestrel/evaluators/.sys/not-...@useless-runes.lsp
M books/kestrel/executable-parsers/.sys/elf-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/memory-...@useless-runes.lsp
M books/kestrel/executable-parsers/.sys/parse-...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/chan...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/close-outp...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/print-objec...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/print-obj...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/read-byt...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/write-by...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/write-bytes...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/write-bytes-...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/write-byt...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/write-object...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/write-objects...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/write-obje...@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
M books/kestrel/fty/.sys/any-n...@useless-runes.lsp
M books/kestrel/fty/.sys/boolean...@useless-runes.lsp
M books/kestrel/fty/.sys/characte...@useless-runes.lsp
M books/kestrel/fty/.sys/character-...@useless-runes.lsp
M books/kestrel/fty/.sys/characte...@useless-runes.lsp
M books/kestrel/fty/.sys/data...@useless-runes.lsp
M books/kestrel/fty/.sys/deffold-...@useless-runes.lsp
M books/kestrel/fty/.sys/deffo...@useless-runes.lsp
M books/kestrel/fty/.sys/deffold-re...@useless-runes.lsp
M books/kestrel/fty/.sys/deffold...@useless-runes.lsp
M books/kestrel/fty/.sys/defmake-s...@useless-runes.lsp
M books/kestrel/fty/.sys/defmak...@useless-runes.lsp
M books/kestrel/fty/.sys/defoma...@useless-runes.lsp
M books/kestrel/fty/.sys/defr...@useless-runes.lsp
M books/kestrel/fty/.sys/depend...@useless-runes.lsp
A books/kestrel/fty/.sys/integer-l...@useless-runes.lsp
M books/kestrel/fty/.sys/integer...@useless-runes.lsp
M books/kestrel/fty/.sys/m...@useless-runes.lsp
M books/kestrel/fty/.sys/maybe-str...@useless-runes.lsp
A books/kestrel/fty/.sys/nat-list-...@useless-runes.lsp
A books/kestrel/fty/.sys/nat-list-l...@useless-runes.lsp
A books/kestrel/fty/.sys/nat-li...@useless-runes.lsp
M books/kestrel/fty/.sys/nat-lis...@useless-runes.lsp
M books/kestrel/fty/.sys/nat-natli...@useless-runes.lsp
M books/kestrel/fty/.sys/nat-option-...@useless-runes.lsp
M books/kestrel/fty/.sys/nat-opti...@useless-runes.lsp
M books/kestrel/fty/.sys/nat-r...@useless-runes.lsp
M books/kestrel/fty/.sys/natoption-natop...@useless-runes.lsp
M books/kestrel/fty/.sys/string-li...@useless-runes.lsp
A books/kestrel/fty/.sys/string-na...@useless-runes.lsp
A books/kestrel/fty/.sys/string-...@useless-runes.lsp
M books/kestrel/fty/.sys/string...@useless-runes.lsp
M books/kestrel/fty/.sys/strin...@useless-runes.lsp
A books/kestrel/fty/.sys/string-string-...@useless-runes.lsp
A books/kestrel/fty/.sys/string-stri...@useless-runes.lsp
A books/kestrel/fty/.sys/string-string-map...@useless-runes.lsp
A books/kestrel/fty/.sys/string-string...@useless-runes.lsp
A books/kestrel/fty/.sys/string-s...@useless-runes.lsp
M books/kestrel/fty/.sys/string-str...@useless-runes.lsp
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
A books/kestrel/fty/msg-list.lisp
A books/kestrel/fty/msg.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/helpers/.sys/advice-imp...@useless-runes.lsp
M books/kestrel/helpers/.sys/de...@useless-runes.lsp
M books/kestrel/helpers/.sys/eval-...@useless-runes.lsp
M books/kestrel/helpers/.sys/hel...@useless-runes.lsp
M books/kestrel/hints/.sys/remove...@useless-runes.lsp
M books/kestrel/hints/.sys/rena...@useless-runes.lsp
M books/kestrel/java/atj/.sys/input-pr...@useless-runes.lsp
M books/kestrel/java/language/.sys/gra...@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/array-b...@useless-runes.lsp
M books/kestrel/jvm/.sys/arra...@useless-runes.lsp
M books/kestrel/jvm/.sys/arr...@useless-runes.lsp
M books/kestrel/jvm/.sys/arr...@useless-runes.lsp
A books/kestrel/jvm/.sys/bind...@useless-runes.lsp
M books/kestrel/jvm/.sys/call-...@useless-runes.lsp
M books/kestrel/jvm/.sys/class-and-...@useless-runes.lsp
M books/kestrel/jvm/.sys/class-fi...@useless-runes.lsp
M books/kestrel/jvm/.sys/class-...@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/events-f...@useless-runes.lsp
M books/kestrel/jvm/.sys/executio...@useless-runes.lsp
M books/kestrel/jvm/.sys/execu...@useless-runes.lsp
M books/kestrel/jvm/.sys/exec...@useless-runes.lsp
M books/kestrel/jvm/.sys/flo...@useless-runes.lsp
M books/kestrel/jvm/.sys/fra...@useless-runes.lsp
M books/kestrel/jvm/.sys/heap-c...@useless-runes.lsp
M books/kestrel/jvm/.sys/he...@useless-runes.lsp
M books/kestrel/jvm/.sys/he...@useless-runes.lsp
M books/kestrel/jvm/.sys/instru...@useless-runes.lsp
M books/kestrel/jvm/.sys/intern...@useless-runes.lsp
M books/kestrel/jvm/.sys/java-...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-f...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-...@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/loc...@useless-runes.lsp
M books/kestrel/jvm/.sys/method-i...@useless-runes.lsp
M books/kestrel/jvm/.sys/met...@useless-runes.lsp
M books/kestrel/jvm/.sys/operand...@useless-runes.lsp
M books/kestrel/jvm/.sys/read-and-par...@useless-runes.lsp
M books/kestrel/jvm/.sys/read-class-f...@useless-runes.lsp
M books/kestrel/jvm/.sys/read...@useless-runes.lsp
M books/kestrel/jvm/.sys/set-c...@useless-runes.lsp
A books/kestrel/jvm/.sys/sta...@useless-runes.lsp
A books/kestrel/jvm/.sys/string-...@useless-runes.lsp
M books/kestrel/jvm/.sys/str...@useless-runes.lsp
M books/kestrel/jvm/.sys/symbolic-exe...@useless-runes.lsp
M books/kestrel/jvm/.sys/symbolic-...@useless-runes.lsp
M books/kestrel/jvm/.sys/symbolic-...@useless-runes.lsp
A books/kestrel/jvm/.sys/t...@useless-runes.lsp
M books/kestrel/jvm/.sys/ty...@useless-runes.lsp
A books/kestrel/jvm/.sys/val...@useless-runes.lsp
M books/kestrel/library-wrappers/.sys/my-make-f...@useless-runes.lsp
M books/kestrel/lists-light/.sys/evens-a...@useless-runes.lsp
M books/kestrel/lists-light/.sys/fir...@useless-runes.lsp
M books/kestrel/lists-light/.sys/group...@useless-runes.lsp
M books/kestrel/lists-light/.sys/gro...@useless-runes.lsp
M books/kestrel/lists-light/.sys/gr...@useless-runes.lsp
M books/kestrel/lists-light/.sys/member...@useless-runes.lsp
M books/kestrel/lists-light/.sys/rul...@useless-runes.lsp
M books/kestrel/lists-light/.sys/ung...@useless-runes.lsp
M books/kestrel/lists-light/.sys/union-e...@useless-runes.lsp
M books/kestrel/lists-light/.sys/update-...@useless-runes.lsp
M books/kestrel/memory/.sys/make-memory-re...@useless-runes.lsp
R 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-r...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/prime-fie...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/rul...@useless-runes.lsp
A books/kestrel/remora/.sys/parse-dire...@useless-runes.lsp
A books/kestrel/remora/.sys/parsing-an...@useless-runes.lsp
A books/kestrel/remora/.sys/portc...@useless-runes.lsp
A books/kestrel/remora/.sys/t...@useless-runes.lsp
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/dynamic-semantics.lisp
R books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/lists.lisp
M books/kestrel/remora/nat-lists.lisp
A books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/remora/type-value-equivalence.lisp
A books/kestrel/remora/values.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/kestrel/risc-v/optimized/.sys/state...@useless-runes.lsp
M books/kestrel/risc-v/specialized/rv32im-le/.sys/sema...@useless-runes.lsp
M books/kestrel/sets/.sys/se...@useless-runes.lsp
M books/kestrel/simpl-imp/.sys/sema...@useless-runes.lsp
M books/kestrel/soft/.sys/te...@useless-runes.lsp
M books/kestrel/strings-light/.sys/add-prefix...@useless-runes.lsp
M books/kestrel/strings-light/.sys/collapse-...@useless-runes.lsp
A books/kestrel/strings-light/.sys/downcas...@useless-runes.lsp
A books/kestrel/strings-light/.sys/split-ch...@useless-runes.lsp
M books/kestrel/strings-light/.sys/strings-st...@useless-runes.lsp
M books/kestrel/strings-light/.sys/strip-suffix...@useless-runes.lsp
M books/kestrel/syntheto/language/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/syntheto/language/.sys/static-sema...@useless-runes.lsp
M books/kestrel/syntheto/language/.sys/static-s...@useless-runes.lsp
M books/kestrel/syntheto/shallow/.sys/te...@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/make-lambda-applic...@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/typed-lists-light/.sys/map-co...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/maxe...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/max...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/mine...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/min...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/string...@useless-runes.lsp
M books/kestrel/unicode-light/.sys/code-point-t...@useless-runes.lsp
M books/kestrel/unicode-light/.sys/hex-digit-char...@useless-runes.lsp
M books/kestrel/untranslated-terms/.sys/conjuncts-a...@useless-runes.lsp
M books/kestrel/untranslated-terms/.sys/let-h...@useless-runes.lsp
M books/kestrel/untranslated-terms/.sys/untranslate...@useless-runes.lsp
M books/kestrel/utilities/.sys/chars-a...@useless-runes.lsp
M books/kestrel/utilities/.sys/conjuncts-and-d...@useless-runes.lsp
M books/kestrel/utilities/.sys/defma...@useless-runes.lsp
M books/kestrel/utilities/.sys/defop...@useless-runes.lsp
M books/kestrel/utilities/.sys/explode-nonne...@useless-runes.lsp
M books/kestrel/utilities/.sys/fast-al...@useless-runes.lsp
A books/kestrel/utilities/.sys/flatten-a...@useless-runes.lsp
M books/kestrel/utilities/.sys/for...@useless-runes.lsp
M books/kestrel/utilities/.sys/fresh...@useless-runes.lsp
M books/kestrel/utilities/.sys/integers...@useless-runes.lsp
M books/kestrel/utilities/.sys/merge-sort-sy...@useless-runes.lsp
M books/kestrel/utilities/.sys/os...@useless-runes.lsp
M books/kestrel/utilities/.sys/st...@useless-runes.lsp
M books/kestrel/utilities/error-checking/.sys/t...@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/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/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/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
M 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/tools/.sys/lifter-...@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/le...@useless-runes.lsp
M books/kestrel/yul/language/.sys/mo...@useless-runes.lsp
M books/kestrel/yul/language/.sys/static-safe...@useless-runes.lsp
M books/kestrel/yul/language/.sys/static-s...@useless-runes.lsp
M books/kestrel/yul/language/.sys/val...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/dead-code-elimi...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/dead-code-eli...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/no-function-def...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/renaming-varia...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/renaming-var...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/rena...@useless-runes.lsp
M books/kestrel/zcash/.sys/jub...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/misc/.sys/hons...@useless-runes.lsp
M books/projects/abnf/.sys/tree-ut...@useless-runes.lsp
R books/projects/abnf/constructor-utilities.lisp
M books/projects/abnf/grammar-operations/.sys/ambi...@useless-runes.lsp
M books/projects/abnf/grammar-operations/.sys/clo...@useless-runes.lsp
M books/projects/abnf/notation/.sys/sema...@useless-runes.lsp
R books/projects/abnf/notation/convenience-constructors.lisp
M books/projects/abnf/notation/core-rules.lisp
M books/projects/abnf/notation/top.lisp
M books/projects/abnf/parsing-tools/.sys/defde...@useless-runes.lsp
A books/projects/abnf/syntax-operations/constructor-utilities.lisp
A books/projects/abnf/syntax-operations/convenience-constructors.lisp
A books/projects/abnf/syntax-operations/top.lisp
M books/projects/abnf/top.lisp
M books/projects/aleo/bft/next/.sys/block...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/certificat...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/certificat...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/certif...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/commi...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/dag-previ...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/dag-signer-...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/dag-sign...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/endorsed-a...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/endorsed-...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/endorsed-pre...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/endorsed-roun...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/endorsement...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/endorsemen...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/endorsement...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/fault-t...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/initial...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/last-anch...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/last-anch...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/last-block...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/ordered-b...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposal-...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposal...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-autho...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-a...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-d...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-endors...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-en...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-pre...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-roun...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/round-af...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/same-committees...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/signed-i...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/signed-p...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/system...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/transitio...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/transitio...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/trans...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/unequiv...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/unequivoca...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/unequivocal-si...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/validato...@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/sup...@useless-runes.lsp
M books/projects/aleo/vm/circuits/library-extensions/.sys/dig...@useless-runes.lsp
M books/projects/aleo/vm/circuits/library-extensions/.sys/om...@useless-runes.lsp
M books/projects/aleo/vm/circuits/pfcs/.sys/boolean-a...@useless-runes.lsp
M books/projects/aleo/vm/circuits/pfcs/.sys/boolean-...@useless-runes.lsp
M books/projects/aleo/vm/circuits/pfcs/.sys/boolean-a...@useless-runes.lsp
M books/projects/aleo/vm/circuits/pfcs/.sys/boole...@useless-runes.lsp
M books/projects/aleo/vm/circuits/pfcs/.sys/field-a...@useless-runes.lsp
M books/projects/aleo/vm/circuits/pfcs/.sys/field-as...@useless-runes.lsp
M books/projects/aleo/vm/circuits/pfcs/.sys/field-di...@useless-runes.lsp
M books/projects/aleo/vm/circuits/pfcs/.sys/fiel...@useless-runes.lsp
M books/projects/aleo/vm/circuits/r1cs/.sys/field-c...@useless-runes.lsp
M books/projects/aleo/vm/circuits/r1cs/.sys/field-p...@useless-runes.lsp
M books/projects/aleo/vm/circuits/r1cs/.sys/unsigned-...@useless-runes.lsp
M books/projects/aleo/vm/circuits/r1cs/.sys/unsigned-med...@useless-runes.lsp
M books/projects/aleo/vm/circuits/r1cs/.sys/unsigned-smal...@useless-runes.lsp
M books/projects/aleo/vm/language/early-version/.sys/par...@useless-runes.lsp
M books/projects/aleo/vm/language/early-version/parser.lisp
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
A books/projects/fields/.sys/embed...@useless-runes.lsp
A books/projects/fields/.sys/exten...@useless-runes.lsp
A books/projects/fields/.sys/gal...@useless-runes.lsp
A books/projects/fields/support/.sys/embed...@useless-runes.lsp
A books/projects/fields/support/.sys/exten...@useless-runes.lsp
A books/projects/fields/support/.sys/gal...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-abstr...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-exp...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-ke...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-mem...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-pars...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-p...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-token...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-top-le...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/portc...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/t...@useless-runes.lsp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp
A books/projects/groups/.sys/abe...@useless-runes.lsp
A books/projects/groups/.sys/act...@useless-runes.lsp
A books/projects/groups/.sys/cau...@useless-runes.lsp
A books/projects/groups/.sys/gro...@useless-runes.lsp
A books/projects/groups/.sys/li...@useless-runes.lsp
A books/projects/groups/.sys/ma...@useless-runes.lsp
A books/projects/groups/.sys/prod...@useless-runes.lsp
A books/projects/groups/.sys/quot...@useless-runes.lsp
A books/projects/groups/.sys/sim...@useless-runes.lsp
A books/projects/groups/.sys/sy...@useless-runes.lsp
A books/projects/groups/.sys/symm...@useless-runes.lsp
A books/projects/groups/support/.sys/a...@useless-runes.lsp
A books/projects/groups/support/.sys/abe...@useless-runes.lsp
A books/projects/groups/support/.sys/act...@useless-runes.lsp
A books/projects/groups/support/.sys/al...@useless-runes.lsp
A books/projects/groups/support/.sys/a...@useless-runes.lsp
A books/projects/groups/support/.sys/dihe...@useless-runes.lsp
A books/projects/groups/support/.sys/gro...@useless-runes.lsp
A books/projects/groups/support/.sys/li...@useless-runes.lsp
A books/projects/groups/support/.sys/ma...@useless-runes.lsp
A books/projects/groups/support/.sys/pe...@useless-runes.lsp
A books/projects/groups/support/.sys/per...@useless-runes.lsp
A books/projects/groups/support/.sys/prod...@useless-runes.lsp
A books/projects/groups/support/.sys/sim...@useless-runes.lsp
A books/projects/groups/support/.sys/sy...@useless-runes.lsp
A books/projects/groups/support/.sys/s...@useless-runes.lsp
A books/projects/groups/support/.sys/tot...@useless-runes.lsp
A books/projects/groups/support/.sys/transpo...@useless-runes.lsp
A books/projects/groups/support/maxine/.sys/dihe...@useless-runes.lsp
A books/projects/groups/support/support/.sys/gro...@useless-runes.lsp
A books/projects/hol-in-acl2/examples/.sys/skolem-th...@useless-runes.lsp
A books/projects/hol-in-acl2/examples/.sys/skole...@useless-runes.lsp
M books/projects/linear/.sys/rati...@useless-runes.lsp
A books/projects/linear/.sys/vec...@useless-runes.lsp
M books/projects/linear/support/.sys/cra...@useless-runes.lsp
M books/projects/linear/support/.sys/fd...@useless-runes.lsp
M books/projects/linear/support/.sys/rd...@useless-runes.lsp
M books/projects/linear/support/.sys/redu...@useless-runes.lsp
A books/projects/linear/support/.sys/vec...@useless-runes.lsp
M books/projects/numbers/support/.sys/birt...@useless-runes.lsp
M books/projects/numbers/support/.sys/derang...@useless-runes.lsp
M books/projects/numbers/support/.sys/divi...@useless-runes.lsp
M books/projects/numbers/support/.sys/parti...@useless-runes.lsp
M books/projects/numbers/support/.sys/sub...@useless-runes.lsp
M books/projects/numbers/support/.sys/sum4s...@useless-runes.lsp
A books/projects/omp/.sys/portc...@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/pfcs/.sys/convenience-...@useless-runes.lsp
M books/projects/pfcs/.sys/gra...@useless-runes.lsp
M books/projects/pfcs/.sys/le...@useless-runes.lsp
M books/projects/pfcs/.sys/lif...@useless-runes.lsp
M books/projects/pfcs/.sys/parser-i...@useless-runes.lsp
M books/projects/pfcs/.sys/par...@useless-runes.lsp
M books/projects/pfcs/.sys/pfield-...@useless-runes.lsp
M books/projects/pfcs/.sys/proof-...@useless-runes.lsp
M books/projects/pfcs/.sys/sema...@useless-runes.lsp
M books/projects/pfcs/.sys/syntax-ab...@useless-runes.lsp
M books/projects/pfcs/.sys/toke...@useless-runes.lsp
M books/projects/pfcs/parser.lisp
M books/projects/poseidon/.sys/ingonya...@useless-runes.lsp
M books/projects/poseidon/.sys/instant...@useless-runes.lsp
M books/projects/poseidon/.sys/main-de...@useless-runes.lsp
R books/projects/rac/examples/imul/.sys/pr...@useless-runes.lsp
M books/projects/set-theory/.sys/ba...@useless-runes.lsp
M books/projects/set-theory/.sys/prove...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/decoding-an...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/interrupt...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/linear...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/pag...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/physica...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/segmen...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/three-byte-op...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/top-leve...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/two-byte-opc...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/vex-opcode...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/x...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/arith-a...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/b...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/b...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/div...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/fl...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/jump-a...@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/mult...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/pa...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/ps...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/push-a...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/ra...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/rotate-a...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/segmen...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/signe...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/str...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/subro...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/sys...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/x...@useless-runes.lsp
R books/projects/x86isa/machine/instructions/fp/.sys/bit...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/fp/.sys/cvt-...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/fp/.sys/shuffle-a...@useless-runes.lsp
M books/projects/x86isa/proofs/codewalker-examples/.sys/fact...@useless-runes.lsp
M books/projects/x86isa/proofs/popcount/.sys/popcount...@useless-runes.lsp
M books/projects/x86isa/proofs/utilities/app-view/.sys/user-level-...@useless-runes.lsp
M books/projects/x86isa/proofs/utilities/sys-view/.sys/marking-...@useless-runes.lsp
M books/projects/x86isa/proofs/utilities/sys-view/.sys/marking-v...@useless-runes.lsp
M books/projects/x86isa/proofs/utilities/sys-view/.sys/non-markin...@useless-runes.lsp
M books/projects/x86isa/proofs/utilities/sys-view/.sys/physical-m...@useless-runes.lsp
M books/projects/x86isa/proofs/utilities/sys-view/paging/.sys/common-pag...@useless-runes.lsp
M books/projects/x86isa/proofs/utilities/sys-view/paging/.sys/gather-pagin...@useless-runes.lsp
M books/projects/x86isa/proofs/utilities/sys-view/paging/.sys/page-dir-ptr...@useless-runes.lsp
M books/projects/x86isa/proofs/utilities/sys-view/paging/.sys/page-direc...@useless-runes.lsp
M books/projects/x86isa/proofs/utilities/sys-view/paging/.sys/t...@useless-runes.lsp
M books/projects/x86isa/proofs/utilities/sys-view/paging/.sys/t...@useless-runes.lsp
M books/projects/x86isa/proofs/wordCount/.sys/w...@useless-runes.lsp
M books/projects/x86isa/proofs/zeroCopy/marking-view/.sys/read-page-after-w...@useless-runes.lsp
M books/projects/x86isa/tools/execution/.sys/init-...@useless-runes.lsp
M books/projects/x86isa/utils/.sys/paging-s...@useless-runes.lsp
M books/projects/x86isa/utils/.sys/segmentatio...@useless-runes.lsp
M books/std/alists/.sys/alist...@useless-runes.lsp
M books/std/omaps/.sys/as...@useless-runes.lsp
A books/std/omaps/.sys/clo...@useless-runes.lsp
M books/std/omaps/.sys/compa...@useless-runes.lsp
A books/std/omaps/.sys/com...@useless-runes.lsp
M books/std/omaps/.sys/co...@useless-runes.lsp
M books/std/omaps/.sys/del...@useless-runes.lsp
M books/std/omaps/.sys/extensi...@useless-runes.lsp
M books/std/omaps/.sys/from-...@useless-runes.lsp
M books/std/omaps/.sys/from-...@useless-runes.lsp
A books/std/omaps/.sys/iden...@useless-runes.lsp
A books/std/omaps/.sys/injec...@useless-runes.lsp
A books/std/omaps/.sys/inv...@useless-runes.lsp
A books/std/omaps/.sys/restric...@useless-runes.lsp
A books/std/omaps/.sys/rest...@useless-runes.lsp
M books/std/omaps/.sys/sub...@useless-runes.lsp
M books/std/omaps/.sys/upd...@useless-runes.lsp
R books/std/omaps/.sys/with-fixin...@useless-runes.lsp
M books/std/strings/.sys/bin-digit-...@useless-runes.lsp
M books/std/strings/.sys/dec-digit-...@useless-runes.lsp
M books/std/strings/.sys/hex-digit-...@useless-runes.lsp
M books/std/strings/.sys/oct-digit-...@useless-runes.lsp
A books/std/system/.sys/current-pa...@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/system/apply/.sys/apply...@useless-runes.lsp
A books/system/tests/.sys/encap-def...@useless-runes.lsp
A books/system/tests/.sys/encap-de...@useless-runes.lsp
A books/unicode/.sys/d...@useless-runes.lsp
M books/unicode/.sys/read...@useless-runes.lsp
M books/unicode/.sys/uc...@useless-runes.lsp
M books/unicode/.sys/utf8-...@useless-runes.lsp
M books/unicode/.sys/utf8-...@useless-runes.lsp
M books/workshops/2020/sswords-rewriter/.sys/sup...@useless-runes.lsp
M books/workshops/2023/coglio-mccarthy-smith/.sys/pf...@useless-runes.lsp
M books/workshops/2023/coglio-mccarthy-smith/.sys/r1...@useless-runes.lsp

Log Message:
-----------
Merge remote-tracking branch 'upstream/testing-kestrel'


Commit: 15cc3ea408ca27fa3cb85f02a39f0a2585dae52a
https://github.com/acl2/acl2/commit/15cc3ea408ca27fa3cb85f02a39f0a2585dae52a
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp

Log Message:
-----------
[JSONRPC] Add jsonrpc/top to kestrel/top and kestrel/top-doc

Co-Authored-By: Claude Sonnet 4.6 <nor...@anthropic.com>


Commit: d77dfb21dffd475caae724038d584e48fb25e240
https://github.com/acl2/acl2/commit/d77dfb21dffd475caae724038d584e48fb25e240
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/process-rpc.lisp

Log Message:
-----------
[JSONRPC] fixed doc issue


Commit: 7f663f15978f47b36263ddcc9ef55b65bef9ca0a
https://github.com/acl2/acl2/commit/7f663f15978f47b36263ddcc9ef55b65bef9ca0a
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/json-to-string.lisp

Log Message:
-----------
[JSONRPC] fixed doc issues


Commit: c9cf2efe42a306f1cbf91639a55f5278e6f4f707
https://github.com/acl2/acl2/commit/c9cf2efe42a306f1cbf91639a55f5278e6f4f707
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/process-rpc.lisp
M books/kestrel/jsonrpc/socket.lisp

Log Message:
-----------
[JSONRPC] fixed doc issues


Commit: 79798991018c5ad82ce94dfac2af1831f4d94f38
https://github.com/acl2/acl2/commit/79798991018c5ad82ce94dfac2af1831f4d94f38
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/top.lisp

Log Message:
-----------
[JSONRPC] fixed doc issues


Commit: 3c453ba2df5ab651716d80e92c8aba18b3dae58e
https://github.com/acl2/acl2/commit/3c453ba2df5ab651716d80e92c8aba18b3dae58e
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/json-to-string.lisp
M books/kestrel/jsonrpc/process-rpc.lisp
M books/kestrel/jsonrpc/socket.lisp
M books/kestrel/jsonrpc/top.lisp
M books/kestrel/jsonrpc/types.lisp

Log Message:
-----------
[JSONRPC] fix doc issues


Commit: 3368bfc449064421e493ffe2ce8ae18a42afb427
https://github.com/acl2/acl2/commit/3368bfc449064421e493ffe2ce8ae18a42afb427
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/cert.acl2
M books/kestrel/jsonrpc/package.lsp
M books/kestrel/jsonrpc/portcullis.acl2
M books/kestrel/jsonrpc/top.lisp

Log Message:
-----------
[JSONRPC] fixed files not ending with newline


Commit: 0ee74944639f9ede546713cf0265ab1c377a6278
https://github.com/acl2/acl2/commit/0ee74944639f9ede546713cf0265ab1c377a6278
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/json-request.txt
M books/kestrel/jsonrpc/json-response.txt
M books/kestrel/jsonrpc/socket-raw.lsp
M books/kestrel/jsonrpc/socket.lisp
M books/kestrel/jsonrpc/top.lisp

Log Message:
-----------
[JSON] updated sockets to allow multiple connections


Commit: be0c1b25270878a13ea784f2fe0d03c49a3d035c
https://github.com/acl2/acl2/commit/be0c1b25270878a13ea784f2fe0d03c49a3d035c
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
R books/kestrel/jsonrpc/json-request.txt
R books/kestrel/jsonrpc/json-response.txt
M books/kestrel/jsonrpc/parse-rpc.lisp

Log Message:
-----------
[JSONRPC] small fix


Commit: 21c06988bad9d50f4ecd5c084929e4d42b4544f8
https://github.com/acl2/acl2/commit/21c06988bad9d50f4ecd5c084929e4d42b4544f8
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
A books/kestrel/jsonrpc/example-request.json
M books/kestrel/jsonrpc/subtract-example.lisp

Log Message:
-----------
[JSONRPC] add example-request.json


Commit: af5b9e0acfcb681344795dc03431866b862db8ba
https://github.com/acl2/acl2/commit/af5b9e0acfcb681344795dc03431866b862db8ba
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
A books/kestrel/jsonrpc/.gitignore

Log Message:
-----------
[JSONRPC] add .gitignore


Commit: e087174069d8ed9f1cbec48665038296575e8fc6
https://github.com/acl2/acl2/commit/e087174069d8ed9f1cbec48665038296575e8fc6
Author: Grant Jurgensen <gr...@kestrel.edu>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
A books/kestrel/jsonrpc/.gitignore
A books/kestrel/jsonrpc/acl2-customization.lsp
A books/kestrel/jsonrpc/cert.acl2
A books/kestrel/jsonrpc/example-request.json
A books/kestrel/jsonrpc/json-to-string.lisp
A books/kestrel/jsonrpc/package.lsp
A books/kestrel/jsonrpc/parse-rpc.lisp
A books/kestrel/jsonrpc/portcullis.acl2
A books/kestrel/jsonrpc/portcullis.lisp
A books/kestrel/jsonrpc/process-rpc.lisp
A books/kestrel/jsonrpc/response.lisp
A books/kestrel/jsonrpc/socket-raw.lsp
A books/kestrel/jsonrpc/socket.lisp
A books/kestrel/jsonrpc/subtract-example.lisp
A books/kestrel/jsonrpc/top.lisp
A books/kestrel/jsonrpc/types.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp

Log Message:
-----------
Merge pull request #1954 from ltmquan/kestrel

JSONRPC - An interface for handling JSON-RPC 2.0 requests via sockets


Compare: https://github.com/acl2/acl2/compare/b80b4da39cd5...e087174069d8

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

Grant Jurgensen

unread,
Jun 18, 2026, 4:38:55 PM (5 days ago) Jun 18
to acl2-...@googlegroups.com
Branch: refs/heads/master

Grant Jurgensen

unread,
Jun 18, 2026, 4:39:45 PM (5 days ago) Jun 18
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Jun 19, 2026, 1:48:31 AM (5 days ago) Jun 19
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: 1315e93ab017590e06b8c05e6610c9926f7a164d
https://github.com/acl2/acl2/commit/1315e93ab017590e06b8c05e6610c9926f7a164d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-values.lisp

Log Message:
-----------
[Remora] Add an operation on values.

This is to retrieve the cells of the arguments of a function application.


Commit: 069f34f725ee0652d60dc2d89fe41c53c2b6f990
https://github.com/acl2/acl2/commit/069f34f725ee0652d60dc2d89fe41c53c2b6f990
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-values.lisp

Log Message:
-----------
[Remora] Add some theorems.


Commit: 9a7ae3dec76b370b471f96937ef59987e6987360
https://github.com/acl2/acl2/commit/9a7ae3dec76b370b471f96937ef59987e6987360
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-values.lisp

Log Message:
-----------
[Remora] Fix some XDOC parents.


Commit: 8099f676c6e20e0b4f8b2d06ebe7b09307d56345
https://github.com/acl2/acl2/commit/8099f676c6e20e0b4f8b2d06ebe7b09307d56345
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Add a lifting operation on values.


Commit: ea6209028d1348a1eb3f31ee25b52818ee5972c3
https://github.com/acl2/acl2/commit/ea6209028d1348a1eb3f31ee25b52818ee5972c3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Fix LaTeX typo.


Commit: 2e1ae77ca4041f5fc8d41210d76ec5f10540fb03
https://github.com/acl2/acl2/commit/2e1ae77ca4041f5fc8d41210d76ec5f10540fb03
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Fix some doc.


Commit: 578afdf31f7d96dfc41ae839533b74be96144456
https://github.com/acl2/acl2/commit/578afdf31f7d96dfc41ae839533b74be96144456
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/lists.lisp

Log Message:
-----------
[Remora] Add a list operation.


Commit: 21fc08df852618d93f91177576a01d3562306bbe
https://github.com/acl2/acl2/commit/21fc08df852618d93f91177576a01d3562306bbe
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-values.lisp

Log Message:
-----------
[Remora] Add a result fixtype.


Commit: 69411422d4dace2f0ef95e3f6d839757b6482813
https://github.com/acl2/acl2/commit/69411422d4dace2f0ef95e3f6d839757b6482813
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Add value lifting for lists of values.


Commit: ddfee03933f095a595ed0340e8a7ed6a96a25038
https://github.com/acl2/acl2/commit/ddfee03933f095a595ed0340e8a7ed6a96a25038
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/lists.lisp

Log Message:
-----------
[Remora] Fix a variable name.


Commit: 85d9f15eb8f651dfd09c65cbdb543a97180448cc
https://github.com/acl2/acl2/commit/85d9f15eb8f651dfd09c65cbdb543a97180448cc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-values.lisp

Log Message:
-----------
[Remora] Add some result fixtypes.


Commit: 2b208d0a8547d32e886748b58527ac1448f1cdc2
https://github.com/acl2/acl2/commit/2b208d0a8547d32e886748b58527ac1448f1cdc2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-semantics.lisp
A books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
[Remora] Start formalizing evaluation of primitives.


Commit: be3375f0d6e757443748e61a9161ece022fd320c
https://github.com/acl2/acl2/commit/be3375f0d6e757443748e61a9161ece022fd320c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
R books/projects/abnf/constructor-utilities.lisp
R books/projects/abnf/notation/convenience-constructors.lisp
M books/projects/abnf/notation/core-rules.lisp
M books/projects/abnf/notation/top.lisp
A books/projects/abnf/syntax-operations/constructor-utilities.lisp
A books/projects/abnf/syntax-operations/convenience-constructors.lisp
A books/projects/abnf/syntax-operations/top.lisp
M books/projects/abnf/top.lisp

Log Message:
-----------
Merge.


Commit: b7667168124e7bc110adaed8d0616e273e1381cc
https://github.com/acl2/acl2/commit/b7667168124e7bc110adaed8d0616e273e1381cc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/projects/pfcs/parser.lisp

Log Message:
-----------
[PFCS] Adapt to changes to ABNF library.


Commit: 4c64eec16f3acc01b44f9d042184f8e99d55b647
https://github.com/acl2/acl2/commit/4c64eec16f3acc01b44f9d042184f8e99d55b647
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/projects/aleo/vm/language/early-version/parser.lisp

Log Message:
-----------
[Aleo] Adapt to changes to ABNF library.


Commit: 1211345029e9df713b85c8f72aa88fd41132d6c5
https://github.com/acl2/acl2/commit/1211345029e9df713b85c8f72aa88fd41132d6c5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/projects/aleo/vm/language/early-version/parser.lisp
M books/projects/pfcs/parser.lisp

Log Message:
-----------
Merge.


Commit: 9eaa6305de3f011203e5acd163155dba437df0b5
https://github.com/acl2/acl2/commit/9eaa6305de3f011203e5acd163155dba437df0b5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/lists.lisp

Log Message:
-----------
[Remora] Add some list theorems.


Commit: 16b62754ca3ae1c0947cf7e3f4429181dd8852c8
https://github.com/acl2/acl2/commit/16b62754ca3ae1c0947cf7e3f4429181dd8852c8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/nat-lists.lisp

Log Message:
-----------
[Remora] Add some theorems on lists of naturals.


Commit: 799aba33c94d92ffc0aefecb8a6ccd422d6540ab
https://github.com/acl2/acl2/commit/799aba33c94d92ffc0aefecb8a6ccd422d6540ab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/nat-lists.lisp

Log Message:
-----------
[Remora] Move a theorem.


Commit: 337d94855ce34afa0ee9816bb1aefb981d474b69
https://github.com/acl2/acl2/commit/337d94855ce34afa0ee9816bb1aefb981d474b69
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-values.lisp

Log Message:
-----------
[Remora] Add a theorem.


Commit: 7fecb32f02b0cdb5ac59c5f8a584664d5b46cfc2
https://github.com/acl2/acl2/commit/7fecb32f02b0cdb5ac59c5f8a584664d5b46cfc2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Add lifting to function application.


Commit: 220e1af9b63aa659c208f09770b33af00c4cfd96
https://github.com/acl2/acl2/commit/220e1af9b63aa659c208f09770b33af00c4cfd96
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/transformation/cert.acl2
M books/kestrel/c/transformation/split-gso.lisp
A books/kestrel/c/transformation/struct-type-split-doc.lisp
A books/kestrel/c/transformation/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/.gitignore
A books/kestrel/c/transformation/tests/struct-type-split/acl2-customization.lsp
A books/kestrel/c/transformation/tests/struct-type-split/anon-member.c
A books/kestrel/c/transformation/tests/struct-type-split/array.c
A books/kestrel/c/transformation/tests/struct-type-split/cert.acl2
A books/kestrel/c/transformation/tests/struct-type-split/fn-param.c
A books/kestrel/c/transformation/tests/struct-type-split/fn-proto.c
A books/kestrel/c/transformation/tests/struct-type-split/impure-init.c
A books/kestrel/c/transformation/tests/struct-type-split/member.c
A books/kestrel/c/transformation/tests/struct-type-split/mixed-init.c
A books/kestrel/c/transformation/tests/struct-type-split/multi1.c
A books/kestrel/c/transformation/tests/struct-type-split/multi2.c
A books/kestrel/c/transformation/tests/struct-type-split/positional-init.c
A books/kestrel/c/transformation/tests/struct-type-split/ptr-member.c
A books/kestrel/c/transformation/tests/struct-type-split/ret-struct.c
A books/kestrel/c/transformation/tests/struct-type-split/self-ref.c
A books/kestrel/c/transformation/tests/struct-type-split/sizeof.c
A books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/test1.c
A books/kestrel/c/transformation/tests/struct-type-split/test2.c
A books/kestrel/c/transformation/tests/struct-type-split/typedef-ptr.c
A books/kestrel/c/transformation/tests/struct-type-split/typedef.c
A books/kestrel/c/transformation/tests/struct-type-split/union-member.c
A books/kestrel/c/transformation/tests/struct-type-split/union.c
M books/kestrel/c/transformation/top.lisp
M books/kestrel/c/transformation/utilities/cert.acl2
A books/kestrel/c/transformation/utilities/context-msg.lisp
A books/kestrel/c/transformation/utilities/print-to-str.lisp
A books/kestrel/fty/msg-list.lisp
A books/kestrel/fty/msg.lisp
M books/kestrel/fty/top.lisp

Log Message:
-----------
Merge.


Commit: 50662695fd66b4e7b12216ae412d9e4fbe8fa7b8
https://github.com/acl2/acl2/commit/50662695fd66b4e7b12216ae412d9e4fbe8fa7b8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
M books/kestrel/remora/dynamic-semantics.lisp
M books/kestrel/remora/dynamic-values.lisp
A books/kestrel/remora/primitives-evaluation.lisp
R books/projects/abnf/constructor-utilities.lisp
R books/projects/abnf/notation/convenience-constructors.lisp
M books/projects/abnf/notation/core-rules.lisp
M books/projects/abnf/notation/top.lisp
A books/projects/abnf/syntax-operations/constructor-utilities.lisp
A books/projects/abnf/syntax-operations/convenience-constructors.lisp
A books/projects/abnf/syntax-operations/top.lisp
M books/projects/abnf/top.lisp
M books/projects/aleo/vm/language/early-version/parser.lisp
M books/projects/pfcs/parser.lisp

Log Message:
-----------
Merge.


Commit: f1e53e3aae2d30dea3aa80f82945fdb46db50b3d
https://github.com/acl2/acl2/commit/f1e53e3aae2d30dea3aa80f82945fdb46db50b3d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Reduce some hints.


Commit: 84b728ec6640a181417a8a783415b1e75fcb12c3
https://github.com/acl2/acl2/commit/84b728ec6640a181417a8a783415b1e75fcb12c3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-15 (Mon, 15 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Make fixing a bit less prominent.


Commit: fb265ab937fab8a6216048e639e6447b95517c29
https://github.com/acl2/acl2/commit/fb265ab937fab8a6216048e639e6447b95517c29
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-06-16 (Tue, 16 Jun 2026)
A books/kestrel/c/syntax/tests/.sys/disambiguator-...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/disambiguato...@useless-runes.lsp
R books/kestrel/c/syntax/tests/.sys/disamb...@useless-runes.lsp
M books/kestrel/c/syntax/tests/.sys/preprocessor-...@useless-runes.lsp
M books/kestrel/c/syntax/tests/.sys/vali...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/add-sect...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/constant-p...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/cop...@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
M books/kestrel/c/transformation/.sys/spli...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/variables-in-co...@useless-runes.lsp
M 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/subst-free/.sys/subst...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/add-att...@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
M books/kestrel/c/transformation/utilities/.sys/qualifi...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/subst...@useless-runes.lsp
M books/projects/abnf/grammar-operations/.sys/ambi...@useless-runes.lsp
M books/projects/abnf/grammar-operations/.sys/clo...@useless-runes.lsp
M books/projects/abnf/notation/.sys/sema...@useless-runes.lsp
M books/projects/abnf/parsing-tools/.sys/defde...@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
A books/projects/fields/.sys/embed...@useless-runes.lsp
A books/projects/fields/.sys/exten...@useless-runes.lsp
A books/projects/fields/.sys/gal...@useless-runes.lsp
A books/projects/fields/support/.sys/embed...@useless-runes.lsp
A books/projects/fields/support/.sys/exten...@useless-runes.lsp
A books/projects/fields/support/.sys/gal...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-abstr...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-exp...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-ke...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-mem...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-pars...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-p...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-token...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/cpp-top-le...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/portc...@useless-runes.lsp
A books/projects/filesystems/utilities/cpp-syntax/.sys/t...@useless-runes.lsp
Updated useless-runes files


Commit: 6e383038423b093047c13f26b23e26bff32b87bb
https://github.com/acl2/acl2/commit/6e383038423b093047c13f26b23e26bff32b87bb
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/transformation/cert.acl2
M books/kestrel/c/transformation/split-gso.lisp
A books/kestrel/c/transformation/struct-type-split-doc.lisp
A books/kestrel/c/transformation/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/.gitignore
A books/kestrel/c/transformation/tests/struct-type-split/acl2-customization.lsp
A books/kestrel/c/transformation/tests/struct-type-split/anon-member.c
A books/kestrel/c/transformation/tests/struct-type-split/array.c
A books/kestrel/c/transformation/tests/struct-type-split/cert.acl2
A books/kestrel/c/transformation/tests/struct-type-split/fn-param.c
A books/kestrel/c/transformation/tests/struct-type-split/fn-proto.c
A books/kestrel/c/transformation/tests/struct-type-split/impure-init.c
A books/kestrel/c/transformation/tests/struct-type-split/member.c
A books/kestrel/c/transformation/tests/struct-type-split/mixed-init.c
A books/kestrel/c/transformation/tests/struct-type-split/multi1.c
A books/kestrel/c/transformation/tests/struct-type-split/multi2.c
A books/kestrel/c/transformation/tests/struct-type-split/positional-init.c
A books/kestrel/c/transformation/tests/struct-type-split/ptr-member.c
A books/kestrel/c/transformation/tests/struct-type-split/ret-struct.c
A books/kestrel/c/transformation/tests/struct-type-split/self-ref.c
A books/kestrel/c/transformation/tests/struct-type-split/sizeof.c
A books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/test1.c
A books/kestrel/c/transformation/tests/struct-type-split/test2.c
A books/kestrel/c/transformation/tests/struct-type-split/typedef-ptr.c
A books/kestrel/c/transformation/tests/struct-type-split/typedef.c
A books/kestrel/c/transformation/tests/struct-type-split/union-member.c
A books/kestrel/c/transformation/tests/struct-type-split/union.c
M books/kestrel/c/transformation/top.lisp
M books/kestrel/c/transformation/utilities/cert.acl2
A books/kestrel/c/transformation/utilities/context-msg.lisp
A books/kestrel/c/transformation/utilities/print-to-str.lisp
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
A books/kestrel/fty/msg-list.lisp
A books/kestrel/fty/msg.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/dynamic-semantics.lisp
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/lists.lisp
M books/kestrel/remora/nat-lists.lisp
A books/kestrel/remora/primitives-evaluation.lisp
R books/projects/abnf/constructor-utilities.lisp
R books/projects/abnf/notation/convenience-constructors.lisp
M books/projects/abnf/notation/core-rules.lisp
M books/projects/abnf/notation/top.lisp
A books/projects/abnf/syntax-operations/constructor-utilities.lisp
A books/projects/abnf/syntax-operations/convenience-constructors.lisp
A books/projects/abnf/syntax-operations/top.lisp
M books/projects/abnf/top.lisp
M books/projects/aleo/vm/language/early-version/parser.lisp
M books/projects/pfcs/parser.lisp

Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/master'


Commit: b5e393a24c9d6e3e91c1c21fced9c42767887458
https://github.com/acl2/acl2/commit/b5e393a24c9d6e3e91c1c21fced9c42767887458
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-values.lisp

Log Message:
-----------
[Remora] Add theorems.


Commit: 26b8e55d16a6d716e27a878309fcb975f34e3040
https://github.com/acl2/acl2/commit/26b8e55d16a6d716e27a878309fcb975f34e3040
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp

Log Message:
-----------
[cpp-syntax] Speed up a file.


Commit: d17801e14737b52c6488947551977425d5903995
https://github.com/acl2/acl2/commit/d17801e14737b52c6488947551977425d5903995
Author: Mihir Mehta <mi...@cs.utexas.edu>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp

Log Message:
-----------
Merge pull request #1955 from acl2/cpp-speedups

[cpp-syntax] Speed up a file.


Commit: 79ca5f613de76dd135c1cc2f946a21789fccf264
https://github.com/acl2/acl2/commit/79ca5f613de76dd135c1cc2f946a21789fccf264
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
[C$] Assign unique identifiers to typedefs

Extend the typedef validation info and the typedef name type specifier annotation with a UID. Assign a fresh UID at each typedef declaration, reusing the existing one when a typedef is redefined in the same scope with a compatible type. Record the declaration's UID at each typedef name use site.

Since every initializer declarator now declares an object, function, or typedef name, all of which receive UIDs, make the init-declor-info UID required rather than optional, updating the transformation utilities that read it. Add validator tests covering typedef UID assignment, redefinition, use sites, and inner-scope shadowing.


Commit: 350c3cc80f89f6eb7fc686180d38f4b80f5dfde5
https://github.com/acl2/acl2/commit/350c3cc80f89f6eb7fc686180d38f4b80f5dfde5
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
Merge branch 'gj-validator-typedef' into testing-kestrel


Commit: 7dd2e5c9db06edde49860f5ea6e1cf27101005c2
https://github.com/acl2/acl2/commit/7dd2e5c9db06edde49860f5ea6e1cf27101005c2
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp

Log Message:
-----------
[C2C] Fix struct-type-split for non-optional typedef uid field

The [C$] validator now assigns a non-optional `uid` field to the info
defprods (init-declor-info, param-declor-nonabstract-info), replacing the
old optional `uid?`. init-declor-sts-split still referenced the removed
info.uid?, breaking certification. Mirror the already-migrated
param-declor-sts-split: drop the now-dead "(not info.uid?)" internal-error
guard (a uid defprod is never nil) and use info.uid.


Commit: 568df750b73e6ad6c9e802e684ab79753e1389a0
https://github.com/acl2/acl2/commit/568df750b73e6ad6c9e802e684ab79753e1389a0
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/typedef-chain.c

Log Message:
-----------
[C2C] Support typedefs of the split struct type.

Now that the validator assigns unique identifiers to typedefs, a typedef
of a splittable type is split into a parallel right typedef, and uses of
the typedef name are substituted via the identifier map. Typedef
declarations reuse the existing uid-keyed declarator renaming, so the
core change is the type-spec typedef use case; the four rejection sites
and two detectors are removed. Add tests for direct, pointer, and chained
typedefs.


Commit: 8c2a205f1091b758ad1764e488a4b54902673462
https://github.com/acl2/acl2/commit/8c2a205f1091b758ad1764e488a4b54902673462
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/typedef-chain.c
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
Merge commit '568df750b73e6ad6c9e802e684ab79753e1389a0' into HEAD


Commit: 2fb6a50f835e33f0116718b5680f958e19de7e3f
https://github.com/acl2/acl2/commit/2fb6a50f835e33f0116718b5680f958e19de7e3f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/lists.lisp

Log Message:
-----------
[Remora] Add a list operation.


Commit: 56bd9fe74b1835781ae91631e31d57f8636cf59e
https://github.com/acl2/acl2/commit/56bd9fe74b1835781ae91631e31d57f8636cf59e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp

Log Message:
-----------
[Remora] Add a fixtype.


Commit: 8a88f46aa2922d8aa93e921d1a1ad29956c3783c
https://github.com/acl2/acl2/commit/8a88f46aa2922d8aa93e921d1a1ad29956c3783c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp

Log Message:
-----------
[Remora] add a structural op and theorem.


Commit: 9aac563a755c203aaff7d5303cb2df8ad6ee0550
https://github.com/acl2/acl2/commit/9aac563a755c203aaff7d5303cb2df8ad6ee0550
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/ispace-equivalence.lisp

Log Message:
-----------
[Remora] Slightly change ispace normalization.

Instead of normalizing to the `:dim` summand of `shape`, normalize to singleton
lists in the `:dims` summand of `shape`, because `:dim` will be removed.


Commit: 0c36eb5d7288cd261e17abb785c2624896858135
https://github.com/acl2/acl2/commit/0c36eb5d7288cd261e17abb785c2624896858135
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/desugaring.lisp

Log Message:
-----------
[Remora] Slightly change core and desugaring.

Avoid the `:dim` summand of `shape` in favor of `:dims` with singleton lists.
The `:dim` summand will be eliminated.


Commit: 494204ea609e352a9d8d66dbb162f7f143f298a7
https://github.com/acl2/acl2/commit/494204ea609e352a9d8d66dbb162f7f143f298a7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/bound-and-free-variable-operations.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp

Log Message:
-----------
[Remora] Join shape and ispaces into AST clique.

This does not change the definitions, but puts shape and ispace ASTs under the
same `fty::deftypes` clique, as a preliminary step towards making them actually
mutually recursive.

We adapt what's needed, particularly calls of `deffold-...`.


Commit: 7da28795b772cf5cd343fa5ed7d1c8096c0ed09c
https://github.com/acl2/acl2/commit/7da28795b772cf5cd343fa5ed7d1c8096c0ed09c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp

Log Message:
-----------
[Remora] Improve type splice ASTs.

Use ispaces instead of shapes, in preparation for the elimination of dimensions
auto-lifted to shapes.

A number of things had to be adapted to this change.


Commit: 5012d0bdb316eaa6dd4f02dc37fa0b3e2eaffa53
https://github.com/acl2/acl2/commit/5012d0bdb316eaa6dd4f02dc37fa0b3e2eaffa53
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
[Remora] Improve some naming and nomenclature.

Use 'expression value' for the values that expressions evaluate to, which is
symmetric with 'type value' and 'ispace value'.


Commit: 9125a39f1856542bdae867e808ce8c30ae4285ca
https://github.com/acl2/acl2/commit/9125a39f1856542bdae867e808ce8c30ae4285ca
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/typedef-chain.c
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp

Log Message:
-----------
Merge.


Commit: 3b2b54c4846550ee7c852305464f671a368ce15a
https://github.com/acl2/acl2/commit/3b2b54c4846550ee7c852305464f671a368ce15a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/primitives-evaluation.lisp

Log Message:
-----------
Merge.


Commit: 441a665d50656d6d1b8024b66db8647be82f3309
https://github.com/acl2/acl2/commit/441a665d50656d6d1b8024b66db8647be82f3309
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp

Log Message:
-----------
[Remora] Reorder some code.


Commit: 01f1f4d1fd045dc859ec05b2e3e81ae06152a81b
https://github.com/acl2/acl2/commit/01f1f4d1fd045dc859ec05b2e3e81ae06152a81b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/dynamic-semantics.lisp
R books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/type-value-equivalence.lisp
A books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Rename a file and topic.


Commit: d667c4f9b523ba9da444c9b63777b14e0b2076ba
https://github.com/acl2/acl2/commit/d667c4f9b523ba9da444c9b63777b14e0b2076ba
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/type-value-equivalence.lisp
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Improve a fixtype field name.


Commit: 052c23397d89243ebeda08a11638775541f24ae4
https://github.com/acl2/acl2/commit/052c23397d89243ebeda08a11638775541f24ae4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Add an op on ispace values.


Commit: d29f9c209df11fc2b9bed5e4fd5d9e0722535a99
https://github.com/acl2/acl2/commit/d29f9c209df11fc2b9bed5e4fd5d9e0722535a99
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Shorten a function definition.


Commit: 729ab0623a19dfea3b4ba789020c56bf611218b6
https://github.com/acl2/acl2/commit/729ab0623a19dfea3b4ba789020c56bf611218b6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/ispace-equivalence.lisp

Log Message:
-----------
[Remora] Improve ispace equivalence.

Add operations for actual ispace, vs. just shape, equivalence.

Add some theorems.


Commit: c90fe281c2f8a2bf1a55503466469ecff47b1810
https://github.com/acl2/acl2/commit/c90fe281c2f8a2bf1a55503466469ecff47b1810
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-matching-operations.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp

Log Message:
-----------
[Remora] Improve some ASTs.

Use ispaces in array types.


Commit: c76d1fe5c34eab5fa0cc4b120e3d11882f18d860
https://github.com/acl2/acl2/commit/c76d1fe5c34eab5fa0cc4b120e3d11882f18d860
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Improve some ASTs.

Use ispaces instead of shapes in bracket types.


Commit: 1786593535ed1044e808ef24bf5e45b0955f82e4
https://github.com/acl2/acl2/commit/1786593535ed1044e808ef24bf5e45b0955f82e4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-16 (Tue, 16 Jun 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-structurals.lisp

Log Message:
-----------
[Remora] Remove function no longer needed.


Commit: cdb4cbdc58ec313f9e5d84a6e8d9b13610725c2c
https://github.com/acl2/acl2/commit/cdb4cbdc58ec313f9e5d84a6e8d9b13610725c2c
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/set-theory/base.lisp
R books/projects/set-theory/change-pkg.lisp
M books/projects/set-theory/doc.lisp
A books/projects/set-theory/finite/base.lisp
A books/projects/set-theory/finite/finite-domain.lisp
A books/projects/set-theory/finite/finite-restrict.lisp
A books/projects/set-theory/finite/finite-union2.lisp
A books/projects/set-theory/finite/top.lisp
A books/projects/set-theory/image-plus.lisp
A books/projects/set-theory/intersection.lisp
M books/projects/set-theory/package.lsp
A books/projects/set-theory/phoenix.lisp
M books/projects/set-theory/set-algebra.lisp
M books/projects/set-theory/top.lisp
A books/projects/set-theory/topology/cert.acl2
A books/projects/set-theory/topology/compact.lisp
A books/projects/set-theory/topology/finite-intersection-closure.lisp
A books/projects/set-theory/topology/normal.lisp
A books/projects/set-theory/topology/prelims.lisp
A books/projects/set-theory/topology/subspace.lisp
A books/projects/set-theory/utilities/change-pkg.lisp
A books/projects/set-theory/utilities/remove-hypz.lisp
A books/projects/set-theory/zfns.lisp

Log Message:
-----------
Extended the set-theory library, motivated by making a start on a topology library (in books/projects/set-theory/topology/)

Note: Claude Fable 5 (run by Eric Smith, using the interface provided
by Eric McCarthy) assisted with a proof in
books/projects/set-theory/topology/finite-intersection-closure.lisp,
as noted in comments there. I was impressed.

I removed some lemmas in books/projects/hol-in-acl2/acl2/lemmas.lisp
that were added to the set-theory library to support development of
the topology library.

Regarding this effort:

A lot of this work was driven by a goal of proving the theorem in
topology that every compact Hausdorff space is normal. I haven't done
that yet, but I intend to do so. I'm not going to claim any sort of
grand accomplishment if and when I do, though. Consider for example
Josef Urban's "130k Lines of Formal Topology in Two Weeks: Simple and
Cheap Autoformalization for Everyone"
(https://arxiv.org/pdf/2601.03298), in particular the theorem
paracompact_Hausdorff_normal, which I believe is a formalization that
every paracompact Hausdorff space is normal, which is probably a much
deeper result than that every compact Hausdorff space is normal. I
think that also, John Harrison reported a fully automatic proof, via
AI, of that deeper theorem. I don't know how much library support for
set theory was already in place for those efforts. My main goal in
proving the (again) simpler theorem that compact Hausdorff spaces are
normal (again, not yet done!) is just to show that ACL2 with set
theory, which I'm now calling ACL2(zfc) -- and which, unlike the two
systems mentioned above, is based on first order logic -- can be used
to do such proofs. My secondary goal is to push development of the
set theory library. As that library continues to be fleshed out and
as AI continues to further its reach, perhaps many such proofs can
eventually be done automatically.


Commit: ae74fae4b052451567eebbb667c4409d9305120e
https://github.com/acl2/acl2/commit/ae74fae4b052451567eebbb667c4409d9305120e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

Log Message:
-----------
[C$] Make some doc more precise.
Commit: 18677beeac40b0c20d0359db37c8c6c765ca8fe4
https://github.com/acl2/acl2/commit/18677beeac40b0c20d0359db37c8c6c765ca8fe4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp

Log Message:
-----------
[C$] Fix bug in disambiguator.

There was a missing check for turning function parameter declarators to function
name declarators (in C17).

Thanks to Grant Jurgensen for running the disambiguator on an example that led
to the discovery of the bug.


Commit: a9542c5a8cdb80ba5f46cd8f391cf35555943178
https://github.com/acl2/acl2/commit/a9542c5a8cdb80ba5f46cd8f391cf35555943178
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/tests/disambiguator-trans-units.lisp

Log Message:
-----------
[C$] Add a disambiguator test.

This demonstrates the fix in the previous commit.


Commit: 094e32b11c33042bf8cf7682d0d767c9c4d99671
https://github.com/acl2/acl2/commit/094e32b11c33042bf8cf7682d0d767c9c4d99671
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp

Log Message:
-----------
[C$] Add a validator test.

This was failing prior to the disambiguator fix in the commit before the
previous one.


Commit: 3248d27c6d0465a9eb39a7fd8d0b57aa6baa9935
https://github.com/acl2/acl2/commit/3248d27c6d0465a9eb39a7fd8d0b57aa6baa9935
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M rewrite.lisp
M type-set-b.lisp

Log Message:
-----------
Improved some comments about ancestors.

Thanks to J for suggesting such improvements.

These are comment changes only, so I only did a build, not a regression.


Commit: 242105ca416a13d790b5b286d732af4c3498e36f
https://github.com/acl2/acl2/commit/242105ca416a13d790b5b286d732af4c3498e36f
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/tests/disambiguator-trans-units.lisp
M books/kestrel/c/syntax/tests/validator.lisp

Log Message:
-----------
Merge commit '094e32b11c33042bf8cf7682d0d767c9c4d99671' into HEAD
Commit: 37645084fbbdeb62476a023ec9654f1287a8de5f
https://github.com/acl2/acl2/commit/37645084fbbdeb62476a023ec9654f1287a8de5f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/projects/abnf/top.lisp
A books/projects/abnf/tree-operations/top.lisp

Log Message:
-----------
[ABNF] Start a subdir and topic for tree operations.


Commit: eeb6bad754147700996048615d18dd0c1872f839
https://github.com/acl2/acl2/commit/eeb6bad754147700996048615d18dd0c1872f839
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/remora/syntax-abstraction.lisp
M books/projects/abnf/top.lisp
M books/projects/abnf/tree-operations/top.lisp
A books/projects/abnf/tree-operations/tree-utilities.lisp
R books/projects/abnf/tree-utilities.lisp
M books/projects/aleo/leo/early-version/definition/syntax-abstraction.lisp
M books/projects/aleo/leo/early-version/definition/tokenizer.lisp
M books/projects/aleo/leo/early-version/testing/lexing.lisp
M books/projects/pfcs/syntax-abstraction.lisp
M books/projects/pfcs/tokenizer.lisp

Log Message:
-----------
[ABNF] Move some tree ops under the new subdir/topic.


Commit: 45e87b2ecb22830eb4fb0ed37feea46454460063
https://github.com/acl2/acl2/commit/45e87b2ecb22830eb4fb0ed37feea46454460063
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/remora/bound-and-free-variable-operations.lisp

Log Message:
-----------
[Remora] Fix free variable calculations.

They were treating the bindings in a `let` as parallel.


Commit: d608ab63dee1c05ac6c6eee4195adb7a131056ef
https://github.com/acl2/acl2/commit/d608ab63dee1c05ac6c6eee4195adb7a131056ef
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/remora/syntax-abstraction.lisp
M books/projects/abnf/top.lisp
A books/projects/abnf/tree-operations/top.lisp
A books/projects/abnf/tree-operations/tree-utilities.lisp
R books/projects/abnf/tree-utilities.lisp
M books/projects/aleo/leo/early-version/definition/syntax-abstraction.lisp
M books/projects/aleo/leo/early-version/definition/tokenizer.lisp
M books/projects/aleo/leo/early-version/testing/lexing.lisp
M books/projects/pfcs/syntax-abstraction.lisp
M books/projects/pfcs/tokenizer.lisp

Log Message:
-----------
Merge.


Commit: b5b564b68a9793c1c079fee7be08af8e67e84641
https://github.com/acl2/acl2/commit/b5b564b68a9793c1c079fee7be08af8e67e84641
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/remora/type-checking.lisp

Log Message:
-----------
[Remora] Add explicit checkers for dimensions.


Commit: 0761c0c6d44647999d7370953c92168011e0cc44
https://github.com/acl2/acl2/commit/0761c0c6d44647999d7370953c92168011e0cc44
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Add some doc.


Commit: b80b4da39cd5c4b565526c93568bdb8e67297143
https://github.com/acl2/acl2/commit/b80b4da39cd5c4b565526c93568bdb8e67297143
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-17 (Wed, 17 Jun 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Extend dynamic semantics.

Add evaluation of combined applications.


Commit: 0ee74944639f9ede546713cf0265ab1c377a6278
https://github.com/acl2/acl2/commit/0ee74944639f9ede546713cf0265ab1c377a6278
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/jsonrpc/json-request.txt
M books/kestrel/jsonrpc/json-response.txt
M books/kestrel/jsonrpc/socket-raw.lsp
M books/kestrel/jsonrpc/socket.lisp
M books/kestrel/jsonrpc/top.lisp

Log Message:
-----------
[JSON] updated sockets to allow multiple connections


Commit: be0c1b25270878a13ea784f2fe0d03c49a3d035c
https://github.com/acl2/acl2/commit/be0c1b25270878a13ea784f2fe0d03c49a3d035c
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
R books/kestrel/jsonrpc/json-request.txt
R books/kestrel/jsonrpc/json-response.txt
M books/kestrel/jsonrpc/parse-rpc.lisp

Log Message:
-----------
[JSONRPC] small fix


Commit: 8313de4e1db7f0297047b100cfba41c4ec76a3d0
https://github.com/acl2/acl2/commit/8313de4e1db7f0297047b100cfba41c4ec76a3d0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp

Log Message:
-----------
[FTY] Improve `deffold-reduce`.

In the generated functions, also make the `:extra-args`, if any,
ignorable. Otherwise certain `:overrides` might cause failure.

Add some demonstrative tests.


Commit: 21c06988bad9d50f4ecd5c084929e4d42b4544f8
https://github.com/acl2/acl2/commit/21c06988bad9d50f4ecd5c084929e4d42b4544f8
Author: ltmquan <ltmqu...@gmail.com>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
A books/kestrel/jsonrpc/example-request.json
M books/kestrel/jsonrpc/subtract-example.lisp

Log Message:
-----------
[JSONRPC] add example-request.json


Commit: 310c578b8026c616c7826621a089bea6ffde4d24
https://github.com/acl2/acl2/commit/310c578b8026c616c7826621a089bea6ffde4d24
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp

Log Message:
-----------
[FTY] Improve `deffold-map`.

Ensure that the `:extra-args`, if present, are declared ignorable in the
generated functions. This was already the case for most types, but not for list
types, which can be overridden. This commit adds that. It also updates the doc
of the other cases, which only mentioned the formal and not the extra args.

Add some demonstrative tests.
Commit: a116d0739e541315355c6a52eb49af699139107a
https://github.com/acl2/acl2/commit/a116d0739e541315355c6a52eb49af699139107a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp

Log Message:
-----------
[C$] Export more symbols.


Commit: 44bbbb4a9dbb87cdcd1541127a6291bb448aebee
https://github.com/acl2/acl2/commit/44bbbb4a9dbb87cdcd1541127a6291bb448aebee
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
A books/kestrel/c/transformation/struct-safety-checks.lisp
M books/kestrel/c/transformation/top.lisp

Log Message:
-----------
[C2C] Start struct safety checks.

These are extremely strict, to the point of not being useful, but they are a
starting point.


Commit: 47a208421c91097d61628e9a875cd5d59efc8a52
https://github.com/acl2/acl2/commit/47a208421c91097d61628e9a875cd5d59efc8a52
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/fty/database.lisp

Log Message:
-----------
[FTY] Add a database query utility.


Commit: 0a8984478608089f2bad12ed8f05825f022c0752
https://github.com/acl2/acl2/commit/0a8984478608089f2bad12ed8f05825f022c0752
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp

Log Message:
-----------
[safestruct] Accept binary expressions.


Commit: 17347c8ae4c5aad39b475046424a4fbf8a94cb70
https://github.com/acl2/acl2/commit/17347c8ae4c5aad39b475046424a4fbf8a94cb70
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/fty/deffold-reduce.lisp

Log Message:
-----------
[FTY] Improve `deffold-reduce`.

Handle finding recognizers of base types, which do not have entries in the FTY
table.


Commit: d800102f900c52cbb64d917c15a137d0d0b1e91b
https://github.com/acl2/acl2/commit/d800102f900c52cbb64d917c15a137d0d0b1e91b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/fty/deffold-map.lisp

Log Message:
-----------
[FTY] Improve `deffold-map`.

Handle finding recognizers of base types, which do not have entries in the FTY
table.


Commit: 105caf57508af2b45afd8568b0ae642404b83199
https://github.com/acl2/acl2/commit/105caf57508af2b45afd8568b0ae642404b83199
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/fty/deffold-map-tests.lisp

Log Message:
-----------
[FTY] Simplify a test.


Commit: 29737382d848f1f208c38ab90c99603857c3739a
https://github.com/acl2/acl2/commit/29737382d848f1f208c38ab90c99603857c3739a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/fty/database.lisp
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp

Log Message:
-----------
Merge.


Commit: ed0517ca35065252382673cb11c8494a8e1a3801
https://github.com/acl2/acl2/commit/ed0517ca35065252382673cb11c8494a8e1a3801
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp

Log Message:
-----------
[C$] Export more symbols.


Commit: 7c26e2b778606026c8cf017a4e7ab7291f0cbad5
https://github.com/acl2/acl2/commit/7c26e2b778606026c8cf017a4e7ab7291f0cbad5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp

Log Message:
-----------
[safestruct] Exclude atomic type qualifiers.


Commit: 506f8fb471da90efa5c096bb76b3bb0c0ed82b51
https://github.com/acl2/acl2/commit/506f8fb471da90efa5c096bb76b3bb0c0ed82b51
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp

Log Message:
-----------
[safestruct] Add some doc.


Commit: 64a53774f31d821c7296275a0865765b2f8d959d
https://github.com/acl2/acl2/commit/64a53774f31d821c7296275a0865765b2f8d959d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp

Log Message:
-----------
[C$] Export more symbols.


Commit: 1b0409aa5e093440352961d230cc2fa601e6ee28
https://github.com/acl2/acl2/commit/1b0409aa5e093440352961d230cc2fa601e6ee28
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
M books/kestrel/c/transformation/struct-safety-checks.lisp

Log Message:
-----------
[safestruct] Elaborate checks.


Commit: 978708391d271438ad21a85619518d33c265bbe0
https://github.com/acl2/acl2/commit/978708391d271438ad21a85619518d33c265bbe0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-06-18 (Thu, 18 Jun 2026)

Changed paths:
A books/kestrel/jsonrpc/.gitignore
A books/kestrel/jsonrpc/acl2-customization.lsp
A books/kestrel/jsonrpc/cert.acl2
A books/kestrel/jsonrpc/example-request.json
A books/kestrel/jsonrpc/json-to-string.lisp
A books/kestrel/jsonrpc/package.lsp
A books/kestrel/jsonrpc/parse-rpc.lisp
A books/kestrel/jsonrpc/portcullis.acl2
A books/kestrel/jsonrpc/portcullis.lisp
A books/kestrel/jsonrpc/process-rpc.lisp
A books/kestrel/jsonrpc/response.lisp
A books/kestrel/jsonrpc/socket-raw.lsp
A books/kestrel/jsonrpc/socket.lisp
A books/kestrel/jsonrpc/subtract-example.lisp
A books/kestrel/jsonrpc/top.lisp
A books/kestrel/jsonrpc/types.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp

Log Message:
-----------
Merge.


Compare: https://github.com/acl2/acl2/compare/ae80770a928b...978708391d27
Reply all
Reply to author
Forward
0 new messages