[acl2/acl2] 6a8c8b: [C strcpy] Fix doc comment.
0 views
Skip to first unread message
Alessandro Coglio
May 28, 2026, 12:02:44 AM (5 days ago) May 28
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 6a8c8bf385281795e4556ef1569dc2b0c92d63db
https://github.com/acl2/acl2/commit/6a8c8bf385281795e4556ef1569dc2b0c92d63db
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-18 (Sat, 18 Apr 2026)
Changed paths:
M books/kestrel/c/examples/strcpy-safe.lisp
Log Message:
-----------
[C strcpy] Fix doc comment.
Commit: 69d92d9634904bab8b6f88b700e0b568f65aefeb
https://github.com/acl2/acl2/commit/69d92d9634904bab8b6f88b700e0b568f65aefeb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-18 (Sat, 18 Apr 2026)
Changed paths:
M books/kestrel/c/language/structure-operations.lisp
Log Message:
-----------
[C] Add a theorem.
Commit: 1a047a6fd55e184ef24b529ec77ef07dbdbca002
https://github.com/acl2/acl2/commit/1a047a6fd55e184ef24b529ec77ef07dbdbca002
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-18 (Sat, 18 Apr 2026)
Changed paths:
M books/kestrel/c/language/array-operations.lisp
Log Message:
-----------
[C] Add two theorems.
Commit: 1790b3c7ce327ecc57b8a6973ee7a74ea26f879e
https://github.com/acl2/acl2/commit/1790b3c7ce327ecc57b8a6973ee7a74ea26f879e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-18 (Sat, 18 Apr 2026)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add a theorem.
Commit: 219450d9609b437a45bd9eead6ade69672f9ee5b
https://github.com/acl2/acl2/commit/219450d9609b437a45bd9eead6ade69672f9ee5b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-20 (Mon, 20 Apr 2026)
Changed paths:
M axioms.lisp
M basis-a.lisp
M books/demos/geneqv-test-log.txt
M books/kestrel/acl2pl/package.lsp
M books/kestrel/java/language/primitive-operations.lisp
M books/kestrel/remora/parser.lisp
A books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/top.lisp
M books/misc/check-acl2-exports.lisp
M books/std/alists/alist-keys.lisp
M books/system/defstobj.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/stobj-help.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
Log Message:
-----------
Merge.
Commit: 1255cfa38de468c37024fc0ed2614b0c8c57ba4b
https://github.com/acl2/acl2/commit/1255cfa38de468c37024fc0ed2614b0c8c57ba4b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-22 (Wed, 22 Apr 2026)
Changed paths:
M books/demos/geneqv-test-log.txt
M books/kestrel/axe/arm/README.md
M books/kestrel/axe/jvm/axe-syntax-functions-jvm.lisp
M books/kestrel/axe/jvm/lifter-utilities.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/output-indicators.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/jvm/tester.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
A books/kestrel/axe/r1cs/README.md
M books/kestrel/axe/risc-v/README.md
M books/kestrel/axe/x86/README.md
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/floats/ieee-floats.lisp
M books/kestrel/floats/round.lisp
M books/kestrel/jvm/acl2-customization.lsp
M books/kestrel/jvm/call-stacks.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/class-tables.lisp
M books/kestrel/jvm/classes.lisp
M books/kestrel/jvm/control-flow.lisp
M books/kestrel/jvm/fields.lisp
M books/kestrel/jvm/floats.lisp
M books/kestrel/jvm/floats2.lisp
M books/kestrel/jvm/frames.lisp
M books/kestrel/jvm/heap.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.lisp
M books/kestrel/jvm/method-indicators.lisp
M books/kestrel/jvm/methods.lisp
M books/kestrel/jvm/states.lisp
M books/kestrel/jvm/symbolic-execution.lisp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/utils/segmentation-structures.lisp
M books/projects/x86isa/utils/structures.lisp
M books/projects/x86isa/utils/utilities.lisp
M books/system/apply/apply-prim.lisp
M boot-strap-pass-2-a.lisp
M induct.lisp
M other-events.lisp
Log Message:
-----------
Merge.
Commit: 438d3f94f35149061f1870bbebb46f25dc27231c
https://github.com/acl2/acl2/commit/438d3f94f35149061f1870bbebb46f25dc27231c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-22 (Wed, 22 Apr 2026)
Changed paths:
A books/kestrel/c/examples/strcpy-safe-induction-support.lisp
Log Message:
-----------
[C examples] Add some tentative generic utilities.
Commit: d0ab8b7d27ac1878b04cc01211f379cef0853140
https://github.com/acl2/acl2/commit/d0ab8b7d27ac1878b04cc01211f379cef0853140
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-25 (Sat, 25 Apr 2026)
Changed paths:
M books/doc/cert.acl2
M books/doc/relnotes.lisp
M books/kestrel/c/language/static-semantics.lisp
M books/kestrel/fty/defresult.lisp
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-structural-operations.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
M books/kestrel/remora/grammar.abnf
R books/kestrel/remora/index-equivalence.lisp
A books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
A books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/static-semantics.lisp
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/yul/language/dynamic-semantics.lisp
M books/kestrel/yul/language/lexer.lisp
M books/kestrel/yul/language/parser.lisp
M books/kestrel/yul/language/static-safety-checking.lisp
M books/kestrel/yul/language/static-soundness.lisp
M books/kestrel/yul/transformations/dead-code-eliminator-execution.lisp
M books/kestrel/yul/transformations/dead-code-eliminator-safety.lisp
M books/kestrel/yul/transformations/no-function-definitions-dynamic.lisp
M books/kestrel/yul/transformations/renaming-variables-execution.lisp
M books/kestrel/yul/transformations/renaming-variables-safety.lisp
M books/projects/abnf/parsing-tools/defdefparse.lisp
M books/projects/abnf/parsing-tools/primitives-defresult.lisp
M books/projects/aleo/leo/early-version/definition/execution.lisp
M books/projects/aleo/leo/early-version/definition/flattening.lisp
M books/projects/aleo/leo/early-version/definition/input-execution.lisp
M books/projects/aleo/leo/early-version/definition/input-parser.lisp
M books/projects/aleo/leo/early-version/definition/input-syntax-abstraction.lisp
M books/projects/aleo/leo/early-version/definition/lexer.lisp
M books/projects/aleo/leo/early-version/definition/parser.lisp
M books/projects/aleo/leo/early-version/definition/program-execution.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/definition/type-checking.lisp
M books/projects/aleo/leo/early-version/definition/value-expressions.lisp
M books/projects/aleo/vm/language/early-version/parser.lisp
M books/projects/pfcs/lexer.lisp
M books/projects/pfcs/parser-interface.lisp
M books/projects/pfcs/parser.lisp
M books/projects/pfcs/proof-support.lisp
M books/projects/pfcs/semantics.lisp
M books/projects/pfcs/syntax-abstraction.lisp
M books/projects/pfcs/tokenizer.lisp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/quicklisp/bundle/software/cffi-20231021-git/grovel/asdf.lisp
M books/quicklisp/top.lisp
M books/quicklisp/update-libs.sh
M books/system/check-system-guards-raw.lsp
M books/system/check-system-guards.lisp
Log Message:
-----------
Merge.
Commit: 1d922d2ad23572a559e2135e90b4713c69d78b77
https://github.com/acl2/acl2/commit/1d922d2ad23572a559e2135e90b4713c69d78b77
Author: Alessandro Coglio <em...@alessandrocoglio.info>
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/build/lib/Certlib.pm
M books/doc/more-topics.lisp
M books/doc/practices.lisp
M books/doc/top.lisp
R books/kestrel/acl2-arrays/.sys/make-emp...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/make-into-ar...@useless-runes.lsp
A books/kestrel/acl2-arrays/.sys/new-a...@useless-runes.lsp
M books/kestrel/acl2-arrays/acl2-arrays.lisp
A books/kestrel/acl2-arrays/alist-to-array1-with-len.lisp
A books/kestrel/acl2-arrays/alist-to-array1.lisp
M books/kestrel/acl2-arrays/aref1.lisp
M books/kestrel/acl2-arrays/array-to-alist.lisp
M books/kestrel/acl2-arrays/compress1.lisp
R books/kestrel/acl2-arrays/make-empty-array.lisp
R books/kestrel/acl2-arrays/make-into-array-with-len.lisp
R books/kestrel/acl2-arrays/make-into-array.lisp
A books/kestrel/acl2-arrays/new-array1.lisp
M books/kestrel/acl2-arrays/top.lisp
M books/kestrel/acl2-arrays/typed-acl2-arrays-tests.lisp
M books/kestrel/acl2-arrays/typed-acl2-arrays.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/arithmetic-light/limit-expt.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/.sys/get-di...@useless-runes.lsp
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/bounded-dag-parent-arrayp.lisp
M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/concretize-with-contexts.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/contexts2.lisp
M books/kestrel/axe/crunch-dag.lisp
M books/kestrel/axe/crunch-dag2.lisp
M books/kestrel/axe/dag-array-builders.lisp
M books/kestrel/axe/dag-array-builders2.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-arrayp.lisp
M books/kestrel/axe/dag-size-fast.lisp
M books/kestrel/axe/dag-size-sparse-tests.lisp
M books/kestrel/axe/dag-size-sparse.lisp
M books/kestrel/axe/dag-size.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dagify.lisp
M books/kestrel/axe/dagify0.lisp
M books/kestrel/axe/def-dag-builder-theorems.lisp
M books/kestrel/axe/defthm-axe-basic-tests.lisp
M books/kestrel/axe/defthm-axe.lisp
M books/kestrel/axe/depth-array.lisp
M books/kestrel/axe/elim.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/evaluate-test-case.lisp
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/extract-dag-array.lisp
M books/kestrel/axe/find-probable-facts-simple.lisp
M books/kestrel/axe/find-probable-facts.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/jvm/lifter-utilities.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/rules-in-rule-lists-jvm.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/make-assumption-array.lisp
M books/kestrel/axe/make-dag-indices.lisp
M books/kestrel/axe/make-evaluator-tests.lisp
M books/kestrel/axe/make-evaluator.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/make-term-into-dag-array-basic.lisp
M books/kestrel/axe/make-term-into-dag-array-simple.lisp
M books/kestrel/axe/memoization.lisp
M books/kestrel/axe/merge-dag-into-dag-quick.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/node-replacement-array.lisp
M books/kestrel/axe/normalize-xors.lisp
A books/kestrel/axe/pre-stp-rules.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/prove-with-stp2.lisp
M books/kestrel/axe/prover-basic-tests.lisp
M books/kestrel/axe/prover-common.lisp
M books/kestrel/axe/prover-tests.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/rebuild-literals.lisp
M books/kestrel/axe/rebuild-nodes.lisp
M books/kestrel/axe/rebuild-nodes2.lisp
M books/kestrel/axe/register-and-wrap-clause-processor-simple.lisp
M books/kestrel/axe/remove-gaps.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/rewriter-alt.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-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/splitting.lisp
M books/kestrel/axe/substitute-vars2.lisp
M books/kestrel/axe/supporting-nodes.lisp
M books/kestrel/axe/supporting-vars.lisp
M books/kestrel/axe/sweep-and-merge-support.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/translation-array.lisp
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/wf-dagp.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/axe/x86/tester-rules-bv.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/built-ins/disable.lisp
M books/kestrel/bv/adder.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/bvplus.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/getbit-rules.lisp
M books/kestrel/bv/getbit.lisp
M books/kestrel/bv/intro.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/bv/trim-elim-rules-bv.lisp
M books/kestrel/c/language/decimal-0-to-octal-0.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/character-constants-c23.abnf
A 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/grammar/string-literals-c17.abnf
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/rename.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-gso.lisp
A books/kestrel/c/transformation/tests/split-gso/implicit-initer.c
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
A books/kestrel/c/transformation/tests/split-gso/unnamed-members.c
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/collect-idents.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
A books/kestrel/error-checking/ensure-function-known-measure.lisp
M books/kestrel/ethereum/semaphore/r1cs-proof-rules.lisp
M books/kestrel/executable-parsers/elf-tools.lisp
M books/kestrel/executable-parsers/mach-o-tools.lisp
A books/kestrel/executable-parsers/memory-regions.lisp
M books/kestrel/executable-parsers/parse-elf-file.lisp
M books/kestrel/executable-parsers/pe-tools.lisp
M books/kestrel/fty/deffold-map-doc.lisp
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp
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/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/java/aij/assumptions.lisp
M books/kestrel/java/aij/top.lisp
M books/kestrel/java/atj/aij-notions.lisp
M books/kestrel/java/atj/array-write-method-names.lisp
M books/kestrel/java/atj/atj.lisp
M books/kestrel/java/atj/code-generation.lisp
M books/kestrel/java/atj/common-code-generation.lisp
M books/kestrel/java/atj/deep-code-generation.lisp
M books/kestrel/java/atj/doc.lisp
M books/kestrel/java/atj/input-processing.lisp
M books/kestrel/java/atj/java-abstract-syntax.lisp
M books/kestrel/java/atj/java-input-types.lisp
M books/kestrel/java/atj/java-pretty-printer.lisp
M books/kestrel/java/atj/java-primitive-array-model.lisp
M books/kestrel/java/atj/java-primitive-arrays.lisp
M books/kestrel/java/atj/java-primitives.lisp
M books/kestrel/java/atj/java-syntax-operations.lisp
M books/kestrel/java/atj/library-extensions.lisp
M books/kestrel/java/atj/name-translation.lisp
M books/kestrel/java/atj/post-translation/cache-const-methods.lisp
M books/kestrel/java/atj/post-translation/fold-returns.lisp
M books/kestrel/java/atj/post-translation/lift-loop-tests.lisp
M books/kestrel/java/atj/post-translation/remove-array-write-calls.lisp
M books/kestrel/java/atj/post-translation/remove-continue.lisp
M books/kestrel/java/atj/post-translation/simplify-conds.lisp
M books/kestrel/java/atj/post-translation/tailrec-elimination.lisp
M books/kestrel/java/atj/post-translation/top.lisp
M books/kestrel/java/atj/pre-translation/array-analysis.lisp
M books/kestrel/java/atj/pre-translation/conjunctions.lisp
M books/kestrel/java/atj/pre-translation/disjunctions.lisp
M books/kestrel/java/atj/pre-translation/multiple-values.lisp
M books/kestrel/java/atj/pre-translation/no-aij-types-analysis.lisp
M books/kestrel/java/atj/pre-translation/remove-dead-if-branches.lisp
M books/kestrel/java/atj/pre-translation/remove-return-last.lisp
M books/kestrel/java/atj/pre-translation/top.lisp
M books/kestrel/java/atj/pre-translation/trivial-vars.lisp
M books/kestrel/java/atj/pre-translation/type-annotation.lisp
M books/kestrel/java/atj/pre-translation/unused-vars.lisp
M books/kestrel/java/atj/pre-translation/var-renaming.lisp
M books/kestrel/java/atj/pre-translation/var-reuse.lisp
M books/kestrel/java/atj/shallow-code-generation.lisp
M books/kestrel/java/atj/shallow-quoted-constant-generation.lisp
M books/kestrel/java/atj/test-structures.lisp
M books/kestrel/java/atj/tests/abnf.lisp
M books/kestrel/java/atj/tests/acl2-times.lisp
M books/kestrel/java/atj/tests/booleans.lisp
M books/kestrel/java/atj/tests/cache-const-methods.lisp
M books/kestrel/java/atj/tests/factorial.lisp
M books/kestrel/java/atj/tests/fibonacci.lisp
M books/kestrel/java/atj/tests/hard-error.lisp
M books/kestrel/java/atj/tests/multivalue.lisp
M books/kestrel/java/atj/tests/natives.lisp
M books/kestrel/java/atj/tests/no-aij-types.lisp
M books/kestrel/java/atj/tests/packages.lisp
M books/kestrel/java/atj/tests/primarrays.lisp
M books/kestrel/java/atj/tests/primitives.lisp
M books/kestrel/java/atj/top.lisp
M books/kestrel/java/atj/tutorial.lisp
M books/kestrel/java/atj/type-macros.lisp
M books/kestrel/java/atj/types-for-built-ins.lisp
M books/kestrel/java/atj/types-for-bv-fns.lisp
M books/kestrel/java/atj/types-for-ihs-fns.lisp
M books/kestrel/java/atj/types-for-list-fns.lisp
M books/kestrel/java/atj/types-for-natives.lisp
M books/kestrel/java/atj/types-for-std-fns.lisp
M books/kestrel/java/atj/types.lisp
M books/kestrel/java/language/binary-digits-validation.lisp
M books/kestrel/java/language/binary-integer-literals.lisp
M books/kestrel/java/language/boolean-literals-validation.lisp
M books/kestrel/java/language/boolean-literals.lisp
M books/kestrel/java/language/decimal-digits-validation.lisp
M books/kestrel/java/language/decimal-integer-literals.lisp
M books/kestrel/java/language/escape-sequences.lisp
M books/kestrel/java/language/floating-point-placeholders.lisp
M books/kestrel/java/language/floating-point-value-set-parameters.lisp
M books/kestrel/java/language/grammar.lisp
M books/kestrel/java/language/hexadecimal-digits-validation.lisp
M books/kestrel/java/language/hexadecimal-integer-literals.lisp
M books/kestrel/java/language/integer-literals.lisp
M books/kestrel/java/language/keywords-validation.lisp
M books/kestrel/java/language/literals.lisp
M books/kestrel/java/language/null-literal-validation.lisp
M books/kestrel/java/language/null-literal.lisp
M books/kestrel/java/language/octal-digits-validation.lisp
M books/kestrel/java/language/octal-integer-literals.lisp
M books/kestrel/java/language/optional-integer-type-suffix.lisp
M books/kestrel/java/language/package-names.lisp
M books/kestrel/java/language/pointers.lisp
M books/kestrel/java/language/primitive-conversions.lisp
M books/kestrel/java/language/primitive-function-macros.lisp
M books/kestrel/java/language/primitive-operations.lisp
M books/kestrel/java/language/primitive-types.lisp
M books/kestrel/java/language/primitive-values.lisp
M books/kestrel/java/language/reference-types.lisp
M books/kestrel/java/language/reference-values.lisp
M books/kestrel/java/language/semantics.lisp
M books/kestrel/java/language/syntax.lisp
M books/kestrel/java/language/top.lisp
M books/kestrel/java/language/types.lisp
M books/kestrel/java/language/unicode-characters.lisp
M books/kestrel/java/language/unicode-escapes.lisp
M books/kestrel/java/language/unicode-input-characters.lisp
M books/kestrel/java/language/values.lisp
M books/kestrel/java/portcullis.lisp
M books/kestrel/java/top.lisp
M books/kestrel/jvm/ads2.lisp
M books/kestrel/jvm/arrays.lisp
M books/kestrel/jvm/call-stacks.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/compile-file-if-needed-core.sh
M books/kestrel/jvm/frames.lisp
M books/kestrel/jvm/heap0.lisp
M books/kestrel/jvm/jvm-rules.lisp
M books/kestrel/jvm/operand-stacks.lisp
M books/kestrel/library-wrappers/my-make-flag-tests.lisp
M books/kestrel/lists-light/all-eql-dollar.lisp
M books/kestrel/lists-light/all-same-eql.lisp
M books/kestrel/lists-light/append-with-key.lisp
M books/kestrel/lists-light/compat.lisp
M books/kestrel/lists-light/evens-and-odds.lisp
M books/kestrel/lists-light/every-nth.lisp
M books/kestrel/lists-light/finalcdr.lisp
M books/kestrel/lists-light/find-index.lisp
M books/kestrel/lists-light/firstn.lisp
M books/kestrel/lists-light/group-rules.lisp
M books/kestrel/lists-light/group.lisp
M books/kestrel/lists-light/member-equal.lisp
M books/kestrel/lists-light/nth.lisp
M books/kestrel/lists-light/nthcdr.lisp
M books/kestrel/lists-light/prefixp.lisp
M books/kestrel/lists-light/rules2.lisp
M books/kestrel/lists-light/take2.lisp
M books/kestrel/lists-light/ungroup.lisp
M books/kestrel/lists-light/union-eql-tail.lisp
M books/kestrel/lists-light/update-subrange.lisp
M books/kestrel/lists-light/update-subrange2.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
R books/kestrel/memory/memory-regions.lisp
M books/kestrel/meta/rewriter0.lisp
M books/kestrel/meta/rewriter1.lisp
M books/kestrel/remora/abstract-syntax-constructors.lisp
A 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-structural-operations.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/cert.acl2
A books/kestrel/remora/character-literal-codes.lisp
A books/kestrel/remora/concrete-syntax-trees.lisp
A books/kestrel/remora/concrete-syntax.lisp
A books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/dynamic-environments.lisp
A books/kestrel/remora/dynamic-semantics.lisp
A books/kestrel/remora/dynamic-values.lisp
A 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
A books/kestrel/remora/identifier-syntax.lisp
A books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/package.lsp
A books/kestrel/remora/parse-directory-files.acl2
A books/kestrel/remora/parse-directory-files.lisp
A 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
A books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/static-semantics.lisp
A books/kestrel/remora/syntax-abstraction.lisp
A books/kestrel/remora/top.acl2
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/utilities/declares0.lisp
M books/kestrel/utilities/error-checking/top.lisp
A books/kestrel/utilities/flatten-ands-in-lit.lisp
M books/kestrel/utilities/legal-variablep.lisp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/package.lsp
M books/kestrel/x86/read-over-write-rules.lisp
M books/kestrel/x86/run-until-return.lisp
M books/kestrel/x86/run-until-return2.lisp
M books/kestrel/x86/support32.lisp
M books/projects/abnf/notation/semantics.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/cpp-top-level-parser.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/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
A books/system/report-timings.lsp
M books/xdoc/fancy/xdoc.js
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.
Commit: 21351df0b8efda36ca0b58447683326e9237e80e
https://github.com/acl2/acl2/commit/21351df0b8efda36ca0b58447683326e9237e80e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)
Changed paths:
M books/kestrel/c/syntax/reader.lisp
Log Message:
-----------
[C$] Add check to reader.
Excludes surrogate Unicode code points.
Commit: 200c77b20922cf18d4c2ee2f78589dde05efa744
https://github.com/acl2/acl2/commit/200c77b20922cf18d4c2ee2f78589dde05efa744
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)
Changed paths:
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/reader.lisp
M books/kestrel/c/syntax/unicode-characters.lisp
Log Message:
-----------
[C$] Tighten some types.
This replaces natural numbers with unicode characters in the character-position
pairs in the parser stobj and in the return of the reader.
Commit: 3836d9db5fb2517ff36be29bc12f3356cf8e10e9
https://github.com/acl2/acl2/commit/3836d9db5fb2517ff36be29bc12f3356cf8e10e9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/unicode-characters.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Tighten a fixtype.
Use the type of Unicode character codes for the code field of a `c-char` AST.
Commit: 2c871417f56bd0c1f383ca1dc2699c58285e42bd
https://github.com/acl2/acl2/commit/2c871417f56bd0c1f383ca1dc2699c58285e42bd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.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/unicode-characters.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Use a tighter fixtype.
Restrict the code field of a `s-char` AST to be a Unicode character code.
Commit: a72c20918812328c39c58213c57c684ab03d72d7
https://github.com/acl2/acl2/commit/a72c20918812328c39c58213c57c684ab03d72d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/language/implementation-environments/dialects.lisp
Log Message:
-----------
[C] Remove needless line break.
Commit: 1a35375fc224bdca59f48eeabd6b359937d67e87
https://github.com/acl2/acl2/commit/1a35375fc224bdca59f48eeabd6b359937d67e87
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
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
Log Message:
-----------
[C$] Start modularizing grammar of expressions.
Commit: d65889a58bc26bbe96526b7802e6e25aaa92e766
https://github.com/acl2/acl2/commit/d65889a58bc26bbe96526b7802e6e25aaa92e766
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/unicode-characters.lisp
Log Message:
-----------
[C$] Tighten a fixtype in ASTs.
Use Unicode character codes instead of natural numbers in `u-char`.
Commit: 087aa269225aceecd4812a2a1e8ea978a9e3bdc6
https://github.com/acl2/acl2/commit/087aa269225aceecd4812a2a1e8ea978a9e3bdc6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Tighten a fixtype in ASTs.
In `q-char` ASTs, use Unicode character codes instead of just natural numbers.
Commit: 21651361a09cd6e5f5d8560ffa610a57516ff358
https://github.com/acl2/acl2/commit/21651361a09cd6e5f5d8560ffa610a57516ff358
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
Log Message:
-----------
[C$] Tighten an AST fixtype.
Use Unicode character codes for the content of block comments, instead of just
natural numbers.
Commit: 7d9daa3a368ca0e71949f02754697a89a96b0fc0
https://github.com/acl2/acl2/commit/7d9daa3a368ca0e71949f02754697a89a96b0fc0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
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
Log Message:
-----------
[C$] Tighten a fixtype in ASTs.
Use Unicode character codes in line comments of preprocessor lexemes.
Commit: 0f3e3841f098b0edf0257451653e83f72554f669
https://github.com/acl2/acl2/commit/0f3e3841f098b0edf0257451653e83f72554f669
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Tighten an AST fixtype.
Commit: 869374490e853ef4671c18c7b03625ab9ddd996f
https://github.com/acl2/acl2/commit/869374490e853ef4671c18c7b03625ab9ddd996f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 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
M books/kestrel/axe/x86/tests/kestrel/assembly/add.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/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-options.lisp
M books/kestrel/c/syntax/preprocessor.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/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/x86/flags.lisp
Log Message:
-----------
Merge.
Commit: 37bb516ee484d7634a0e71590cc4a6b07e59a2de
https://github.com/acl2/acl2/commit/37bb516ee484d7634a0e71590cc4a6b07e59a2de
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/language/implementation-environments/dialects.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
Log Message:
-----------
Merge.
Commit: 93e710588700b1329c3859d33004c0f36de197b8
https://github.com/acl2/acl2/commit/93e710588700b1329c3859d33004c0f36de197b8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Fix doc.
Commit: 5435b91b3c6838d05265b85de2006588e77da113
https://github.com/acl2/acl2/commit/5435b91b3c6838d05265b85de2006588e77da113
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/extra-grammatical-restrictions.lisp
Log Message:
-----------
[Remora] Remove done 'todo'.
Commit: 4687da0d5121e41667a0a2afafc61126e8380eec
https://github.com/acl2/acl2/commit/4687da0d5121e41667a0a2afafc61126e8380eec
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/dynamic-values.lisp
Log Message:
-----------
[Remora] Add two result fixtypes.
Commit: f5bf9346991fdd60c36c8e5e75400d2819b0a539
https://github.com/acl2/acl2/commit/f5bf9346991fdd60c36c8e5e75400d2819b0a539
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Add evaluation of types.
Commit: 2bc473280507869ee7499f5b8c3090e1300617e4
https://github.com/acl2/acl2/commit/2bc473280507869ee7499f5b8c3090e1300617e4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/acl2-arrays/compress11.lisp
M books/kestrel/arithmetic-light/floor2.lisp
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/add-and-normalize-expr.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
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
M 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.
Commit: 573ce451aa9d06bfedd97f5253216e7c32e882bd
https://github.com/acl2/acl2/commit/573ce451aa9d06bfedd97f5253216e7c32e882bd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
Log Message:
-----------
[Remora] Reorder some code within a file.
Commit: d4674a5be002c1bac340919c953831d9792d820b
https://github.com/acl2/acl2/commit/d4674a5be002c1bac340919c953831d9792d820b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Add literal evaluation.
Commit: 4f6914331618ac4ea1aaaa1847155e5350290d7a
https://github.com/acl2/acl2/commit/4f6914331618ac4ea1aaaa1847155e5350290d7a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/grammar.abnf
Log Message:
-----------
[Remora] Add missing `%s` instances to grammar.
As discussed with Eric M. on Zulip.
Commit: b114c34de8d29a1259cc8b502cc337ec2af8252b
https://github.com/acl2/acl2/commit/b114c34de8d29a1259cc8b502cc337ec2af8252b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Extend type checking to string literals.
Commit: 86e68b4a88ca2ce6e0e4cebf2612a67b4c9da71f
https://github.com/acl2/acl2/commit/86e68b4a88ca2ce6e0e4cebf2612a67b4c9da71f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
Log Message:
-----------
[Remora] Extend some variable ops to programs.
Commit: 15907d889010f4bc46d0c1e4d5fa361865082c2f
https://github.com/acl2/acl2/commit/15907d889010f4bc46d0c1e4d5fa361865082c2f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/fty/fty-set.lisp
Log Message:
-----------
[FTY] More consistent line spacing.
Commit: ab882484e264d7f473081ef4eeaa982cdc388c40
https://github.com/acl2/acl2/commit/ab882484e264d7f473081ef4eeaa982cdc388c40
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
Log Message:
-----------
[Remora] Extend variable ops to expressions.
These are the predicates to check no capture of ispace variables.
Commit: 8a3a1039c8c42b9779cee077fa8e01959e839725
https://github.com/acl2/acl2/commit/8a3a1039c8c42b9779cee077fa8e01959e839725
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/language/implementation-environments/dialects.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
Log Message:
-----------
Merge.
Commit: 2a85f0a4188b5b5163518c0c20a045f1443b03b6
https://github.com/acl2/acl2/commit/2a85f0a4188b5b5163518c0c20a045f1443b03b6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
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/structure-operations.lisp
M books/kestrel/fty/fty-set.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/f347790b179c...2a85f0a4188b
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 6a8c8bf385281795e4556ef1569dc2b0c92d63db
https://github.com/acl2/acl2/commit/6a8c8bf385281795e4556ef1569dc2b0c92d63db
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-18 (Sat, 18 Apr 2026)
Changed paths:
M books/kestrel/c/examples/strcpy-safe.lisp
Log Message:
-----------
[C strcpy] Fix doc comment.
Commit: 69d92d9634904bab8b6f88b700e0b568f65aefeb
https://github.com/acl2/acl2/commit/69d92d9634904bab8b6f88b700e0b568f65aefeb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-18 (Sat, 18 Apr 2026)
Changed paths:
M books/kestrel/c/language/structure-operations.lisp
Log Message:
-----------
[C] Add a theorem.
Commit: 1a047a6fd55e184ef24b529ec77ef07dbdbca002
https://github.com/acl2/acl2/commit/1a047a6fd55e184ef24b529ec77ef07dbdbca002
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-18 (Sat, 18 Apr 2026)
Changed paths:
M books/kestrel/c/language/array-operations.lisp
Log Message:
-----------
[C] Add two theorems.
Commit: 1790b3c7ce327ecc57b8a6973ee7a74ea26f879e
https://github.com/acl2/acl2/commit/1790b3c7ce327ecc57b8a6973ee7a74ea26f879e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-18 (Sat, 18 Apr 2026)
Changed paths:
M books/kestrel/c/language/computation-states.lisp
Log Message:
-----------
[C] Add a theorem.
Commit: 219450d9609b437a45bd9eead6ade69672f9ee5b
https://github.com/acl2/acl2/commit/219450d9609b437a45bd9eead6ade69672f9ee5b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-20 (Mon, 20 Apr 2026)
Changed paths:
M axioms.lisp
M basis-a.lisp
M books/demos/geneqv-test-log.txt
M books/kestrel/acl2pl/package.lsp
M books/kestrel/java/language/primitive-operations.lisp
M books/kestrel/remora/parser.lisp
A books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/top.lisp
M books/misc/check-acl2-exports.lisp
M books/std/alists/alist-keys.lisp
M books/system/defstobj.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/stobj-help.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M other-events.lisp
Log Message:
-----------
Merge.
Commit: 1255cfa38de468c37024fc0ed2614b0c8c57ba4b
https://github.com/acl2/acl2/commit/1255cfa38de468c37024fc0ed2614b0c8c57ba4b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-22 (Wed, 22 Apr 2026)
Changed paths:
M books/demos/geneqv-test-log.txt
M books/kestrel/axe/arm/README.md
M books/kestrel/axe/jvm/axe-syntax-functions-jvm.lisp
M books/kestrel/axe/jvm/lifter-utilities.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/output-indicators.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/jvm/tester.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
A books/kestrel/axe/r1cs/README.md
M books/kestrel/axe/risc-v/README.md
M books/kestrel/axe/x86/README.md
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/floats/ieee-floats.lisp
M books/kestrel/floats/round.lisp
M books/kestrel/jvm/acl2-customization.lsp
M books/kestrel/jvm/call-stacks.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/class-tables.lisp
M books/kestrel/jvm/classes.lisp
M books/kestrel/jvm/control-flow.lisp
M books/kestrel/jvm/fields.lisp
M books/kestrel/jvm/floats.lisp
M books/kestrel/jvm/floats2.lisp
M books/kestrel/jvm/frames.lisp
M books/kestrel/jvm/heap.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.lisp
M books/kestrel/jvm/method-indicators.lisp
M books/kestrel/jvm/methods.lisp
M books/kestrel/jvm/states.lisp
M books/kestrel/jvm/symbolic-execution.lisp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/utils/segmentation-structures.lisp
M books/projects/x86isa/utils/structures.lisp
M books/projects/x86isa/utils/utilities.lisp
M books/system/apply/apply-prim.lisp
M boot-strap-pass-2-a.lisp
M induct.lisp
M other-events.lisp
Log Message:
-----------
Merge.
Commit: 438d3f94f35149061f1870bbebb46f25dc27231c
https://github.com/acl2/acl2/commit/438d3f94f35149061f1870bbebb46f25dc27231c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-22 (Wed, 22 Apr 2026)
Changed paths:
A books/kestrel/c/examples/strcpy-safe-induction-support.lisp
Log Message:
-----------
[C examples] Add some tentative generic utilities.
Commit: d0ab8b7d27ac1878b04cc01211f379cef0853140
https://github.com/acl2/acl2/commit/d0ab8b7d27ac1878b04cc01211f379cef0853140
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-04-25 (Sat, 25 Apr 2026)
Changed paths:
M books/doc/cert.acl2
M books/doc/relnotes.lisp
M books/kestrel/c/language/static-semantics.lisp
M books/kestrel/fty/defresult.lisp
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-structural-operations.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
M books/kestrel/remora/grammar.abnf
R books/kestrel/remora/index-equivalence.lisp
A books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
A books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/static-semantics.lisp
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/yul/language/dynamic-semantics.lisp
M books/kestrel/yul/language/lexer.lisp
M books/kestrel/yul/language/parser.lisp
M books/kestrel/yul/language/static-safety-checking.lisp
M books/kestrel/yul/language/static-soundness.lisp
M books/kestrel/yul/transformations/dead-code-eliminator-execution.lisp
M books/kestrel/yul/transformations/dead-code-eliminator-safety.lisp
M books/kestrel/yul/transformations/no-function-definitions-dynamic.lisp
M books/kestrel/yul/transformations/renaming-variables-execution.lisp
M books/kestrel/yul/transformations/renaming-variables-safety.lisp
M books/projects/abnf/parsing-tools/defdefparse.lisp
M books/projects/abnf/parsing-tools/primitives-defresult.lisp
M books/projects/aleo/leo/early-version/definition/execution.lisp
M books/projects/aleo/leo/early-version/definition/flattening.lisp
M books/projects/aleo/leo/early-version/definition/input-execution.lisp
M books/projects/aleo/leo/early-version/definition/input-parser.lisp
M books/projects/aleo/leo/early-version/definition/input-syntax-abstraction.lisp
M books/projects/aleo/leo/early-version/definition/lexer.lisp
M books/projects/aleo/leo/early-version/definition/parser.lisp
M books/projects/aleo/leo/early-version/definition/program-execution.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/definition/type-checking.lisp
M books/projects/aleo/leo/early-version/definition/value-expressions.lisp
M books/projects/aleo/vm/language/early-version/parser.lisp
M books/projects/pfcs/lexer.lisp
M books/projects/pfcs/parser-interface.lisp
M books/projects/pfcs/parser.lisp
M books/projects/pfcs/proof-support.lisp
M books/projects/pfcs/semantics.lisp
M books/projects/pfcs/syntax-abstraction.lisp
M books/projects/pfcs/tokenizer.lisp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/quicklisp/bundle/software/cffi-20231021-git/grovel/asdf.lisp
M books/quicklisp/top.lisp
M books/quicklisp/update-libs.sh
M books/system/check-system-guards-raw.lsp
M books/system/check-system-guards.lisp
Log Message:
-----------
Merge.
Commit: 1d922d2ad23572a559e2135e90b4713c69d78b77
https://github.com/acl2/acl2/commit/1d922d2ad23572a559e2135e90b4713c69d78b77
Author: Alessandro Coglio <em...@alessandrocoglio.info>
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/build/lib/Certlib.pm
M books/doc/more-topics.lisp
M books/doc/practices.lisp
M books/doc/top.lisp
R books/kestrel/acl2-arrays/.sys/make-emp...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/make-into-ar...@useless-runes.lsp
A books/kestrel/acl2-arrays/.sys/new-a...@useless-runes.lsp
M books/kestrel/acl2-arrays/acl2-arrays.lisp
A books/kestrel/acl2-arrays/alist-to-array1-with-len.lisp
A books/kestrel/acl2-arrays/alist-to-array1.lisp
M books/kestrel/acl2-arrays/aref1.lisp
M books/kestrel/acl2-arrays/array-to-alist.lisp
M books/kestrel/acl2-arrays/compress1.lisp
R books/kestrel/acl2-arrays/make-empty-array.lisp
R books/kestrel/acl2-arrays/make-into-array-with-len.lisp
R books/kestrel/acl2-arrays/make-into-array.lisp
A books/kestrel/acl2-arrays/new-array1.lisp
M books/kestrel/acl2-arrays/top.lisp
M books/kestrel/acl2-arrays/typed-acl2-arrays-tests.lisp
M books/kestrel/acl2-arrays/typed-acl2-arrays.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/arithmetic-light/limit-expt.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/.sys/get-di...@useless-runes.lsp
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/bounded-dag-parent-arrayp.lisp
M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/concretize-with-contexts.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/contexts2.lisp
M books/kestrel/axe/crunch-dag.lisp
M books/kestrel/axe/crunch-dag2.lisp
M books/kestrel/axe/dag-array-builders.lisp
M books/kestrel/axe/dag-array-builders2.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-arrayp.lisp
M books/kestrel/axe/dag-size-fast.lisp
M books/kestrel/axe/dag-size-sparse-tests.lisp
M books/kestrel/axe/dag-size-sparse.lisp
M books/kestrel/axe/dag-size.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dagify.lisp
M books/kestrel/axe/dagify0.lisp
M books/kestrel/axe/def-dag-builder-theorems.lisp
M books/kestrel/axe/defthm-axe-basic-tests.lisp
M books/kestrel/axe/defthm-axe.lisp
M books/kestrel/axe/depth-array.lisp
M books/kestrel/axe/elim.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/evaluate-test-case.lisp
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/extract-dag-array.lisp
M books/kestrel/axe/find-probable-facts-simple.lisp
M books/kestrel/axe/find-probable-facts.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/jvm/lifter-utilities.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/rules-in-rule-lists-jvm.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/make-assumption-array.lisp
M books/kestrel/axe/make-dag-indices.lisp
M books/kestrel/axe/make-evaluator-tests.lisp
M books/kestrel/axe/make-evaluator.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/make-term-into-dag-array-basic.lisp
M books/kestrel/axe/make-term-into-dag-array-simple.lisp
M books/kestrel/axe/memoization.lisp
M books/kestrel/axe/merge-dag-into-dag-quick.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/node-replacement-array.lisp
M books/kestrel/axe/normalize-xors.lisp
A books/kestrel/axe/pre-stp-rules.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/prove-with-stp2.lisp
M books/kestrel/axe/prover-basic-tests.lisp
M books/kestrel/axe/prover-common.lisp
M books/kestrel/axe/prover-tests.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/rebuild-literals.lisp
M books/kestrel/axe/rebuild-nodes.lisp
M books/kestrel/axe/rebuild-nodes2.lisp
M books/kestrel/axe/register-and-wrap-clause-processor-simple.lisp
M books/kestrel/axe/remove-gaps.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/rewriter-alt.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-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/splitting.lisp
M books/kestrel/axe/substitute-vars2.lisp
M books/kestrel/axe/supporting-nodes.lisp
M books/kestrel/axe/supporting-vars.lisp
M books/kestrel/axe/sweep-and-merge-support.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/translation-array.lisp
M books/kestrel/axe/trim-intro-rules-axe.lisp
M books/kestrel/axe/wf-dagp.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/axe/x86/tester-rules-bv.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/built-ins/disable.lisp
M books/kestrel/bv/adder.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/bvplus.lisp
M books/kestrel/bv/bvsx.lisp
M books/kestrel/bv/getbit-rules.lisp
M books/kestrel/bv/getbit.lisp
M books/kestrel/bv/intro.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/bv/trim-elim-rules-bv.lisp
M books/kestrel/c/language/decimal-0-to-octal-0.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/character-constants-c23.abnf
A 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/grammar/string-literals-c17.abnf
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/rename.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-gso.lisp
A books/kestrel/c/transformation/tests/split-gso/implicit-initer.c
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
A books/kestrel/c/transformation/tests/split-gso/unnamed-members.c
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/collect-idents.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
A books/kestrel/error-checking/ensure-function-known-measure.lisp
M books/kestrel/ethereum/semaphore/r1cs-proof-rules.lisp
M books/kestrel/executable-parsers/elf-tools.lisp
M books/kestrel/executable-parsers/mach-o-tools.lisp
A books/kestrel/executable-parsers/memory-regions.lisp
M books/kestrel/executable-parsers/parse-elf-file.lisp
M books/kestrel/executable-parsers/pe-tools.lisp
M books/kestrel/fty/deffold-map-doc.lisp
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp
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/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/java/aij/assumptions.lisp
M books/kestrel/java/aij/top.lisp
M books/kestrel/java/atj/aij-notions.lisp
M books/kestrel/java/atj/array-write-method-names.lisp
M books/kestrel/java/atj/atj.lisp
M books/kestrel/java/atj/code-generation.lisp
M books/kestrel/java/atj/common-code-generation.lisp
M books/kestrel/java/atj/deep-code-generation.lisp
M books/kestrel/java/atj/doc.lisp
M books/kestrel/java/atj/input-processing.lisp
M books/kestrel/java/atj/java-abstract-syntax.lisp
M books/kestrel/java/atj/java-input-types.lisp
M books/kestrel/java/atj/java-pretty-printer.lisp
M books/kestrel/java/atj/java-primitive-array-model.lisp
M books/kestrel/java/atj/java-primitive-arrays.lisp
M books/kestrel/java/atj/java-primitives.lisp
M books/kestrel/java/atj/java-syntax-operations.lisp
M books/kestrel/java/atj/library-extensions.lisp
M books/kestrel/java/atj/name-translation.lisp
M books/kestrel/java/atj/post-translation/cache-const-methods.lisp
M books/kestrel/java/atj/post-translation/fold-returns.lisp
M books/kestrel/java/atj/post-translation/lift-loop-tests.lisp
M books/kestrel/java/atj/post-translation/remove-array-write-calls.lisp
M books/kestrel/java/atj/post-translation/remove-continue.lisp
M books/kestrel/java/atj/post-translation/simplify-conds.lisp
M books/kestrel/java/atj/post-translation/tailrec-elimination.lisp
M books/kestrel/java/atj/post-translation/top.lisp
M books/kestrel/java/atj/pre-translation/array-analysis.lisp
M books/kestrel/java/atj/pre-translation/conjunctions.lisp
M books/kestrel/java/atj/pre-translation/disjunctions.lisp
M books/kestrel/java/atj/pre-translation/multiple-values.lisp
M books/kestrel/java/atj/pre-translation/no-aij-types-analysis.lisp
M books/kestrel/java/atj/pre-translation/remove-dead-if-branches.lisp
M books/kestrel/java/atj/pre-translation/remove-return-last.lisp
M books/kestrel/java/atj/pre-translation/top.lisp
M books/kestrel/java/atj/pre-translation/trivial-vars.lisp
M books/kestrel/java/atj/pre-translation/type-annotation.lisp
M books/kestrel/java/atj/pre-translation/unused-vars.lisp
M books/kestrel/java/atj/pre-translation/var-renaming.lisp
M books/kestrel/java/atj/pre-translation/var-reuse.lisp
M books/kestrel/java/atj/shallow-code-generation.lisp
M books/kestrel/java/atj/shallow-quoted-constant-generation.lisp
M books/kestrel/java/atj/test-structures.lisp
M books/kestrel/java/atj/tests/abnf.lisp
M books/kestrel/java/atj/tests/acl2-times.lisp
M books/kestrel/java/atj/tests/booleans.lisp
M books/kestrel/java/atj/tests/cache-const-methods.lisp
M books/kestrel/java/atj/tests/factorial.lisp
M books/kestrel/java/atj/tests/fibonacci.lisp
M books/kestrel/java/atj/tests/hard-error.lisp
M books/kestrel/java/atj/tests/multivalue.lisp
M books/kestrel/java/atj/tests/natives.lisp
M books/kestrel/java/atj/tests/no-aij-types.lisp
M books/kestrel/java/atj/tests/packages.lisp
M books/kestrel/java/atj/tests/primarrays.lisp
M books/kestrel/java/atj/tests/primitives.lisp
M books/kestrel/java/atj/top.lisp
M books/kestrel/java/atj/tutorial.lisp
M books/kestrel/java/atj/type-macros.lisp
M books/kestrel/java/atj/types-for-built-ins.lisp
M books/kestrel/java/atj/types-for-bv-fns.lisp
M books/kestrel/java/atj/types-for-ihs-fns.lisp
M books/kestrel/java/atj/types-for-list-fns.lisp
M books/kestrel/java/atj/types-for-natives.lisp
M books/kestrel/java/atj/types-for-std-fns.lisp
M books/kestrel/java/atj/types.lisp
M books/kestrel/java/language/binary-digits-validation.lisp
M books/kestrel/java/language/binary-integer-literals.lisp
M books/kestrel/java/language/boolean-literals-validation.lisp
M books/kestrel/java/language/boolean-literals.lisp
M books/kestrel/java/language/decimal-digits-validation.lisp
M books/kestrel/java/language/decimal-integer-literals.lisp
M books/kestrel/java/language/escape-sequences.lisp
M books/kestrel/java/language/floating-point-placeholders.lisp
M books/kestrel/java/language/floating-point-value-set-parameters.lisp
M books/kestrel/java/language/grammar.lisp
M books/kestrel/java/language/hexadecimal-digits-validation.lisp
M books/kestrel/java/language/hexadecimal-integer-literals.lisp
M books/kestrel/java/language/integer-literals.lisp
M books/kestrel/java/language/keywords-validation.lisp
M books/kestrel/java/language/literals.lisp
M books/kestrel/java/language/null-literal-validation.lisp
M books/kestrel/java/language/null-literal.lisp
M books/kestrel/java/language/octal-digits-validation.lisp
M books/kestrel/java/language/octal-integer-literals.lisp
M books/kestrel/java/language/optional-integer-type-suffix.lisp
M books/kestrel/java/language/package-names.lisp
M books/kestrel/java/language/pointers.lisp
M books/kestrel/java/language/primitive-conversions.lisp
M books/kestrel/java/language/primitive-function-macros.lisp
M books/kestrel/java/language/primitive-operations.lisp
M books/kestrel/java/language/primitive-types.lisp
M books/kestrel/java/language/primitive-values.lisp
M books/kestrel/java/language/reference-types.lisp
M books/kestrel/java/language/reference-values.lisp
M books/kestrel/java/language/semantics.lisp
M books/kestrel/java/language/syntax.lisp
M books/kestrel/java/language/top.lisp
M books/kestrel/java/language/types.lisp
M books/kestrel/java/language/unicode-characters.lisp
M books/kestrel/java/language/unicode-escapes.lisp
M books/kestrel/java/language/unicode-input-characters.lisp
M books/kestrel/java/language/values.lisp
M books/kestrel/java/portcullis.lisp
M books/kestrel/java/top.lisp
M books/kestrel/jvm/ads2.lisp
M books/kestrel/jvm/arrays.lisp
M books/kestrel/jvm/call-stacks.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/compile-file-if-needed-core.sh
M books/kestrel/jvm/frames.lisp
M books/kestrel/jvm/heap0.lisp
M books/kestrel/jvm/jvm-rules.lisp
M books/kestrel/jvm/operand-stacks.lisp
M books/kestrel/library-wrappers/my-make-flag-tests.lisp
M books/kestrel/lists-light/all-eql-dollar.lisp
M books/kestrel/lists-light/all-same-eql.lisp
M books/kestrel/lists-light/append-with-key.lisp
M books/kestrel/lists-light/compat.lisp
M books/kestrel/lists-light/evens-and-odds.lisp
M books/kestrel/lists-light/every-nth.lisp
M books/kestrel/lists-light/finalcdr.lisp
M books/kestrel/lists-light/find-index.lisp
M books/kestrel/lists-light/firstn.lisp
M books/kestrel/lists-light/group-rules.lisp
M books/kestrel/lists-light/group.lisp
M books/kestrel/lists-light/member-equal.lisp
M books/kestrel/lists-light/nth.lisp
M books/kestrel/lists-light/nthcdr.lisp
M books/kestrel/lists-light/prefixp.lisp
M books/kestrel/lists-light/rules2.lisp
M books/kestrel/lists-light/take2.lisp
M books/kestrel/lists-light/ungroup.lisp
M books/kestrel/lists-light/union-eql-tail.lisp
M books/kestrel/lists-light/update-subrange.lisp
M books/kestrel/lists-light/update-subrange2.lisp
M books/kestrel/memory/make-memory-region-machinery.lisp
R books/kestrel/memory/memory-regions.lisp
M books/kestrel/meta/rewriter0.lisp
M books/kestrel/meta/rewriter1.lisp
M books/kestrel/remora/abstract-syntax-constructors.lisp
A 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-structural-operations.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/cert.acl2
A books/kestrel/remora/character-literal-codes.lisp
A books/kestrel/remora/concrete-syntax-trees.lisp
A books/kestrel/remora/concrete-syntax.lisp
A books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/dynamic-environments.lisp
A books/kestrel/remora/dynamic-semantics.lisp
A books/kestrel/remora/dynamic-values.lisp
A 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
A books/kestrel/remora/identifier-syntax.lisp
A books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/package.lsp
A books/kestrel/remora/parse-directory-files.acl2
A books/kestrel/remora/parse-directory-files.lisp
A 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
A books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/static-semantics.lisp
A books/kestrel/remora/syntax-abstraction.lisp
A books/kestrel/remora/top.acl2
M books/kestrel/remora/top.lisp
M books/kestrel/remora/type-checking.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/kestrel/utilities/declares0.lisp
M books/kestrel/utilities/error-checking/top.lisp
A books/kestrel/utilities/flatten-ands-in-lit.lisp
M books/kestrel/utilities/legal-variablep.lisp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/package.lsp
M books/kestrel/x86/read-over-write-rules.lisp
M books/kestrel/x86/run-until-return.lisp
M books/kestrel/x86/run-until-return2.lisp
M books/kestrel/x86/support32.lisp
M books/projects/abnf/notation/semantics.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/cpp-top-level-parser.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/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
A books/system/report-timings.lsp
M books/xdoc/fancy/xdoc.js
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.
Commit: 21351df0b8efda36ca0b58447683326e9237e80e
https://github.com/acl2/acl2/commit/21351df0b8efda36ca0b58447683326e9237e80e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)
Changed paths:
M books/kestrel/c/syntax/reader.lisp
Log Message:
-----------
[C$] Add check to reader.
Excludes surrogate Unicode code points.
Commit: 200c77b20922cf18d4c2ee2f78589dde05efa744
https://github.com/acl2/acl2/commit/200c77b20922cf18d4c2ee2f78589dde05efa744
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)
Changed paths:
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/reader.lisp
M books/kestrel/c/syntax/unicode-characters.lisp
Log Message:
-----------
[C$] Tighten some types.
This replaces natural numbers with unicode characters in the character-position
pairs in the parser stobj and in the return of the reader.
Commit: 3836d9db5fb2517ff36be29bc12f3356cf8e10e9
https://github.com/acl2/acl2/commit/3836d9db5fb2517ff36be29bc12f3356cf8e10e9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/syntax/unicode-characters.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Tighten a fixtype.
Use the type of Unicode character codes for the code field of a `c-char` AST.
Commit: 2c871417f56bd0c1f383ca1dc2699c58285e42bd
https://github.com/acl2/acl2/commit/2c871417f56bd0c1f383ca1dc2699c58285e42bd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.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/unicode-characters.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Use a tighter fixtype.
Restrict the code field of a `s-char` AST to be a Unicode character code.
Commit: a72c20918812328c39c58213c57c684ab03d72d7
https://github.com/acl2/acl2/commit/a72c20918812328c39c58213c57c684ab03d72d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/language/implementation-environments/dialects.lisp
Log Message:
-----------
[C] Remove needless line break.
Commit: 1a35375fc224bdca59f48eeabd6b359937d67e87
https://github.com/acl2/acl2/commit/1a35375fc224bdca59f48eeabd6b359937d67e87
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
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
Log Message:
-----------
[C$] Start modularizing grammar of expressions.
Commit: d65889a58bc26bbe96526b7802e6e25aaa92e766
https://github.com/acl2/acl2/commit/d65889a58bc26bbe96526b7802e6e25aaa92e766
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/unicode-characters.lisp
Log Message:
-----------
[C$] Tighten a fixtype in ASTs.
Use Unicode character codes instead of natural numbers in `u-char`.
Commit: 087aa269225aceecd4812a2a1e8ea978a9e3bdc6
https://github.com/acl2/acl2/commit/087aa269225aceecd4812a2a1e8ea978a9e3bdc6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Tighten a fixtype in ASTs.
In `q-char` ASTs, use Unicode character codes instead of just natural numbers.
Commit: 21651361a09cd6e5f5d8560ffa610a57516ff358
https://github.com/acl2/acl2/commit/21651361a09cd6e5f5d8560ffa610a57516ff358
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
Log Message:
-----------
[C$] Tighten an AST fixtype.
Use Unicode character codes for the content of block comments, instead of just
natural numbers.
Commit: 7d9daa3a368ca0e71949f02754697a89a96b0fc0
https://github.com/acl2/acl2/commit/7d9daa3a368ca0e71949f02754697a89a96b0fc0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
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
Log Message:
-----------
[C$] Tighten a fixtype in ASTs.
Use Unicode character codes in line comments of preprocessor lexemes.
Commit: 0f3e3841f098b0edf0257451653e83f72554f669
https://github.com/acl2/acl2/commit/0f3e3841f098b0edf0257451653e83f72554f669
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/printer.lisp
Log Message:
-----------
[C$] Tighten an AST fixtype.
Commit: 869374490e853ef4671c18c7b03625ab9ddd996f
https://github.com/acl2/acl2/commit/869374490e853ef4671c18c7b03625ab9ddd996f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 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
M books/kestrel/axe/x86/tests/kestrel/assembly/add.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/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-options.lisp
M books/kestrel/c/syntax/preprocessor.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/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/x86/flags.lisp
Log Message:
-----------
Merge.
Commit: 37bb516ee484d7634a0e71590cc4a6b07e59a2de
https://github.com/acl2/acl2/commit/37bb516ee484d7634a0e71590cc4a6b07e59a2de
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/language/implementation-environments/dialects.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
Log Message:
-----------
Merge.
Commit: 93e710588700b1329c3859d33004c0f36de197b8
https://github.com/acl2/acl2/commit/93e710588700b1329c3859d33004c0f36de197b8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Fix doc.
Commit: 5435b91b3c6838d05265b85de2006588e77da113
https://github.com/acl2/acl2/commit/5435b91b3c6838d05265b85de2006588e77da113
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/extra-grammatical-restrictions.lisp
Log Message:
-----------
[Remora] Remove done 'todo'.
Commit: 4687da0d5121e41667a0a2afafc61126e8380eec
https://github.com/acl2/acl2/commit/4687da0d5121e41667a0a2afafc61126e8380eec
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/dynamic-values.lisp
Log Message:
-----------
[Remora] Add two result fixtypes.
Commit: f5bf9346991fdd60c36c8e5e75400d2819b0a539
https://github.com/acl2/acl2/commit/f5bf9346991fdd60c36c8e5e75400d2819b0a539
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Add evaluation of types.
Commit: 2bc473280507869ee7499f5b8c3090e1300617e4
https://github.com/acl2/acl2/commit/2bc473280507869ee7499f5b8c3090e1300617e4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/acl2-arrays/compress11.lisp
M books/kestrel/arithmetic-light/floor2.lisp
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/add-and-normalize-expr.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
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
M 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.
Commit: 573ce451aa9d06bfedd97f5253216e7c32e882bd
https://github.com/acl2/acl2/commit/573ce451aa9d06bfedd97f5253216e7c32e882bd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-trees.lisp
Log Message:
-----------
[Remora] Reorder some code within a file.
Commit: d4674a5be002c1bac340919c953831d9792d820b
https://github.com/acl2/acl2/commit/d4674a5be002c1bac340919c953831d9792d820b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/evaluation.lisp
Log Message:
-----------
[Remora] Add literal evaluation.
Commit: 4f6914331618ac4ea1aaaa1847155e5350290d7a
https://github.com/acl2/acl2/commit/4f6914331618ac4ea1aaaa1847155e5350290d7a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/grammar.abnf
Log Message:
-----------
[Remora] Add missing `%s` instances to grammar.
As discussed with Eric M. on Zulip.
Commit: b114c34de8d29a1259cc8b502cc337ec2af8252b
https://github.com/acl2/acl2/commit/b114c34de8d29a1259cc8b502cc337ec2af8252b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/type-checking.lisp
Log Message:
-----------
[Remora] Extend type checking to string literals.
Commit: 86e68b4a88ca2ce6e0e4cebf2612a67b4c9da71f
https://github.com/acl2/acl2/commit/86e68b4a88ca2ce6e0e4cebf2612a67b4c9da71f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
Log Message:
-----------
[Remora] Extend some variable ops to programs.
Commit: 15907d889010f4bc46d0c1e4d5fa361865082c2f
https://github.com/acl2/acl2/commit/15907d889010f4bc46d0c1e4d5fa361865082c2f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/fty/fty-set.lisp
Log Message:
-----------
[FTY] More consistent line spacing.
Commit: ab882484e264d7f473081ef4eeaa982cdc388c40
https://github.com/acl2/acl2/commit/ab882484e264d7f473081ef4eeaa982cdc388c40
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
Log Message:
-----------
[Remora] Extend variable ops to expressions.
These are the predicates to check no capture of ispace variables.
Commit: 8a3a1039c8c42b9779cee077fa8e01959e839725
https://github.com/acl2/acl2/commit/8a3a1039c8c42b9779cee077fa8e01959e839725
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
M books/kestrel/c/language/implementation-environments/dialects.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
Log Message:
-----------
Merge.
Commit: 2a85f0a4188b5b5163518c0c20a045f1443b03b6
https://github.com/acl2/acl2/commit/2a85f0a4188b5b5163518c0c20a045f1443b03b6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-27 (Wed, 27 May 2026)
Changed paths:
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/structure-operations.lisp
M books/kestrel/fty/fty-set.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/f347790b179c...2a85f0a4188b
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
May 28, 2026, 3:42:18 AM (4 days ago) May 28
to acl2-...@googlegroups.com
Alessandro Coglio
May 28, 2026, 3:42:39 AM (4 days ago) May 28
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
May 29, 2026, 2:42:13 AM (3 days ago) May 29
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: 05b5302cdb796d854e63fe7153382ba666541b13
https://github.com/acl2/acl2/commit/05b5302cdb796d854e63fe7153382ba666541b13
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/memory.lisp
Log Message:
-----------
[arm] Improve rule.
Commit: 4cc35df39e2905ccb2f38ba18030dafd1b63d18e
https://github.com/acl2/acl2/commit/4cc35df39e2905ccb2f38ba18030dafd1b63d18e
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
Log Message:
-----------
[axe/arm] Add UXTH and recharacterize flags for sub-immediate.
Commit: 61db1b98b70ecc26af21bd03836eede3f1ea1671
https://github.com/acl2/acl2/commit/61db1b98b70ecc26af21bd03836eede3f1ea1671
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/def-inst.lisp
M books/kestrel/arm/instructions.lisp
Log Message:
-----------
[arm] Start fleshing out unconditional instructions.
Commit: ffbd9d00a7a974dc9603790edbcda313eff888af
https://github.com/acl2/acl2/commit/ffbd9d00a7a974dc9603790edbcda313eff888af
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
Log Message:
-----------
[arm] Add REV16 instruction.
Commit: 6eec8bdd1c24cecd97e7e0794e02bce8c283c7f8
https://github.com/acl2/acl2/commit/6eec8bdd1c24cecd97e7e0794e02bce8c283c7f8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/def-inst.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/axe/arm/rule-lists.lisp
Log Message:
-----------
[axe/arm] Add support for one kind of unconditional instruction.
Commit: 999d78daf5df4c961e607b367aba0494aaf681bd
https://github.com/acl2/acl2/commit/999d78daf5df4c961e607b367aba0494aaf681bd
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/step.lisp
M books/kestrel/arm/tests/simple.lisp
M books/kestrel/axe/arm/run-until-return.lisp
Log Message:
-----------
[axe/arm] Improve checking of processor mode.
Now we get an error if not in ARM mode.
Commit: 371deba36d974d003b94da32ea239986a6391ed0
https://github.com/acl2/acl2/commit/371deba36d974d003b94da32ea239986a6391ed0
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
Log Message:
-----------
[arm] Add more instructions.
REV, REVSH, and ROR.
Commit: f3de74de64d3bc075ab37b4bc0c6a7acdde97050
https://github.com/acl2/acl2/commit/f3de74de64d3bc075ab37b4bc0c6a7acdde97050
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/apt/doc.lisp
Log Message:
-----------
[apt] Include remove-nesting in doc.
Commit: 689bb969882c79e18435b6aa04f02f05c1c9505e
https://github.com/acl2/acl2/commit/689bb969882c79e18435b6aa04f02f05c1c9505e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
[C$] Add missing ordered subtopic.
Commit: 2d60074541c778f719c1b64a3846f2b06eb57d44
https://github.com/acl2/acl2/commit/2d60074541c778f719c1b64a3846f2b06eb57d44
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
A books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
[C$] Move some code to a new file.
Commit: 12d46d37c40444cc40d7f1d9aed7175e768de5d6
https://github.com/acl2/acl2/commit/12d46d37c40444cc40d7f1d9aed7175e768de5d6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/c/syntax/package.lsp
Log Message:
-----------
[C$] Import symbol and avoid prefix.
Commit: b2ccbc8b9973d0d852a47646ffa802503385efaa
https://github.com/acl2/acl2/commit/b2ccbc8b9973d0d852a47646ffa802503385efaa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
A books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
[C$] Move some code to a new file.
Commit: b7afbbb26903702d57c6dea52090f050032bf7a7
https://github.com/acl2/acl2/commit/b7afbbb26903702d57c6dea52090f050032bf7a7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
A books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
[C$] Move some code to a new file.
Commit: 0a456ca59854c8699d36598394df1b23851c0724
https://github.com/acl2/acl2/commit/0a456ca59854c8699d36598394df1b23851c0724
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
A books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
[C$] Move some code to a new file.
Commit: 715e292a6b8d8580f2436807fde3fc2ee8bf0d08
https://github.com/acl2/acl2/commit/715e292a6b8d8580f2436807fde3fc2ee8bf0d08
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/validation-annotations.lisp
Log Message:
-----------
[C$] Add some doc.
Commit: 55a91ce233ef427337495aed9d4e9d21cb658838
https://github.com/acl2/acl2/commit/55a91ce233ef427337495aed9d4e9d21cb658838
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/uid.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
R books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validation.lisp
M books/kestrel/c/syntax/validator.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/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/wrap-fn-doc.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Eliminate file no longer needed.
Redirect book inclusions and XDOC references.
Commit: 6e60eee7be4bed37888bfdecab09a039cb6e40b2
https://github.com/acl2/acl2/commit/6e60eee7be4bed37888bfdecab09a039cb6e40b2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/top.lisp
Log Message:
-----------
[C$] Fix XDOC link.
Compare: https://github.com/acl2/acl2/compare/37bb516ee484...6e60eee7be4b
https://github.com/acl2/acl2/commit/05b5302cdb796d854e63fe7153382ba666541b13
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/memory.lisp
Log Message:
-----------
[arm] Improve rule.
Commit: 4cc35df39e2905ccb2f38ba18030dafd1b63d18e
https://github.com/acl2/acl2/commit/4cc35df39e2905ccb2f38ba18030dafd1b63d18e
Author: Eric Smith <ews...@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/arm/rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/rules.lisp
Log Message:
-----------
[axe/arm] Add UXTH and recharacterize flags for sub-immediate.
Commit: 61db1b98b70ecc26af21bd03836eede3f1ea1671
https://github.com/acl2/acl2/commit/61db1b98b70ecc26af21bd03836eede3f1ea1671
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/def-inst.lisp
M books/kestrel/arm/instructions.lisp
Log Message:
-----------
[arm] Start fleshing out unconditional instructions.
Commit: ffbd9d00a7a974dc9603790edbcda313eff888af
https://github.com/acl2/acl2/commit/ffbd9d00a7a974dc9603790edbcda313eff888af
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
Log Message:
-----------
[arm] Add REV16 instruction.
Commit: 6eec8bdd1c24cecd97e7e0794e02bce8c283c7f8
https://github.com/acl2/acl2/commit/6eec8bdd1c24cecd97e7e0794e02bce8c283c7f8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/def-inst.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/axe/arm/rule-lists.lisp
Log Message:
-----------
[axe/arm] Add support for one kind of unconditional instruction.
Commit: 999d78daf5df4c961e607b367aba0494aaf681bd
https://github.com/acl2/acl2/commit/999d78daf5df4c961e607b367aba0494aaf681bd
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/step.lisp
M books/kestrel/arm/tests/simple.lisp
M books/kestrel/axe/arm/run-until-return.lisp
Log Message:
-----------
[axe/arm] Improve checking of processor mode.
Now we get an error if not in ARM mode.
Commit: 371deba36d974d003b94da32ea239986a6391ed0
https://github.com/acl2/acl2/commit/371deba36d974d003b94da32ea239986a6391ed0
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
Log Message:
-----------
[arm] Add more instructions.
REV, REVSH, and ROR.
Commit: f3de74de64d3bc075ab37b4bc0c6a7acdde97050
https://github.com/acl2/acl2/commit/f3de74de64d3bc075ab37b4bc0c6a7acdde97050
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/apt/doc.lisp
Log Message:
-----------
[apt] Include remove-nesting in doc.
Commit: 689bb969882c79e18435b6aa04f02f05c1c9505e
https://github.com/acl2/acl2/commit/689bb969882c79e18435b6aa04f02f05c1c9505e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
[C$] Add missing ordered subtopic.
Commit: 2d60074541c778f719c1b64a3846f2b06eb57d44
https://github.com/acl2/acl2/commit/2d60074541c778f719c1b64a3846f2b06eb57d44
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
A books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
[C$] Move some code to a new file.
Commit: 12d46d37c40444cc40d7f1d9aed7175e768de5d6
https://github.com/acl2/acl2/commit/12d46d37c40444cc40d7f1d9aed7175e768de5d6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/c/syntax/package.lsp
Log Message:
-----------
[C$] Import symbol and avoid prefix.
Commit: b2ccbc8b9973d0d852a47646ffa802503385efaa
https://github.com/acl2/acl2/commit/b2ccbc8b9973d0d852a47646ffa802503385efaa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
A books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
[C$] Move some code to a new file.
Commit: b7afbbb26903702d57c6dea52090f050032bf7a7
https://github.com/acl2/acl2/commit/b7afbbb26903702d57c6dea52090f050032bf7a7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
A books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
[C$] Move some code to a new file.
Commit: 0a456ca59854c8699d36598394df1b23851c0724
https://github.com/acl2/acl2/commit/0a456ca59854c8699d36598394df1b23851c0724
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
A books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validation.lisp
Log Message:
-----------
[C$] Move some code to a new file.
Commit: 715e292a6b8d8580f2436807fde3fc2ee8bf0d08
https://github.com/acl2/acl2/commit/715e292a6b8d8580f2436807fde3fc2ee8bf0d08
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/validation-annotations.lisp
Log Message:
-----------
[C$] Add some doc.
Commit: 55a91ce233ef427337495aed9d4e9d21cb658838
https://github.com/acl2/acl2/commit/55a91ce233ef427337495aed9d4e9d21cb658838
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/uid.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
R books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validation.lisp
M books/kestrel/c/syntax/validator.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/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/wrap-fn-doc.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
Log Message:
-----------
[C$] Eliminate file no longer needed.
Redirect book inclusions and XDOC references.
Commit: 6e60eee7be4bed37888bfdecab09a039cb6e40b2
https://github.com/acl2/acl2/commit/6e60eee7be4bed37888bfdecab09a039cb6e40b2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-28 (Thu, 28 May 2026)
Changed paths:
M books/kestrel/c/syntax/top.lisp
Log Message:
-----------
[C$] Fix XDOC link.
Compare: https://github.com/acl2/acl2/compare/37bb516ee484...6e60eee7be4b
Reply all
Reply to author
Forward
0 new messages