[acl2/acl2] 5232b2: [C$] Add info field to desiniters

0 views
Skip to first unread message

Grant Jurgensen

unread,
May 3, 2026, 5:51:59 PM (4 days ago) May 3
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 5232b2e2eeded586735d72d0811267ef26c63d66
https://github.com/acl2/acl2/commit/5232b2e2eeded586735d72d0811267ef26c63d66
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-04-28 (Tue, 28 Apr 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C$] Add info field to desiniters

Now, designations are added as annotations to initializers which lack
designations (if they can be determined).


Commit: 8a185aa0d8c522f0089e5c2d145d3621431e6516
https://github.com/acl2/acl2/commit/8a185aa0d8c522f0089e5c2d145d3621431e6516
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-04-28 (Tue, 28 Apr 2026)

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

Log Message:
-----------
[C2C] Add controlled-configuration to split-gso


Commit: 10a715fdc690dd00ccaf0475256ab6c55a2ad926
https://github.com/acl2/acl2/commit/10a715fdc690dd00ccaf0475256ab6c55a2ad926
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp

Log Message:
-----------
[C$] Extend split-gso to handle more initializers

This makes initializers explicit when possible. It also removes
restrictions on unnamed and bit fields.


Commit: bee744d193d35f6ff7c385f8b603200232f4f012
https://github.com/acl2/acl2/commit/bee744d193d35f6ff7c385f8b603200232f4f012
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/acl2s/aspf/interface/top.lisp
M books/kestrel/arithmetic-light/limit-expt.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/defthm-axe-basic-tests.lisp
M books/kestrel/axe/defthm-axe.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/prover-basic-tests.lisp
M books/kestrel/axe/prover-tests.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv/bvplus.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.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/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/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/stringization.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.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/java/aij/assumptions.lisp
M books/kestrel/java/atj/code-generation.lisp
M books/kestrel/java/atj/common-code-generation.lisp
M books/kestrel/java/atj/java-abstract-syntax.lisp
M books/kestrel/java/atj/library-extensions.lisp
M books/kestrel/java/atj/shallow-quoted-constant-generation.lisp
M books/kestrel/java/atj/tests/acl2-times.lisp
M books/kestrel/java/language/binary-integer-literals.lisp
M books/kestrel/java/language/hexadecimal-integer-literals.lisp
M books/kestrel/java/language/primitive-operations.lisp
M books/kestrel/java/top.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
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/character-literal-codes.lisp
A books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/grammar.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
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/static-environments.lisp
M 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/std/omaps/core.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Merge branch 'testing-kestrel'


Commit: 9f7696b0327bed12d592a0aa31d80b975dec30b2
https://github.com/acl2/acl2/commit/9f7696b0327bed12d592a0aa31d80b975dec30b2
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[C$] Fix typo


Commit: 92da4b8c81c509c49cc19353f898202433a40cad
https://github.com/acl2/acl2/commit/92da4b8c81c509c49cc19353f898202433a40cad
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
Fix merge

And also correct a typo.


Commit: 38cb9f1763cdf2df24dc574231f0a8f9edc64d31
https://github.com/acl2/acl2/commit/38cb9f1763cdf2df24dc574231f0a8f9edc64d31
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
A books/kestrel/c/transformation/tests/split-gso/implicit-initer.c
A books/kestrel/c/transformation/tests/split-gso/unnamed-members.c

Log Message:
-----------
[C2C] Add split-gso tests

These tests show the new supported cases.


Commit: e514ed4df9e1c656d6d1a1bfc355015a64044e31
https://github.com/acl2/acl2/commit/e514ed4df9e1c656d6d1a1bfc355015a64044e31
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
A books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp

Log Message:
-----------
Merge branch 'testing-kestrel'


Compare: https://github.com/acl2/acl2/compare/58fe968355f7...e514ed4df9e1

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

Grant Jurgensen

unread,
May 3, 2026, 10:17:21 PM (4 days ago) May 3
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: b9146e8565a737d98f9eabff8f08d165e9b3db0e
https://github.com/acl2/acl2/commit/b9146e8565a737d98f9eabff8f08d165e9b3db0e
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/validator.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/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

Log Message:
-----------
Merge branch 'master' into testing-kestrel


Commit: c37583797e28a4ea6e0ad45175f0a587866819ce
https://github.com/acl2/acl2/commit/c37583797e28a4ea6e0ad45175f0a587866819ce
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-03 (Sun, 03 May 2026)

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

Log Message:
-----------
[C2C] Fix missing parents


Compare: https://github.com/acl2/acl2/compare/5d60d7a5a09d...c37583797e28

Grant Jurgensen

unread,
May 3, 2026, 10:17:39 PM (4 days ago) May 3
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
May 5, 2026, 10:01:38 PM (2 days ago) May 5
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: 0b98169d00441737568856f7f6cd6687df910b52
https://github.com/acl2/acl2/commit/0b98169d00441737568856f7f6cd6687df910b52
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:
M books/kestrel/jvm/call-stacks.lisp
M books/kestrel/jvm/frames.lisp

Log Message:
-----------
[jvm] Tweaks.


Commit: 533053b49d379b9d63b6a4391dd6d6cf0e2761b3
https://github.com/acl2/acl2/commit/533053b49d379b9d63b6a4391dd6d6cf0e2761b3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-04-30 (Thu, 30 Apr 2026)

Changed paths:
M books/kestrel/axe/.sys/get-di...@useless-runes.lsp
M books/kestrel/axe/get-disjuncts.lisp

Log Message:
-----------
[axe] Clarify code and speed up proofs.


Commit: aac28afd4ce21da31a0166aa07ee18ec1d565a1e
https://github.com/acl2/acl2/commit/aac28afd4ce21da31a0166aa07ee18ec1d565a1e
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/java/aij/assumptions.lisp
M books/kestrel/java/atj/code-generation.lisp
M books/kestrel/java/atj/common-code-generation.lisp
M books/kestrel/java/atj/java-abstract-syntax.lisp
M books/kestrel/java/atj/library-extensions.lisp
M books/kestrel/java/atj/shallow-quoted-constant-generation.lisp
M books/kestrel/java/atj/tests/acl2-times.lisp
M books/kestrel/java/language/binary-integer-literals.lisp
M books/kestrel/java/language/hexadecimal-integer-literals.lisp
M books/kestrel/java/language/primitive-operations.lisp
M books/kestrel/java/top.lisp
A books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
M books/kestrel/remora/abstract-syntax-trees.lisp
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/character-literal-codes.lisp
A books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/grammar.abnf
A books/kestrel/remora/parse-directory-files.acl2
A books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M 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

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


Commit: 10a715fdc690dd00ccaf0475256ab6c55a2ad926
https://github.com/acl2/acl2/commit/10a715fdc690dd00ccaf0475256ab6c55a2ad926
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp

Log Message:
-----------
[C$] Extend split-gso to handle more initializers

This makes initializers explicit when possible. It also removes
restrictions on unnamed and bit fields.


Commit: af109f9d3302dac59e0cec3f7c8430a847adae7a
https://github.com/acl2/acl2/commit/af109f9d3302dac59e0cec3f7c8430a847adae7a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-01 (Fri, 01 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/lexer.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validation-information.lisp

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


Commit: 4d3b0b1a9a1161a1d82713e3d91032309c9c50c0
https://github.com/acl2/acl2/commit/4d3b0b1a9a1161a1d82713e3d91032309c9c50c0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

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

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


Commit: b080e44d0edc0265ce18661f0ec121e85fa0e7a4
https://github.com/acl2/acl2/commit/b080e44d0edc0265ce18661f0ec121e85fa0e7a4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

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

Log Message:
-----------
[Remora] Add some structural AST ops.


Commit: 9931067c0d66e9a9e44196d4710df5868a2ca95f
https://github.com/acl2/acl2/commit/9931067c0d66e9a9e44196d4710df5868a2ca95f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

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

Log Message:
-----------
[Remora] Add desugaring of string literals.


Commit: be2632595f27915dfcbfd290c3fe0abfb06630df
https://github.com/acl2/acl2/commit/be2632595f27915dfcbfd290c3fe0abfb06630df
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

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

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


Commit: 527887248738ee9a18a5038be2a1e4e84fa69fd2
https://github.com/acl2/acl2/commit/527887248738ee9a18a5038be2a1e4e84fa69fd2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
Merge.


Commit: 49b581c97b3df9f80af74135b5943abf72f3f2fe
https://github.com/acl2/acl2/commit/49b581c97b3df9f80af74135b5943abf72f3f2fe
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

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

Log Message:
-----------
[Remora] Add desugaring of combined application.


Commit: acf686317afc2b1d12bb4a3061cc33929d030ce0
https://github.com/acl2/acl2/commit/acf686317afc2b1d12bb4a3061cc33929d030ce0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Import symbol.


Commit: c8fac6905996d3f7fdc6d0d20246986e0722bd44
https://github.com/acl2/acl2/commit/c8fac6905996d3f7fdc6d0d20246986e0722bd44
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

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

Log Message:
-----------
[Remora] Add two nested list fixtypes.


Commit: 10d24fa210c3f696665266d49511a8c3406e49ae
https://github.com/acl2/acl2/commit/10d24fa210c3f696665266d49511a8c3406e49ae
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

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

Log Message:
-----------
[Remora] Add some structural AST ops.


Commit: 6f477b3dbd497f7d2f3e692237b7f8ffb291237c
https://github.com/acl2/acl2/commit/6f477b3dbd497f7d2f3e692237b7f8ffb291237c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-01 (Fri, 01 May 2026)

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Import a symbol.


Commit: 09ca324b656a1a33751116e7a5e4a57a70ff84c3
https://github.com/acl2/acl2/commit/09ca324b656a1a33751116e7a5e4a57a70ff84c3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Consistently use tt font for `let`.


Commit: a3041f62f431b04b82ac4a8602db5f4b6a707d65
https://github.com/acl2/acl2/commit/a3041f62f431b04b82ac4a8602db5f4b6a707d65
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Extend desugaring.

Add desugaring of bracket expressions.

Expand doc to compare with Haskell implementation.
Commit: 059fd35d94541df709dd5a46d647524e92363f8a
https://github.com/acl2/acl2/commit/059fd35d94541df709dd5a46d647524e92363f8a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/compress1.lisp

Log Message:
-----------
[acl2-arrays] Improve comments.


Commit: 4516aec8640ab0ec37dbbd1f623dd3ba18cfe82f
https://github.com/acl2/acl2/commit/4516aec8640ab0ec37dbbd1f623dd3ba18cfe82f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
A books/kestrel/axe/pre-stp-rules.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/top.lisp

Log Message:
-----------
[axe] Create a book that brings in the pre-stp rules.


Commit: 58baad5154a396642346622815af637cdc817aea
https://github.com/acl2/acl2/commit/58baad5154a396642346622815af637cdc817aea
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Remove stray annotaation.


Commit: 9428d940aacd3eab3132cd623c575ad0c726983f
https://github.com/acl2/acl2/commit/9428d940aacd3eab3132cd623c575ad0c726983f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Finish desugaring.

Include `let` in the core for now, for the (slightly tricky) reasons described
in the added documentation.


Commit: 10d515b829fe25d3b6eff88ef91bbb106c737ee0
https://github.com/acl2/acl2/commit/10d515b829fe25d3b6eff88ef91bbb106c737ee0
Author: Eric McCarthy <mcca...@kestrel.edu>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[remora] import some symbols from acl2 and str packages


Commit: 0c2a9ec7bef63fb107a5ba9584c71e32e3ddd7aa
https://github.com/acl2/acl2/commit/0c2a9ec7bef63fb107a5ba9584c71e32e3ddd7aa
Author: Eric McCarthy <mcca...@kestrel.edu>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
A books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/syntax-abstraction.lisp

Log Message:
-----------
[remora] move identifier-syntax-related code into new file identifier-syntax.lisp. Also get rid of some no-longer-needd package prefixes, and comment out the xdoc for the shape macro since there is a name collision (which will be fixed soon)


Commit: c8b229579e0a23febb81a3d178934b38cc3b62df
https://github.com/acl2/acl2/commit/c8b229579e0a23febb81a3d178934b38cc3b62df
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
A books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/syntax-abstraction.lisp

Log Message:
-----------
Merge commit '0c2a9ec7bef63fb107a5ba9584c71e32e3ddd7aa' into HEAD


Commit: 39e9a79fcad231c8069c0a2ba297b98ea072ab91
https://github.com/acl2/acl2/commit/39e9a79fcad231c8069c0a2ba297b98ea072ab91
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

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


Commit: db64582e5de740c15c9941b118379f31ed71d30e
https://github.com/acl2/acl2/commit/db64582e5de740c15c9941b118379f31ed71d30e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/frame-flattening.lisp

Log Message:
-----------
[Remora] Add frame flattening transformation.


Commit: f8a33ec5968ef6dc16a26c49db2586a984e57cde
https://github.com/acl2/acl2/commit/f8a33ec5968ef6dc16a26c49db2586a984e57cde
Author: Eric McCarthy <mcca...@kestrel.edu>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/static-environments.lisp

Log Message:
-----------
[remora] change name of dims to shape macro from "shape" to "shp" to avoid name clash with the "shape" type


Commit: 5506801f00b70b77d1e98bb023b524ed890964a7
https://github.com/acl2/acl2/commit/5506801f00b70b77d1e98bb023b524ed890964a7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
A books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/syntax-abstraction.lisp

Log Message:
-----------
Merge and resolve conflicts.


Commit: 8be8fc0ff3fd78c166fff320b0d72a0e47b0c146
https://github.com/acl2/acl2/commit/8be8fc0ff3fd78c166fff320b0d72a0e47b0c146
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Prove more properties of desugaring.


Commit: 90180c157d21a6e2a169695f456e1b9c728741de
https://github.com/acl2/acl2/commit/90180c157d21a6e2a169695f456e1b9c728741de
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/static-environments.lisp

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


Commit: 11563705e3583a212d714e289bfe184b03f9fe68
https://github.com/acl2/acl2/commit/11563705e3583a212d714e289bfe184b03f9fe68
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
M books/kestrel/remora/static-environments.lisp

Log Message:
-----------
Merge commit 'f8a33ec5968ef6dc16a26c49db2586a984e57cde' into HEAD


Commit: 15e46589b6b5db314d9358b596bb35b188f2d094
https://github.com/acl2/acl2/commit/15e46589b6b5db314d9358b596bb35b188f2d094
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Add more properties of desugaring.


Commit: 9dba0c50cbb8d0b911df554c9eb8151dbf998cf4
https://github.com/acl2/acl2/commit/9dba0c50cbb8d0b911df554c9eb8151dbf998cf4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:

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


Commit: 4037bc2a7439e9597486bf79dbcb27501d9d429b
https://github.com/acl2/acl2/commit/4037bc2a7439e9597486bf79dbcb27501d9d429b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Generate more core-AST-checking predicates.


Commit: 6eb939ea6d0a847ea7141fc6a5fd77992636877c
https://github.com/acl2/acl2/commit/6eb939ea6d0a847ea7141fc6a5fd77992636877c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Add theorems about structural ops.


Commit: e2d6e9057b50aaacc0470004969e8f02d841e974
https://github.com/acl2/acl2/commit/e2d6e9057b50aaacc0470004969e8f02d841e974
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
M books/kestrel/remora/frame-flattening.lisp

Log Message:
-----------
[Remora] Prove core preservation of frame flattening.


Commit: 58fe968355f772e05c86209b47d876e4166b640f
https://github.com/acl2/acl2/commit/58fe968355f772e05c86209b47d876e4166b640f
Author: Eric McCarthy <mcca...@kestrel.edu>
Date: 2026-05-02 (Sat, 02 May 2026)

Changed paths:
A books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
[remora] define xxx-wf-ast-p well-formed predicates on asts


Commit: c48471dca5a210a9f1c6f48b5ec9e9e21bf81776
https://github.com/acl2/acl2/commit/c48471dca5a210a9f1c6f48b5ec9e9e21bf81776
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-02 (Sat, 02 May 2026)

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

Log Message:
-----------
[Remora] Fix XDOC link.


Commit: 91a4d57bf07a1b3c8139d053e309ffd8aa4ccf37
https://github.com/acl2/acl2/commit/91a4d57bf07a1b3c8139d053e309ffd8aa4ccf37
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:

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


Commit: 5b5fc52bbd2c608d7318b697028bda17354f9d4a
https://github.com/acl2/acl2/commit/5b5fc52bbd2c608d7318b697028bda17354f9d4a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
A books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp

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


Commit: bcafe9e154b0bb5c778bfe3fb4641f4b1b2db0e8
https://github.com/acl2/acl2/commit/bcafe9e154b0bb5c778bfe3fb4641f4b1b2db0e8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/aref1.lisp
M books/kestrel/acl2-arrays/make-empty-array.lisp

Log Message:
-----------
[acl2-arrays] Clarify.


Commit: b52f0256de7eb63f76d0bbaae95ced60dfaf2ae2
https://github.com/acl2/acl2/commit/b52f0256de7eb63f76d0bbaae95ced60dfaf2ae2
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/.sys/make-into-ar...@useless-runes.lsp
M books/kestrel/acl2-arrays/make-into-array-with-len.lisp

Log Message:
-----------
[acl2-arrays] Generalize rules.


Commit: 0915da35d963143b5e5e2c5f09f11d0c0cae634c
https://github.com/acl2/acl2/commit/0915da35d963143b5e5e2c5f09f11d0c0cae634c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/make-empty-array.lisp
M books/kestrel/acl2-arrays/make-into-array-with-len.lisp
M books/kestrel/acl2-arrays/make-into-array.lisp

Log Message:
-----------
[acl2-arrays] Clarify.


Commit: 919cadc91e950a44aa7023a1ddd5d3f098274b91
https://github.com/acl2/acl2/commit/919cadc91e950a44aa7023a1ddd5d3f098274b91
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/make-into-array-with-len.lisp
M books/kestrel/acl2-arrays/make-into-array.lisp

Log Message:
-----------
[acl2-arrays] Reduce includes.


Commit: 64ddcc477870f06830a64400287d381110fed7d4
https://github.com/acl2/acl2/commit/64ddcc477870f06830a64400287d381110fed7d4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/array-to-alist.lisp
M books/kestrel/acl2-arrays/make-empty-array.lisp
M books/kestrel/acl2-arrays/make-into-array-with-len.lisp
M books/kestrel/acl2-arrays/make-into-array.lisp

Log Message:
-----------
[acl2-arrays] Clarify.

Also simplify hints.


Commit: 5d60d7a5a09daf1c617d5a5b615d1f44240d8e34
https://github.com/acl2/acl2/commit/5d60d7a5a09daf1c617d5a5b615d1f44240d8e34
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
A books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/abstract-syntax.lisp

Log Message:
-----------
Merge commit '58fe968355f772e05c86209b47d876e4166b640f' into HEAD


Commit: b53ce9052e8a76b4225d9383def08ce9c852a4bf
https://github.com/acl2/acl2/commit/b53ce9052e8a76b4225d9383def08ce9c852a4bf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/make-empty-array.lisp
M books/kestrel/acl2-arrays/make-into-array.lisp

Log Message:
-----------
[acl2-arrays] Generalize more rules.


Commit: b26ed19dfac0d701709ccbfb16b0bf9d1a946104
https://github.com/acl2/acl2/commit/b26ed19dfac0d701709ccbfb16b0bf9d1a946104
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
R books/kestrel/acl2-arrays/.sys/make-emp...@useless-runes.lsp
A books/kestrel/acl2-arrays/.sys/new-a...@useless-runes.lsp
M books/kestrel/acl2-arrays/acl2-arrays.lisp
R books/kestrel/acl2-arrays/make-empty-array.lisp
M 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/axe/bounded-dag-parent-arrayp.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.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/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/jvm/lifter.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-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/node-replacement-array.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/prove-with-stp2.lisp
M books/kestrel/axe/prover-common.lisp
M books/kestrel/axe/prover.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/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/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/translation-array.lisp
M books/kestrel/axe/wf-dagp.lisp

Log Message:
-----------
[acl2-arrays] Rename make-empty-array to new-array1.

And similarly for make-empty-array-with-default.


Commit: e514ed4df9e1c656d6d1a1bfc355015a64044e31
https://github.com/acl2/acl2/commit/e514ed4df9e1c656d6d1a1bfc355015a64044e31
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-constructors.lisp
A books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parse-directory-files.lisp
M books/kestrel/remora/parser-interface.lisp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/syntax-abstraction.lisp

Log Message:
-----------
Merge branch 'testing-kestrel'


Commit: 92c92c2a336ce7f2d4705934bc9bd0fdf37ee9d4
https://github.com/acl2/acl2/commit/92c92c2a336ce7f2d4705934bc9bd0fdf37ee9d4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/axe/concretize-with-contexts.lisp
M books/kestrel/axe/dag-size.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/find-probable-facts-simple.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/rewriter-alt.lisp

Log Message:
-----------
[axe] Optimize.


Commit: e19f8b42a9d12e23ee2a87acd0a3d619b83109b9
https://github.com/acl2/acl2/commit/e19f8b42a9d12e23ee2a87acd0a3d619b83109b9
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/make-into-array-with-len.lisp
M books/kestrel/acl2-arrays/make-into-array.lisp

Log Message:
-----------
[acl2-arrays] Update todos.


Commit: 92bee35b58dd943103c28c2b8c50132a9cad9c3a
https://github.com/acl2/acl2/commit/92bee35b58dd943103c28c2b8c50132a9cad9c3a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/x86/support32.lisp

Log Message:
-----------
[x86] Add rule.

Uses a better normal form for the slice term.


Commit: b14401df6a221d9ed5fd2f1709cba284cfaaccd6
https://github.com/acl2/acl2/commit/b14401df6a221d9ed5fd2f1709cba284cfaaccd6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/axe/jvm/rules-in-rule-lists-jvm.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/x86/rule-lists.lisp

Log Message:
-----------
[axe] Use the convert-to-bv-rules more.

Also use the rule to convert slice's arg to a bv.


Commit: c2c0eb9260bf65e9b4d2135c397757a031e4909f
https://github.com/acl2/acl2/commit/c2c0eb9260bf65e9b4d2135c397757a031e4909f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.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/subst-free.lisp

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


Commit: 3c497d7b5308d5414465567a0d4b80289d42031d
https://github.com/acl2/acl2/commit/3c497d7b5308d5414465567a0d4b80289d42031d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/x86/rule-lists.lisp

Log Message:
-----------
[axe] Build in rule more deeply.
Commit: c3a648a205ab924ef828810e126bbe3f246e4fb6
https://github.com/acl2/acl2/commit/c3a648a205ab924ef828810e126bbe3f246e4fb6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
A books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/abstract-syntax.lisp

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


Commit: 8f7559950fa2c2a0d7469059ed2f1eb837b14946
https://github.com/acl2/acl2/commit/8f7559950fa2c2a0d7469059ed2f1eb837b14946
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.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/subst-free.lisp

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


Commit: 12bf5dc307e987281e2d9c4d3088f20290a41559
https://github.com/acl2/acl2/commit/12bf5dc307e987281e2d9c4d3088f20290a41559
Author: Eric McCarthy <mcca...@kestrel.edu>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/remora/parse-directory-files.lisp
A books/kestrel/remora/printer.lisp
M books/kestrel/remora/top.lisp

Log Message:
-----------
[remora] add Wadler-style pretty printer and round-trip tests


Commit: ec50a736224e65377eb1c19bee0ffd260b43f304
https://github.com/acl2/acl2/commit/ec50a736224e65377eb1c19bee0ffd260b43f304
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-03 (Sun, 03 May 2026)

Changed paths:
M books/kestrel/remora/parse-directory-files.lisp
A books/kestrel/remora/printer.lisp
M books/kestrel/remora/top.lisp

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


Commit: 1316b8420c4c9c762d4a25fa911bc49d767a3951
https://github.com/acl2/acl2/commit/1316b8420c4c9c762d4a25fa911bc49d767a3951
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
A books/kestrel/acl2-arrays/alist-to-array1-with-len.lisp
A books/kestrel/acl2-arrays/alist-to-array1.lisp
R books/kestrel/acl2-arrays/make-into-array-with-len.lisp
R books/kestrel/acl2-arrays/make-into-array.lisp
M books/kestrel/acl2-arrays/top.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-size-sparse-tests.lisp
M books/kestrel/axe/dagify0.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/find-probable-facts.lisp
M books/kestrel/axe/get-disjuncts.lisp
M books/kestrel/axe/jvm/lifter.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/merge-dag-into-dag-quick.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/prune-with-contexts.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/wf-dagp.lisp

Log Message:
-----------
[acl2-arrays] Rename make-into-array to alist-to-array1.

Add similarly for make-into-array-with-len.


Commit: 8dc8c776cc18c29dfd66127ce87bc74f7a6e74dc
https://github.com/acl2/acl2/commit/8dc8c776cc18c29dfd66127ce87bc74f7a6e74dc
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.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/subst-free.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.lisp
M books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parse-directory-files.lisp
A books/kestrel/remora/printer.lisp
M books/kestrel/remora/top.lisp

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


Commit: 1e6e7670a65ba3e5e867aca4bcda4c248d2021f0
https://github.com/acl2/acl2/commit/1e6e7670a65ba3e5e867aca4bcda4c248d2021f0
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/split-gso.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.lisp
M books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/frame-flattening.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parse-directory-files.lisp
A books/kestrel/remora/printer.lisp
M books/kestrel/remora/top.lisp

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


Commit: 4c499a6a7be73af93fb0fdbd33b1d9802991c57f
https://github.com/acl2/acl2/commit/4c499a6a7be73af93fb0fdbd33b1d9802991c57f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
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/axe/.sys/get-di...@useless-runes.lsp
M books/kestrel/axe/bounded-dag-parent-arrayp.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/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.lisp
M books/kestrel/axe/jvm/lifter.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/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-common.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/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/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/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/wf-dagp.lisp
M books/kestrel/jvm/call-stacks.lisp
M books/kestrel/jvm/frames.lisp

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


Commit: 13cdb54c506e65bfee8cea1b7c5d33a967a71bf2
https://github.com/acl2/acl2/commit/13cdb54c506e65bfee8cea1b7c5d33a967a71bf2
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/jvm/operand-stacks.lisp

Log Message:
-----------
[jvm] Improve file organization.


Commit: bc3f887116f87a9f6e4f0bfb7af0e02cca9fba76
https://github.com/acl2/acl2/commit/bc3f887116f87a9f6e4f0bfb7af0e02cca9fba76
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/jvm/operand-stacks.lisp

Log Message:
-----------
[jvm] Continue modernizing file.


Commit: aef9dff1be76f87898ed3e0de546beb0ba4ca032
https://github.com/acl2/acl2/commit/aef9dff1be76f87898ed3e0de546beb0ba4ca032
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv/bitops.lisp

Log Message:
-----------
[bv/axe] Replace b-not with bitnot.


Commit: 8e3f341c7e056862cbb31c3c45bdd229536135bb
https://github.com/acl2/acl2/commit/8e3f341c7e056862cbb31c3c45bdd229536135bb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M GNUmakefile
M LICENSE
M acl2-check.lisp
M acl2-fns.lisp
M acl2-init.lisp
M acl2.lisp
M akcl-acl2-trace.lisp
M all-files.txt
M allegro-acl2-trace.lisp
M apply-constraints.lisp
M apply-prim.lisp
M apply-raw.lisp
M apply.lisp
M axioms.lisp
M basis-a.lisp
M basis-b.lisp
M bdd.lisp
M bin/purity-acl2.sh
M books/GNUmakefile
M books/Makefile-generic
M books/Makefile-psubdirs
M books/Makefile-subdirs
M books/acl2s/aspf/interface/top.lisp
M books/acl2s/ccg/ccg.lisp
M books/acl2s/distribution/acl2s-hooks/interaction-hooks.lisp
M books/acl2s/distribution/acl2s-hooks/markup-hooks.lisp
M books/acl2s/distribution/acl2s-hooks/protection-hooks.lisp
M books/acl2s/distribution/acl2s-hooks/super-history.lisp
M books/build/cert.pl
M books/build/doc.lisp
M books/build/lib/Certlib.pm
M books/build/universal-dependency.certdep
A books/centaur/bridge/bridge-sbcl-raw.lsp
M books/centaur/bridge/python/README
M books/centaur/bridge/python/async_demo.py
M books/centaur/bridge/python/demo.py
M books/centaur/bridge/ruby/README
M books/centaur/bridge/top.lisp
M books/centaur/esim/tests/.sys/com...@useless-runes.lsp
M books/centaur/esim/tutorial/.sys/in...@useless-runes.lsp
M books/centaur/fgl/annotation.lisp
M books/centaur/fgl/binder-rules.lisp
M books/centaur/fgl/clauseproc.lisp
M books/centaur/fgl/config.lisp
M books/centaur/fgl/congruence-rules.lisp
M books/centaur/fgl/congruence.lisp
M books/centaur/fgl/constraint-db.lisp
M books/centaur/fgl/contexts.lisp
M books/centaur/fgl/fgl-object.lisp
M books/centaur/fgl/fgl-primitive-congruences.lisp
M books/centaur/fgl/helper-utils.lisp
M books/centaur/fgl/interp-st.lisp
M books/centaur/fgl/interp.lisp
M books/centaur/fgl/logicman.lisp
M books/centaur/fgl/pathcond-aignet.lisp
M books/centaur/fgl/pathcond.lisp
M books/centaur/fgl/primitives-stub.lisp
A books/centaur/fgl/reference-ctrex.lisp
M books/centaur/fgl/rules.lisp
M books/centaur/fgl/svex-primitives.lisp
M books/centaur/fgl/syntax-bind.lisp
M books/centaur/fgl/top.lisp
M books/centaur/fgl/trace.lisp
M books/centaur/gl/.sys/gl-generic-...@useless-runes.lsp
M books/centaur/gl/.sys/gl-generic-...@useless-runes.lsp
M books/centaur/gl/.sys/gl-gener...@useless-runes.lsp
M books/centaur/gl/.sys/gl-t...@useless-runes.lsp
M books/centaur/gl/.sys/g...@useless-runes.lsp
M books/centaur/gl/.sys/glcp-rewr...@useless-runes.lsp
M books/centaur/gl/.sys/rewrite...@useless-runes.lsp
M books/centaur/gl/.sys/run-gi...@useless-runes.lsp
M books/centaur/gl/gl-generic-clause-proc.lisp
M books/centaur/gl/gl-generic-interp-defs.lisp
M books/centaur/gl/gl-generic-interp.lisp
M books/centaur/gl/glcp-rewrite-tables.lisp
M books/centaur/gl/rewrite-tables.lisp
M books/centaur/gl/run-gified-cp.lisp
M books/centaur/glmc/.sys/glmc-gene...@useless-runes.lsp
M books/centaur/glmc/.sys/gl...@useless-runes.lsp
M books/centaur/glmc/glmc-generic-proof.lisp
M books/centaur/glmc/glmc.lisp
M books/centaur/meta/.sys/bindi...@useless-runes.lsp
M books/centaur/meta/.sys/congr...@useless-runes.lsp
M books/centaur/meta/.sys/equiv...@useless-runes.lsp
A books/centaur/meta/.sys/fixed-e...@useless-runes.lsp
A books/centaur/meta/.sys/fnsy...@useless-runes.lsp
M books/centaur/meta/.sys/lambda-...@useless-runes.lsp
M books/centaur/meta/.sys/let...@useless-runes.lsp
M books/centaur/meta/.sys/parse-...@useless-runes.lsp
M books/centaur/meta/.sys/pseudo-re...@useless-runes.lsp
A books/centaur/meta/.sys/pseudo-ter...@useless-runes.lsp
A books/centaur/meta/.sys/subst...@useless-runes.lsp
M books/centaur/meta/.sys/su...@useless-runes.lsp
M books/centaur/meta/.sys/subst...@useless-runes.lsp
M books/centaur/meta/.sys/term...@useless-runes.lsp
M books/centaur/meta/.sys/unify-...@useless-runes.lsp
M books/centaur/meta/.sys/urew...@useless-runes.lsp
M books/centaur/meta/.sys/variab...@useless-runes.lsp
M books/centaur/meta/bindinglist.lisp
M books/centaur/meta/congruence.lisp
M books/centaur/meta/equivalence.lisp
A books/centaur/meta/fnsymlist.lisp
M books/centaur/meta/package.lsp
M books/centaur/meta/pseudo-rewrite-rule.lisp
M books/centaur/meta/subst-vars.lisp
M books/centaur/meta/subst.lisp
M books/centaur/meta/term-vars.lisp
M books/centaur/meta/urewrite.lisp
M books/centaur/misc/.sys/bound-r...@useless-runes.lsp
M books/centaur/misc/.sys/conte...@useless-runes.lsp
M books/centaur/misc/.sys/defa...@useless-runes.lsp
M books/centaur/misc/.sys/evaluator-m...@useless-runes.lsp
M books/centaur/misc/.sys/interp-func...@useless-runes.lsp
M books/centaur/misc/context-rw.lisp
M books/centaur/misc/defapply.lisp
M books/centaur/misc/interp-function-lookup.lisp
M books/centaur/misc/seed-random.lisp
M books/centaur/sv/svex/.sys/evals-eq...@useless-runes.lsp
M books/centaur/sv/svex/.sys/svex-env-...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-ge...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-sto...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-stobj-...@useless-runes.lsp
M books/centaur/sv/svtv/.sys/svtv-...@useless-runes.lsp
M books/centaur/sv/svtv/svtv-to-fsm-defs.lisp
M books/centaur/svl/.sys/svex-s...@useless-runes.lsp
M books/centaur/svl/.sys/svl-f...@useless-runes.lsp
M books/centaur/svl/.sys/type...@useless-runes.lsp
M books/centaur/svl/meta/.sys/4vec-r...@useless-runes.lsp
M books/centaur/svl/meta/.sys/bits...@useless-runes.lsp
M books/centaur/svl/meta/.sys/svex-eval...@useless-runes.lsp
M books/centaur/svl/svex-reduce/.sys/ba...@useless-runes.lsp
M books/centaur/svl/svex-reduce/.sys/integerp...@useless-runes.lsp
M books/centaur/svl/svex-reduce/.sys/simplify-bi...@useless-runes.lsp
M books/centaur/svl/svex-reduce/.sys/svex-reduc...@useless-runes.lsp
M books/centaur/vl/mlib/.sys/desig...@useless-runes.lsp
M books/centaur/vl2014/mlib/.sys/desig...@useless-runes.lsp
M books/clause-processors/.sys/ev-th...@useless-runes.lsp
M books/clause-processors/.sys/indu...@useless-runes.lsp
M books/clause-processors/.sys/just-...@useless-runes.lsp
M books/clause-processors/.sys/meta-ext...@useless-runes.lsp
M books/clause-processors/.sys/replace-e...@useless-runes.lsp
M books/clause-processors/.sys/witne...@useless-runes.lsp
M books/clause-processors/ev-theoremp.lisp
M books/clause-processors/induction.lisp
M books/clause-processors/just-expand.lisp
M books/clause-processors/meta-extract-user.lisp
M books/clause-processors/replace-equalities.lisp
M books/clause-processors/witness-cp.lisp
M books/defexec/dag-unification/dag-unification-l.lisp
M books/defexec/dag-unification/dag-unification-rules.lisp
M books/defexec/dag-unification/dag-unification-st.lisp
M books/defexec/dag-unification/dags.lisp
M books/defexec/dag-unification/list-unification-rules.lisp
M books/defexec/dag-unification/matching.lisp
M books/defexec/dag-unification/subsumption-subst.lisp
M books/defexec/dag-unification/subsumption.lisp
M books/defexec/dag-unification/terms-as-dag.lisp
M books/defexec/dag-unification/terms-dag-stobj.lisp
M books/defexec/dag-unification/terms.lisp
M books/demos/floating-point-log.txt
M books/demos/geneqv-test-log.txt
M books/demos/gl-and-std/.sys/defaggregat...@useless-runes.lsp
M books/demos/gl-and-std/.sys/defaggrega...@useless-runes.lsp
M books/demos/gl-and-std/.sys/defprod-...@useless-runes.lsp
M books/demos/memoize-partial-log.txt
M books/doc/.sys/public...@useless-runes.lsp
M books/doc/cert.acl2
A books/doc/images/acs-book-cover.jpg
A books/doc/images/car-book-cover.jpg
M books/doc/practices.lisp
M books/doc/publications.lisp
M books/doc/relnotes.lisp
M books/doc/top.lisp
M books/emacs/acl2-doc-open-url.el
M books/emacs/acl2-doc.el
M books/emacs/emacs-acl2.el
M books/emacs/html-to-xdoc.el
M books/emacs/monitor.el
M books/hacking/dynamic-make-event-test.lisp
M books/hacking/hacker-pkg.lsp
M books/hacking/table-guard.lisp
M books/hints/.sys/basic...@useless-runes.lsp
M books/kestrel/.sys/top...@useless-runes.lsp
M books/kestrel/.sys/t...@useless-runes.lsp
A books/kestrel/abstract-domains/.sys/t...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/arith...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/co...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/ex...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/i...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/min-max...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/noninterval-...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/portc...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/subint...@useless-runes.lsp
A books/kestrel/abstract-domains/intervals/.sys/t...@useless-runes.lsp
M books/kestrel/abstract-domains/intervals/arithmetic.lisp
M books/kestrel/abstract-domains/intervals/core.lisp
M books/kestrel/abstract-domains/intervals/min-max-support.lisp
M books/kestrel/abstract-domains/intervals/subintervalp.lisp
M books/kestrel/abstract-domains/intervals/top.lisp
A books/kestrel/abstract-domains/many-valued-logics/.sys/3...@useless-runes.lsp
A books/kestrel/abstract-domains/many-valued-logics/.sys/t...@useless-runes.lsp
M books/kestrel/abstract-domains/many-valued-logics/3vl.lisp
M books/kestrel/acl2-arrays/.sys/aref1...@useless-runes.lsp
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-list.lisp
M books/kestrel/acl2-arrays/aref1.lisp
M books/kestrel/acl2-arrays/array-to-alist.lisp
M books/kestrel/acl2-arrays/array1p.lisp
M books/kestrel/acl2-arrays/bounded-nat-alists.lisp
M books/kestrel/acl2-arrays/compress1.lisp
M books/kestrel/acl2-arrays/constants.lisp
M books/kestrel/acl2-arrays/copy-array-vals.lisp
M books/kestrel/acl2-arrays/dimensions.lisp
M books/kestrel/acl2-arrays/expandable-arrays.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/acl2data/gather/event-symbol-table.lisp
M books/kestrel/acl2data/gather/remove-rune-checkpoints.lisp
A books/kestrel/acl2pl/.gitattributes
M books/kestrel/acl2pl/.sys/evaluati...@useless-runes.lsp
M books/kestrel/acl2pl/.sys/evalu...@useless-runes.lsp
M books/kestrel/acl2pl/equivalence.lisp
M books/kestrel/acl2pl/evaluation-states.lisp
M books/kestrel/acl2pl/evaluation.lisp
A books/kestrel/acl2pl/grammar.abnf
A books/kestrel/acl2pl/grammar.lisp
M books/kestrel/acl2pl/package.lsp
M books/kestrel/acl2pl/primitive-functions.lisp
A books/kestrel/acl2pl/reader-tests.acl2
A books/kestrel/acl2pl/reader-tests.lisp
A books/kestrel/acl2pl/sharp-dot-test-consts.lisp
M books/kestrel/acl2pl/top.lisp
A books/kestrel/air/.sys/portc...@useless-runes.lsp
A books/kestrel/air/.sys/t...@useless-runes.lsp
A books/kestrel/air/model-0/.sys/library-e...@useless-runes.lsp
A books/kestrel/air/model-0/.sys/portc...@useless-runes.lsp
A books/kestrel/air/model-0/.sys/t...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/corre...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/exa...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/field-e...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/fi...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/pfcs-con...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/pfcs-l...@useless-runes.lsp
A books/kestrel/air/model-0/air/.sys/tra...@useless-runes.lsp
M books/kestrel/air/model-0/air/correctness.lisp
M books/kestrel/air/model-0/air/example.lisp
M books/kestrel/air/model-0/air/field-encoding.lisp
M books/kestrel/air/model-0/air/pfcs-constraints.lisp
M books/kestrel/air/model-0/air/pfcs-lifting.lisp
M books/kestrel/air/model-0/air/traces.lisp
A books/kestrel/air/model-0/language/.sys/abstrac...@useless-runes.lsp
A books/kestrel/air/model-0/language/.sys/dynamic-...@useless-runes.lsp
A books/kestrel/air/model-0/language/.sys/exa...@useless-runes.lsp
A books/kestrel/air/model-0/language/.sys/input-outpu...@useless-runes.lsp
A books/kestrel/air/model-0/language/.sys/static-s...@useless-runes.lsp
M books/kestrel/air/model-0/language/dynamic-semantics.lisp
M books/kestrel/air/model-0/language/example.lisp
M books/kestrel/algorithm-theories/generic-tail-rec.lisp
M books/kestrel/alists-light/.sys/acons-...@useless-runes.lsp
M books/kestrel/alists-light/alists-equiv-on.lisp
M books/kestrel/alists-light/compat.lisp
M books/kestrel/alists-light/keep-pairs.lisp
M books/kestrel/alists-light/lookup-eq-safe.lisp
M books/kestrel/alists-light/lookup-eq.lisp
M books/kestrel/alists-light/lookup-equal-safe.lisp
M books/kestrel/alists-light/lookup-equal.lisp
M books/kestrel/alists-light/lookup-safe.lisp
M books/kestrel/alists-light/lookup.lisp
M books/kestrel/alists-light/pairlis-dollar.lisp
M books/kestrel/alists-light/rassoc-equal.lisp
M books/kestrel/alists-light/string-string-alistp.lisp
M books/kestrel/alists-light/strip-cars.lisp
M books/kestrel/alists-light/strip-cars2.lisp
M books/kestrel/alists-light/top.lisp
M books/kestrel/alists-light/uniquify-alist-eq.lisp
A books/kestrel/apt/.sys/simplify-conj...@useless-runes.lsp
A books/kestrel/apt/.sys/simplify-c...@useless-runes.lsp
M books/kestrel/apt/common-concepts.lisp
M books/kestrel/apt/doc.lisp
M books/kestrel/apt/drop-irrelevant-params.lisp
M books/kestrel/apt/finite-difference.lisp
M books/kestrel/apt/isodata-doc.lisp
M books/kestrel/apt/isodata-tests.lisp
M books/kestrel/apt/lift-iso-doc.lisp
M books/kestrel/apt/lift-iso.lisp
M books/kestrel/apt/propagate-iso-doc.lisp
M books/kestrel/apt/rename-calls.lisp
M books/kestrel/apt/rename-params.lisp
M books/kestrel/apt/restrict-tests.lisp
M books/kestrel/apt/schemalg-divconq-list-0-1-2-doc.lisp
M books/kestrel/apt/schemalg-divconq-list-0-1-doc.lisp
A books/kestrel/apt/simplify-conjunctions-tests.lisp
A books/kestrel/apt/simplify-conjunctions.lisp
M books/kestrel/apt/simplify-defun-impl.lisp
M books/kestrel/apt/simplify-defun-sk-doc.lisp
M books/kestrel/apt/simplify-doc.lisp
M books/kestrel/apt/simplify-term-doc.lisp
M books/kestrel/apt/simplify-term-impl.lisp
M books/kestrel/apt/solve-method-axe-rewriter.lisp
M books/kestrel/apt/solve.lisp
M books/kestrel/apt/tailrec-doc.lisp
M books/kestrel/apt/tailrec.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/deftransformation.lisp
M books/kestrel/apt/utilities/find-a-base-case-tests.lisp
M books/kestrel/apt/utilities/find-a-base-case.lisp
M books/kestrel/apt/wrap-output.lisp
M books/kestrel/arithmetic-light/.sys/l...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/m...@useless-runes.lsp
M books/kestrel/arithmetic-light/.sys/m...@useless-runes.lsp
M books/kestrel/arithmetic-light/ash.lisp
M books/kestrel/arithmetic-light/cancel-addends.lisp
M books/kestrel/arithmetic-light/ceiling-of-lg.lisp
M books/kestrel/arithmetic-light/ceiling.lisp
M books/kestrel/arithmetic-light/divide.lisp
M books/kestrel/arithmetic-light/evenp.lisp
M books/kestrel/arithmetic-light/expt.lisp
M books/kestrel/arithmetic-light/expt2.lisp
M books/kestrel/arithmetic-light/floor.lisp
M books/kestrel/arithmetic-light/floor2.lisp
M books/kestrel/arithmetic-light/ifix.lisp
M books/kestrel/arithmetic-light/lg.lisp
M books/kestrel/arithmetic-light/limit-expt.lisp
M books/kestrel/arithmetic-light/log2.lisp
M books/kestrel/arithmetic-light/mod.lisp
M books/kestrel/arithmetic-light/plus-times-and-divide.lisp
M books/kestrel/arithmetic-light/power-of-2p.lisp
M books/kestrel/arithmetic-light/top.lisp
M books/kestrel/arithmetic-light/truncate.lisp
M books/kestrel/arithmetic-light/unguarded-built-ins.lisp
R books/kestrel/arm/.sys/ar...@useless-runes.lsp
M books/kestrel/arm/.sys/dec...@useless-runes.lsp
A books/kestrel/arm/.sys/def-...@useless-runes.lsp
A books/kestrel/arm/.sys/d...@useless-runes.lsp
A books/kestrel/arm/.sys/enco...@useless-runes.lsp
A books/kestrel/arm/.sys/instru...@useless-runes.lsp
A books/kestrel/arm/.sys/memo...@useless-runes.lsp
M books/kestrel/arm/.sys/mem...@useless-runes.lsp
M books/kestrel/arm/.sys/pseud...@useless-runes.lsp
A books/kestrel/arm/.sys/ru...@useless-runes.lsp
M books/kestrel/arm/.sys/st...@useless-runes.lsp
A books/kestrel/arm/.sys/st...@useless-runes.lsp
A books/kestrel/arm/.sys/t...@useless-runes.lsp
M books/kestrel/arm/decoder.lisp
M books/kestrel/arm/def-inst.lisp
M books/kestrel/arm/doc.lisp
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/memory.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/pseudocode.lisp
A books/kestrel/arm/rules.lisp
M books/kestrel/arm/state.lisp
A books/kestrel/arm/tests/.sys/sim...@useless-runes.lsp
M books/kestrel/arm/tests/simple.lisp
M books/kestrel/arm/top.lisp
M books/kestrel/arrays-2d/arrays-2d.lisp
M books/kestrel/arrays-2d/bv-arrays-2d.lisp
M books/kestrel/auto-termination/.sys/defunt...@useless-runes.lsp
M books/kestrel/auto-termination/README
M books/kestrel/auto-termination/defunt.lisp
M books/kestrel/auto-termination/td-cands.acl2
M books/kestrel/auto-termination/td-cands.lisp
M books/kestrel/auto-termination/termination-database-utilities.lisp
M books/kestrel/auto-termination/termination-database.lisp
M books/kestrel/axe/.sys/add-and-nor...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bitxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bitxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/add-t...@useless-runes.lsp
M books/kestrel/axe/.sys/alist-suitab...@useless-runes.lsp
M books/kestrel/axe/.sys/assumpti...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-bind-free-...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-clause...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntax-fun...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntax-...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntax...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-syntaxp-e...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-tr...@useless-runes.lsp
M books/kestrel/axe/.sys/axe-...@useless-runes.lsp
M books/kestrel/axe/.sys/bitops...@useless-runes.lsp
M books/kestrel/axe/.sys/bounded-...@useless-runes.lsp
M books/kestrel/axe/.sys/bounded-dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/bounded-d...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-array-...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-intr...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-list-...@useless-runes.lsp
M books/kestrel/axe/.sys/bv-rul...@useless-runes.lsp
M books/kestrel/axe/.sys/cars-decre...@useless-runes.lsp
M books/kestrel/axe/.sys/cars-incre...@useless-runes.lsp
M books/kestrel/axe/.sys/concretize-w...@useless-runes.lsp
M books/kestrel/axe/.sys/conjoin-te...@useless-runes.lsp
M books/kestrel/axe/.sys/conjunctions-a...@useless-runes.lsp
M books/kestrel/axe/.sys/consec...@useless-runes.lsp
M books/kestrel/axe/.sys/cont...@useless-runes.lsp
M books/kestrel/axe/.sys/cont...@useless-runes.lsp
M books/kestrel/axe/.sys/convert-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/count-b...@useless-runes.lsp
M books/kestrel/axe/.sys/crunc...@useless-runes.lsp
M books/kestrel/axe/.sys/crunc...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-arr...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-array...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-a...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-parent-ar...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-pare...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-pare...@useless-runes.lsp
A books/kestrel/axe/.sys/dag-pr...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-si...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-siz...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-to-ter...@useless-runes.lsp
M books/kestrel/axe/.sys/dag-t...@useless-runes.lsp
M books/kestrel/axe/.sys/dag...@useless-runes.lsp
M books/kestrel/axe/.sys/dag...@useless-runes.lsp
M books/kestrel/axe/.sys/da...@useless-runes.lsp
M books/kestrel/axe/.sys/da...@useless-runes.lsp
M books/kestrel/axe/.sys/darg-...@useless-runes.lsp
M books/kestrel/axe/.sys/da...@useless-runes.lsp
M books/kestrel/axe/.sys/def-simpli...@useless-runes.lsp
M books/kestrel/axe/.sys/def-sim...@useless-runes.lsp
M books/kestrel/axe/.sys/defthm-a...@useless-runes.lsp
M books/kestrel/axe/.sys/defth...@useless-runes.lsp
M books/kestrel/axe/.sys/depth...@useless-runes.lsp
M books/kestrel/axe/.sys/el...@useless-runes.lsp
M books/kestrel/axe/.sys/equality-assu...@useless-runes.lsp
M books/kestrel/axe/.sys/equality-a...@useless-runes.lsp
M books/kestrel/axe/.sys/equivalen...@useless-runes.lsp
M books/kestrel/axe/.sys/equival...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluat...@useless-runes.lsp
A books/kestrel/axe/.sys/evaluato...@useless-runes.lsp
M books/kestrel/axe/.sys/eval...@useless-runes.lsp
M books/kestrel/axe/.sys/extract-...@useless-runes.lsp
M books/kestrel/axe/.sys/find-probable...@useless-runes.lsp
M books/kestrel/axe/.sys/find-probable...@useless-runes.lsp
M books/kestrel/axe/.sys/find-prob...@useless-runes.lsp
M books/kestrel/axe/.sys/fixup-...@useless-runes.lsp
M books/kestrel/axe/.sys/get-args...@useless-runes.lsp
M books/kestrel/axe/.sys/get-di...@useless-runes.lsp
M books/kestrel/axe/.sys/hit-c...@useless-runes.lsp
M books/kestrel/axe/.sys/identical...@useless-runes.lsp
M books/kestrel/axe/.sys/instantiat...@useless-runes.lsp
M books/kestrel/axe/.sys/instant...@useless-runes.lsp
M books/kestrel/axe/.sys/keep-node...@useless-runes.lsp
M books/kestrel/axe/.sys/known-b...@useless-runes.lsp
M books/kestrel/axe/.sys/leaves-of-normal...@useless-runes.lsp
M books/kestrel/axe/.sys/leaves-of-norma...@useless-runes.lsp
M books/kestrel/axe/.sys/lifter...@useless-runes.lsp
M books/kestrel/axe/.sys/make-assum...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-bind-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-ax...@useless-runes.lsp
M books/kestrel/axe/.sys/make-ax...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-syntaxp...@useless-runes.lsp
M books/kestrel/axe/.sys/make-axe-synt...@useless-runes.lsp
M books/kestrel/axe/.sys/make-conju...@useless-runes.lsp
M books/kestrel/axe/.sys/make-dag-co...@useless-runes.lsp
M books/kestrel/axe/.sys/make-dag...@useless-runes.lsp
M books/kestrel/axe/.sys/make-dag-va...@useless-runes.lsp
M books/kestrel/axe/.sys/make-equ...@useless-runes.lsp
M books/kestrel/axe/.sys/make-ev...@useless-runes.lsp
M books/kestrel/axe/.sys/make-impli...@useless-runes.lsp
M books/kestrel/axe/.sys/make-node-rep...@useless-runes.lsp
M books/kestrel/axe/.sys/make-prov...@useless-runes.lsp
M books/kestrel/axe/.sys/make-rewri...@useless-runes.lsp
M books/kestrel/axe/.sys/make-subcor-var-an...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-in...@useless-runes.lsp
M books/kestrel/axe/.sys/make-term-in...@useless-runes.lsp
M books/kestrel/axe/.sys/match-hyp-with-node...@useless-runes.lsp
M books/kestrel/axe/.sys/memoi...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-dag-in...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-greater-tha...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-less-than...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-nodes-i...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-sort-le...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-term-into...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-term-into-...@useless-runes.lsp
M books/kestrel/axe/.sys/merge-tree-into...@useless-runes.lsp
M books/kestrel/axe/.sys/node...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replacement-...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replac...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replac...@useless-runes.lsp
M books/kestrel/axe/.sys/node-replac...@useless-runes.lsp
M books/kestrel/axe/.sys/normali...@useless-runes.lsp
M books/kestrel/axe/.sys/numeri...@useless-runes.lsp
M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
M books/kestrel/axe/.sys/prove-w...@useless-runes.lsp
M books/kestrel/axe/.sys/prover...@useless-runes.lsp
M books/kestrel/axe/.sys/prover...@useless-runes.lsp
M books/kestrel/axe/.sys/prover-st...@useless-runes.lsp
M books/kestrel/axe/.sys/pro...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-dag-a...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-dag...@useless-runes.lsp
M books/kestrel/axe/.sys/prune...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-with-c...@useless-runes.lsp
M books/kestrel/axe/.sys/prune-wit...@useless-runes.lsp
M books/kestrel/axe/.sys/pure-da...@useless-runes.lsp
M books/kestrel/axe/.sys/pure...@useless-runes.lsp
M books/kestrel/axe/.sys/rationa...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuild-...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuild...@useless-runes.lsp
M books/kestrel/axe/.sys/rebuil...@useless-runes.lsp
M books/kestrel/axe/.sys/refine-as...@useless-runes.lsp
M books/kestrel/axe/.sys/refined-assum...@useless-runes.lsp
M books/kestrel/axe/.sys/refined-assum...@useless-runes.lsp
M books/kestrel/axe/.sys/refined-assu...@useless-runes.lsp
M books/kestrel/axe/.sys/remove-duplicates...@useless-runes.lsp
M books/kestrel/axe/.sys/remov...@useless-runes.lsp
M books/kestrel/axe/.sys/renamin...@useless-runes.lsp
M books/kestrel/axe/.sys/renumber...@useless-runes.lsp
M books/kestrel/axe/.sys/replac...@useless-runes.lsp
M books/kestrel/axe/.sys/replace-usin...@useless-runes.lsp
M books/kestrel/axe/.sys/replace-...@useless-runes.lsp
M books/kestrel/axe/.sys/result...@useless-runes.lsp
M books/kestrel/axe/.sys/result-ar...@useless-runes.lsp
M books/kestrel/axe/.sys/result...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/.sys/rewriter-...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/.sys/rewriter-...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewrite...@useless-runes.lsp
M books/kestrel/axe/.sys/rewriter...@useless-runes.lsp
M books/kestrel/axe/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/.sys/rul...@useless-runes.lsp
M books/kestrel/axe/.sys/rul...@useless-runes.lsp
M books/kestrel/axe/.sys/speci...@useless-runes.lsp
M books/kestrel/axe/.sys/spli...@useless-runes.lsp
M books/kestrel/axe/.sys/stored...@useless-runes.lsp
M books/kestrel/axe/.sys/stp-clause...@useless-runes.lsp
M books/kestrel/axe/.sys/stp-count...@useless-runes.lsp
M books/kestrel/axe/.sys/sublis-var-a...@useless-runes.lsp
M books/kestrel/axe/.sys/sublis-va...@useless-runes.lsp
M books/kestrel/axe/.sys/substitu...@useless-runes.lsp
M books/kestrel/axe/.sys/substit...@useless-runes.lsp
M books/kestrel/axe/.sys/supporti...@useless-runes.lsp
M books/kestrel/axe/.sys/support...@useless-runes.lsp
M books/kestrel/axe/.sys/sweep-and-m...@useless-runes.lsp
M books/kestrel/axe/.sys/tactic...@useless-runes.lsp
M books/kestrel/axe/.sys/term-eq...@useless-runes.lsp
M books/kestrel/axe/.sys/test-...@useless-runes.lsp
M books/kestrel/axe/.sys/translate-...@useless-runes.lsp
M books/kestrel/axe/.sys/translat...@useless-runes.lsp
M books/kestrel/axe/.sys/trim-intro...@useless-runes.lsp
M books/kestrel/axe/.sys/type-in...@useless-runes.lsp
M books/kestrel/axe/.sys/unguarde...@useless-runes.lsp
M books/kestrel/axe/.sys/unguarde...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-and-...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-term-and...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-ter...@useless-runes.lsp
M books/kestrel/axe/.sys/unify-tre...@useless-runes.lsp
M books/kestrel/axe/.sys/unroll-s...@useless-runes.lsp
M books/kestrel/axe/.sys/wf-...@useless-runes.lsp
M books/kestrel/axe/.sys/worklis...@useless-runes.lsp
M books/kestrel/axe/README.md
M books/kestrel/axe/add-and-normalize-expr.lisp
M books/kestrel/axe/add-bvxor-nest-to-dag-array-with-name.lisp
M books/kestrel/axe/add-bvxor-nest-to-dag-array.lisp
M books/kestrel/axe/alist-suitable-for-hypsp.lisp
A books/kestrel/axe/arm/.sys/assum...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/axe-...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/d...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/eval...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/portc...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/rewr...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/rule-...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/run-unti...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/sup...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/syntaxp-...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/t...@useless-runes.lsp
A books/kestrel/axe/arm/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/arm/README.md
M books/kestrel/axe/arm/acl2-customization.lsp
M books/kestrel/axe/arm/assumptions.lisp
A books/kestrel/axe/arm/doc.acl2
A books/kestrel/axe/arm/doc.lisp
M books/kestrel/axe/arm/evaluator.lisp
A books/kestrel/axe/arm/examples/add/.sys/add-with...@useless-runes.lsp
A books/kestrel/axe/arm/examples/add/.sys/a...@useless-runes.lsp
M books/kestrel/axe/arm/examples/add/add-with-stop-pcs.lisp
M books/kestrel/axe/arm/examples/add/add.lisp
M books/kestrel/axe/arm/package.lsp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/run-until-return.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/assumption-array.lisp
M books/kestrel/axe/axe-clause-utilities.lisp
M books/kestrel/axe/axe-rules-mixed.lisp
M books/kestrel/axe/axe-rules.lisp
M books/kestrel/axe/axe-syntax-functions.lisp
M books/kestrel/axe/axe-syntax.lisp
M books/kestrel/axe/axe-trees.lisp
M books/kestrel/axe/axe-types.lisp
M books/kestrel/axe/basic-rules.lisp
M books/kestrel/axe/bounded-dag-parent-arrayp.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/bv-array-rules.lisp
M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/bv-list-rules-axe.lisp
M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/bv-rules-axe0.lisp
M books/kestrel/axe/call-axe-script.lisp
M books/kestrel/axe/callstp.bash
M books/kestrel/axe/cars-decreasing-by-1.lisp
M books/kestrel/axe/concretize-with-contexts.lisp
M books/kestrel/axe/conjoin-term-with-dag.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/contexts2.lisp
M books/kestrel/axe/convert-to-bv-rules-axe.lisp
M books/kestrel/axe/count-branches.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-array-builders3.lisp
M books/kestrel/axe/dag-array-printing.lisp
M books/kestrel/axe/dag-array-printing2.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-conjuncts.lisp
M books/kestrel/axe/dag-constant-alist.lisp
M books/kestrel/axe/dag-exprs.lisp
M books/kestrel/axe/dag-info.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-arrayp.lisp
A books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/dag-size-array.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-stobj.lisp
M books/kestrel/axe/dag-tests.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dag-variable-alist.lisp
M books/kestrel/axe/dagify.lisp
M books/kestrel/axe/dagify0.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/dags2.lisp
M books/kestrel/axe/def-dag-builder-theorems.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/defthm-axe-basic-tests.lisp
M books/kestrel/axe/defthm-axe.lisp
M books/kestrel/axe/defthm-stp-tests.lisp
M books/kestrel/axe/depth-array.lisp
M books/kestrel/axe/doc.lisp
M books/kestrel/axe/elim.lisp
M books/kestrel/axe/equality-assumption-alists.lisp
M books/kestrel/axe/equality-assumptions.lisp
M books/kestrel/axe/equivalence-checker-helpers.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/equivs.lisp
M books/kestrel/axe/evaluate-test-case-simple.lisp
M books/kestrel/axe/evaluate-test-case.lisp
M books/kestrel/axe/evaluator-basic.lisp
M books/kestrel/axe/evaluator-support.lisp
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/examples/.sys/aes-blas...@useless-runes.lsp
M books/kestrel/axe/examples/aes-blast-boolean.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/fixup-context.lisp
M books/kestrel/axe/get-disjuncts.lisp
M books/kestrel/axe/hit-counts.lisp
M books/kestrel/axe/identical-xor-nests.lisp
M books/kestrel/axe/implementation-notes.txt
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/interpreted-function-alistp.lisp
M books/kestrel/axe/interpreted-function-alists.lisp
M books/kestrel/axe/jvm/.sys/axe-bind-free...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/axe-syntaxp-...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/evalua...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/jvm-rul...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/jvm-ru...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lifter-u...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lifter-u...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lifter-u...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/lif...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/nice-output...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/symbolic-exe...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/tes...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/unrolle...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/jvm/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/jvm/axe-syntax-functions-jvm.lisp
M books/kestrel/axe/jvm/axe-syntax-functions-jvm2.lisp
M books/kestrel/axe/jvm/evaluator-jvm.lisp
M books/kestrel/axe/jvm/lifter-utilities.lisp
M books/kestrel/axe/jvm/lifter-utilities2.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/symbolic-execution-rules.lisp
M books/kestrel/axe/jvm/tester.lisp
M books/kestrel/axe/jvm/top.lisp
M books/kestrel/axe/jvm/unroller-common.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/known-booleans.lisp
M books/kestrel/axe/leaves-of-normalized-bvxor-nest.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/list-rules-axe.lisp
M books/kestrel/axe/logops-rules-axe.lisp
M books/kestrel/axe/make-assumption-array.lisp
M books/kestrel/axe/make-axe-rules.lisp
M books/kestrel/axe/make-axe-rules2.lisp
M books/kestrel/axe/make-axe-syntaxp-evaluator.lisp
M books/kestrel/axe/make-conjunction-dag.lisp
M books/kestrel/axe/make-dag-indices.lisp
M books/kestrel/axe/make-equality-dag-basic.lisp
M books/kestrel/axe/make-equality-dag-gen.lisp
M books/kestrel/axe/make-equality-dag.lisp
M books/kestrel/axe/make-evaluator-simple.lisp
M books/kestrel/axe/make-evaluator-tests.lisp
M books/kestrel/axe/make-evaluator.lisp
M books/kestrel/axe/make-implication-dag.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/make-term-into-dag-basic.lisp
M books/kestrel/axe/match-hyp-with-nodenum-to-assume-false.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-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/packbv-axe.lisp
A books/kestrel/axe/pre-stp-rules.lisp
M books/kestrel/axe/prove-equal-with-axe-tests.lisp
M books/kestrel/axe/prove-with-stp-tester.lisp
M books/kestrel/axe/prove-with-stp-tests.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/prover2.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/prune-term.lisp
M books/kestrel/axe/prune-with-contexts-tests.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/pure-dags.lisp
M books/kestrel/axe/query.lisp
M books/kestrel/axe/r1cs/.sys/axe-evalu...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-pro...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-rul...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/axe-syntaxp-e...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/lift-r1...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/lift...@useless-runes.lsp
M books/kestrel/axe/r1cs/.sys/verif...@useless-runes.lsp
A books/kestrel/axe/r1cs/README.md
M books/kestrel/axe/r1cs/axe-prover-r1cs.lisp
M books/kestrel/axe/r1cs/axe-rules-r1cs.lisp
M books/kestrel/axe/r1cs/lift-r1cs-common.lisp
M books/kestrel/axe/r1cs/lift-r1cs.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/refined-assumption-alists.lisp
M books/kestrel/axe/refined-assumption-alists3.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/result-alist.lisp
M books/kestrel/axe/result-array-stobj.lisp
M books/kestrel/axe/rewrite-stobj2.lisp
M books/kestrel/axe/rewriter-alt.lisp
M books/kestrel/axe/rewriter-basic-smt-tests.lisp
M books/kestrel/axe/rewriter-basic-tests.lisp
M books/kestrel/axe/rewriter-basic.lisp
M books/kestrel/axe/rewriter-common.lisp
M books/kestrel/axe/rewriter-tests.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/risc-v/.sys/clear-...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/eval...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/lifter...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/read-an...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/read-over-...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/regi...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/rewr...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/run-unti...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/sup...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/syntax-f...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/syntaxp-...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/unro...@useless-runes.lsp
M books/kestrel/axe/risc-v/.sys/write-over-...@useless-runes.lsp
M books/kestrel/axe/risc-v/README.md
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/evaluator.lisp
M books/kestrel/axe/risc-v/examples/add/.sys/add-n...@useless-runes.lsp
M books/kestrel/axe/risc-v/lifter-rules.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/registers.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-alists.lisp
M books/kestrel/axe/rule-limits.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/set-rules.lisp
M books/kestrel/axe/specialize.lisp
M books/kestrel/axe/splitting.lisp
M books/kestrel/axe/stored-rules.lisp
M books/kestrel/axe/stp-counterexamples.lisp
M books/kestrel/axe/strengthen-facts.lisp
M books/kestrel/axe/sublis-var-and-eval-basic.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/supporting-vars.lisp
M books/kestrel/axe/sweep-and-merge-support.lisp
M books/kestrel/axe/tactic-prover-tests.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/tagged-rule-sets.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/unguarded-defuns.lisp
M books/kestrel/axe/unguarded-defuns2.lisp
M books/kestrel/axe/unify-term-and-dag-fast.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
M books/kestrel/axe/wf-dagp.lisp
M books/kestrel/axe/x86/.sys/axe-syntax-f...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/bind-free-e...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/evalua...@useless-runes.lsp
A books/kestrel/axe/x86/.sys/lifter-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/loop-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/prove-eq...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/rewrit...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/rule-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/syntaxp-ev...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/tester-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/tes...@useless-runes.lsp
A books/kestrel/axe/x86/.sys/unroller-...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/unro...@useless-runes.lsp
A books/kestrel/axe/x86/.sys/with-suppo...@useless-runes.lsp
M books/kestrel/axe/x86/.sys/x86-...@useless-runes.lsp
M books/kestrel/axe/x86/README.md
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/lifter-support.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/prove-equivalence.lisp
M books/kestrel/axe/x86/rule-lists.acl2
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester-code-only.lisp
M books/kestrel/axe/x86/tester-rules-bv.lisp
M books/kestrel/axe/x86/tester-rules.acl2
M books/kestrel/axe/x86/tester-rules.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/axe/x86/x86-rules.acl2
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/bibtex/.sys/xdoc-ge...@useless-runes.lsp
M books/kestrel/bibtex/xdoc-generation.lisp
M books/kestrel/big-data/packages.lisp
M books/kestrel/bitcoin/base58.lisp
M books/kestrel/bitcoin/bech32.lisp
M books/kestrel/bitcoin/bip32.lisp
M books/kestrel/bitcoin/bip39.lisp
M books/kestrel/booleans/booland.lisp
M books/kestrel/booleans/booleans.lisp
M books/kestrel/booleans/booleans2.lisp
M books/kestrel/booleans/boolif.lisp
M books/kestrel/booleans/boolor.lisp
M books/kestrel/booleans/boolxor.lisp
M books/kestrel/booleans/iff.lisp
M books/kestrel/built-ins/collect.lisp
M books/kestrel/built-ins/disable.lisp
A books/kestrel/bv-arrays/append-arrays.lisp
A books/kestrel/bv-arrays/array-of-zeros.lisp
A books/kestrel/bv-arrays/array-patterns.lisp
A books/kestrel/bv-arrays/bv-array-clear-range.lisp
A books/kestrel/bv-arrays/bv-array-clear.lisp
A books/kestrel/bv-arrays/bv-array-conversions-gen.lisp
A books/kestrel/bv-arrays/bv-array-conversions.lisp
A books/kestrel/bv-arrays/bv-array-conversions2-tests.lisp
A books/kestrel/bv-arrays/bv-array-conversions2.lisp
A books/kestrel/bv-arrays/bv-array-if.lisp
A books/kestrel/bv-arrays/bv-array-read-chunk-little.lisp
A books/kestrel/bv-arrays/bv-array-read-rules.lisp
A books/kestrel/bv-arrays/bv-array-read.lisp
A books/kestrel/bv-arrays/bv-array-write.lisp
A books/kestrel/bv-arrays/bv-arrayp.lisp
A books/kestrel/bv-arrays/bv-arrays.lisp
A books/kestrel/bv-arrays/tests-top.lisp
A books/kestrel/bv-arrays/top.lisp
M books/kestrel/bv-lists/.sys/all-unsign...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/append...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/array-o...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/array-p...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-con...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-c...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-ar...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-read...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-array-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arr...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-arra...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-a...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-a...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv-list-read...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvchop...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvcho...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvnot...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bv...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvxor-li...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bvxor...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/byte-f...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/bytes-t...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/getbi...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/list-p...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/logex...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-bvp...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-packbv-an...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-pack...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-p...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/map-reve...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/negated-e...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv-an...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv-little-an...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/packbv-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pack...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/pac...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/unpackb...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/unpa...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/unsigned-...@useless-runes.lsp
M books/kestrel/bv-lists/.sys/width-of-...@useless-runes.lsp
M books/kestrel/bv-lists/all-unsigned-byte-p2.lisp
R books/kestrel/bv-lists/append-arrays.lisp
R books/kestrel/bv-lists/array-of-zeros.lisp
R books/kestrel/bv-lists/array-patterns.lisp
M books/kestrel/bv-lists/bits-and-bytes-inversions-little.lisp
M books/kestrel/bv-lists/bits-and-bytes-inversions.lisp
R books/kestrel/bv-lists/bv-array-clear-range.lisp
R books/kestrel/bv-lists/bv-array-clear.lisp
R books/kestrel/bv-lists/bv-array-conversions-gen.lisp
R books/kestrel/bv-lists/bv-array-conversions.lisp
R books/kestrel/bv-lists/bv-array-conversions2-tests.lisp
R books/kestrel/bv-lists/bv-array-conversions2.lisp
R books/kestrel/bv-lists/bv-array-if.lisp
R books/kestrel/bv-lists/bv-array-read-chunk-little.lisp
R books/kestrel/bv-lists/bv-array-read-rules.lisp
R books/kestrel/bv-lists/bv-array-read.lisp
R books/kestrel/bv-lists/bv-array-write.lisp
R books/kestrel/bv-lists/bv-arrayp.lisp
R books/kestrel/bv-lists/bv-arrays.lisp
M books/kestrel/bv-lists/bv-list-read-chunk-little.lisp
M books/kestrel/bv-lists/bvchop-list.lisp
M books/kestrel/bv-lists/bvchop-list2.lisp
M books/kestrel/bv-lists/bvnot-list.lisp
M books/kestrel/bv-lists/byte-listp-def.lisp
M books/kestrel/bv-lists/bytes-to-bits-little.lisp
M books/kestrel/bv-lists/list-patterns.lisp
M books/kestrel/bv-lists/logext-list.lisp
M books/kestrel/bv-lists/map-bvplus-val.lisp
M books/kestrel/bv-lists/packbv-theorems.lisp
M books/kestrel/bv-lists/tests-top.lisp
M books/kestrel/bv-lists/top.lisp
M books/kestrel/bv-lists/unpackbv-def.lisp
M books/kestrel/bv-lists/width-of-widest-int.lisp
M books/kestrel/bv/.sys/ad...@useless-runes.lsp
M books/kestrel/bv/.sys/a...@useless-runes.lsp
M books/kestrel/bv/.sys/b...@useless-runes.lsp
M books/kestrel/bv/.sys/bit-t...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bi...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bit...@useless-runes.lsp
M books/kestrel/bv/.sys/bool-...@useless-runes.lsp
A books/kestrel/bv/.sys/bvan...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bva...@useless-runes.lsp
M books/kestrel/bv/.sys/bvcat...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvc...@useless-runes.lsp
M books/kestrel/bv/.sys/bvc...@useless-runes.lsp
M books/kestrel/bv/.sys/bvdiv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvequa...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
A books/kestrel/bv/.sys/bvmin...@useless-runes.lsp
M books/kestrel/bv/.sys/bvm...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvmult...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvp...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/bvsx-...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
A books/kestrel/bv/.sys/bvumin...@useless-runes.lsp
M books/kestrel/bv/.sys/bvum...@useless-runes.lsp
M books/kestrel/bv/.sys/bv...@useless-runes.lsp
M books/kestrel/bv/.sys/convert-t...@useless-runes.lsp
M books/kestrel/bv/.sys/de...@useless-runes.lsp
M books/kestrel/bv/.sys/getbit...@useless-runes.lsp
M books/kestrel/bv/.sys/get...@useless-runes.lsp
M books/kestrel/bv/.sys/idi...@useless-runes.lsp
M books/kestrel/bv/.sys/if-becomes...@useless-runes.lsp
M books/kestrel/bv/.sys/in...@useless-runes.lsp
M books/kestrel/bv/.sys/leftrota...@useless-runes.lsp
M books/kestrel/bv/.sys/leftro...@useless-runes.lsp
M books/kestrel/bv/.sys/leftr...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/log...@useless-runes.lsp
M books/kestrel/bv/.sys/ones-co...@useless-runes.lsp
M books/kestrel/bv/.sys/overflow-an...@useless-runes.lsp
M books/kestrel/bv/.sys/put...@useless-runes.lsp
M books/kestrel/bv/.sys/right...@useless-runes.lsp
M books/kestrel/bv/.sys/rot...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/rul...@useless-runes.lsp
M books/kestrel/bv/.sys/ru...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvdiv...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvdivdo...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvlt...@useless-runes.lsp
M books/kestrel/bv/.sys/sb...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvmo...@useless-runes.lsp
M books/kestrel/bv/.sys/sbvrem...@useless-runes.lsp
M books/kestrel/bv/.sys/sbv...@useless-runes.lsp
M books/kestrel/bv/.sys/singl...@useless-runes.lsp
M books/kestrel/bv/.sys/slice...@useless-runes.lsp
M books/kestrel/bv/.sys/sli...@useless-runes.lsp
M books/kestrel/bv/.sys/sl...@useless-runes.lsp
M books/kestrel/bv/.sys/s...@useless-runes.lsp
M books/kestrel/bv/.sys/trim-elim...@useless-runes.lsp
M books/kestrel/bv/.sys/trim-elim-r...@useless-runes.lsp
M books/kestrel/bv/.sys/trim-int...@useless-runes.lsp
M books/kestrel/bv/.sys/unsigned-byte-...@useless-runes.lsp
M books/kestrel/bv/adder.lisp
M books/kestrel/bv/arith.lisp
M books/kestrel/bv/bitand.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bitor.lisp
M books/kestrel/bv/bitwise.lisp
M books/kestrel/bv/bitxor.lisp
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/bvand.lisp
M books/kestrel/bv/bvashr-def.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-def.lisp
M books/kestrel/bv/bvmod.lisp
M books/kestrel/bv/bvmult.lisp
M books/kestrel/bv/bvnot.lisp
A books/kestrel/bv/bvor-def.lisp
M books/kestrel/bv/bvor.lisp
M books/kestrel/bv/bvplus.lisp
M books/kestrel/bv/bvsx-rules.lisp
A books/kestrel/bv/bvxor-def.lisp
M books/kestrel/bv/bvxor.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/bv/defs-bitwise.lisp
M books/kestrel/bv/floor-mod-expt.lisp
M books/kestrel/bv/getbit-rules.lisp
M books/kestrel/bv/getbit.lisp
M books/kestrel/bv/idioms.lisp
M books/kestrel/bv/if-becomes-bvif-rules.lisp
M books/kestrel/bv/intro.lisp
M books/kestrel/bv/leftrotate-rules.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/logand-b.lisp
M books/kestrel/bv/logext.lisp
M books/kestrel/bv/logtail.lisp
M books/kestrel/bv/overflow-and-underflow.lisp
M books/kestrel/bv/padding.lisp
M books/kestrel/bv/rightrotate-rules.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/rules3.lisp
M books/kestrel/bv/rules4.lisp
M books/kestrel/bv/rules6.lisp
M books/kestrel/bv/rules9.lisp
M books/kestrel/bv/sbvlt-rules.lisp
M books/kestrel/bv/single-bit.lisp
M books/kestrel/bv/slice.lisp
M books/kestrel/bv/slice2.lisp
M books/kestrel/bv/top.lisp
M books/kestrel/bv/trim-elim-rules-bv.lisp
M books/kestrel/bv/trim-elim-rules-non-bv.lisp
M books/kestrel/bv/trim-intro-rules.lisp
M books/kestrel/bv/unsigned-byte-p-forced-rules.lisp
M books/kestrel/bv/validation-smt-lib.lisp
M books/kestrel/c/atc/.sys/gener...@useless-runes.lsp
M books/kestrel/c/atc/.sys/pretty-...@useless-runes.lsp
M books/kestrel/c/atc/abstract-syntax.lisp
M books/kestrel/c/atc/defobject.lisp
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/generation-contexts.lisp
M books/kestrel/c/atc/generation.lisp
M books/kestrel/c/atc/input-processing.lisp
M books/kestrel/c/atc/let-designations.lisp
M books/kestrel/c/atc/pretty-printer.lisp
R books/kestrel/c/atc/pure-expression-execution.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/exec-expr...@useless-runes.lsp
R books/kestrel/c/atc/symbolic-execution-rules/.sys/exec...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/li...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/.sys/object-de...@useless-runes.lsp
M books/kestrel/c/atc/symbolic-execution-rules/boolean-equality.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-arrsub.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-binary-strict-pure-gen.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-cast.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-call.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-pure.lisp
R books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-unary.lisp
M books/kestrel/c/atc/symbolic-execution-rules/sint-from-boolean.lisp
R books/kestrel/c/atc/symbolic-execution-rules/syntaxp.lisp
M books/kestrel/c/atc/symbolic-execution-rules/test-value.lisp
M books/kestrel/c/atc/symbolic-execution-rules/top.lisp
M books/kestrel/c/atc/tag-generation.lisp
R books/kestrel/c/atc/test-star.lisp
M books/kestrel/c/atc/tutorial.lisp
A books/kestrel/c/examples/README.md
A books/kestrel/c/examples/add-uints.lisp
A books/kestrel/c/examples/add_uints.c
A books/kestrel/c/examples/cert.acl2
A books/kestrel/c/examples/strcpy-safe-induction.lisp
A books/kestrel/c/examples/strcpy-safe-support.lisp
A books/kestrel/c/examples/strcpy-safe.lisp
A books/kestrel/c/examples/strcpy_safe.c
M books/kestrel/c/language/.sys/abstrac...@useless-runes.lsp
M books/kestrel/c/language/.sys/computati...@useless-runes.lsp
A books/kestrel/c/language/.sys/decimal-0-...@useless-runes.lsp
M books/kestrel/c/language/.sys/frame-and-s...@useless-runes.lsp
M books/kestrel/c/language/.sys/function-e...@useless-runes.lsp
M books/kestrel/c/language/.sys/keyw...@useless-runes.lsp
A books/kestrel/c/language/.sys/punct...@useless-runes.lsp
M books/kestrel/c/language/.sys/static-s...@useless-runes.lsp
M books/kestrel/c/language/.sys/tag-envi...@useless-runes.lsp
M books/kestrel/c/language/.sys/ty...@useless-runes.lsp
M books/kestrel/c/language/.sys/val...@useless-runes.lsp
M books/kestrel/c/language/abstract-syntax.lisp
M books/kestrel/c/language/character-sets.lisp
M books/kestrel/c/language/decimal-0-to-octal-0.lisp
M books/kestrel/c/language/function-environments.lisp
M books/kestrel/c/language/implementation-environments/.sys/vers...@useless-runes.lsp
M books/kestrel/c/language/implementation-environments/bool-formats.lisp
A books/kestrel/c/language/implementation-environments/dialects.lisp
M books/kestrel/c/language/implementation-environments/integer-format-templates.lisp
M books/kestrel/c/language/implementation-environments/integer-formats.lisp
M books/kestrel/c/language/implementation-environments/schar-formats.lisp
M books/kestrel/c/language/implementation-environments/top.lisp
M books/kestrel/c/language/implementation-environments/uchar-formats.lisp
R books/kestrel/c/language/implementation-environments/versions.lisp
M books/kestrel/c/language/keywords.lisp
M books/kestrel/c/language/pointer-operations.lisp
M books/kestrel/c/language/portable-ascii-identifiers.lisp
M books/kestrel/c/language/punctuators.lisp
M books/kestrel/c/language/static-semantics.lisp
M books/kestrel/c/package.lsp
A books/kestrel/c/proof-support/.sys/const-ast...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/const-...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/exec-stm...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/exec-stmt-w...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/pure-express...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/test...@useless-runes.lsp
A books/kestrel/c/proof-support/.sys/t...@useless-runes.lsp
A books/kestrel/c/proof-support/acl2-customization.lsp
A books/kestrel/c/proof-support/const-ast-accessors.lisp
A books/kestrel/c/proof-support/const-folding.lisp
A books/kestrel/c/proof-support/exec-expr-pure-list-openers.lisp
A books/kestrel/c/proof-support/exec-expr-pure-openers.lisp
A books/kestrel/c/proof-support/exec-stmt-openers.lisp
A books/kestrel/c/proof-support/exec-stmt-while-openers.lisp
A books/kestrel/c/proof-support/pure-expression-execution.lisp
A books/kestrel/c/proof-support/syntaxp-for-expr-pure.lisp
A books/kestrel/c/proof-support/test-star.lisp
A books/kestrel/c/proof-support/top.lisp
M books/kestrel/c/syntax/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-syn...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-synt...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/abstract-s...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/ascii-id...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/code-en...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/disamb...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/external-pr...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/fi...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/forma...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/gra...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/implementatio...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/infer...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/input...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/langdef-map...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/langdef...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/le...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/macro-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/output...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/parser-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/parser...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/par...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/posi...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preprocesso...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preprocess...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/prepro...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/preservable...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/pri...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/pur...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/rea...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/sp...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/stan...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/string...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/token-con...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/unamb...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/unicode-c...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/validation-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/vali...@useless-runes.lsp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
A books/kestrel/c/syntax/abstract-syntax-structurals.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/abstract-syntax.lisp
M books/kestrel/c/syntax/abstraction-mapping.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
A books/kestrel/c/syntax/built-in.lisp
R books/kestrel/c/syntax/builtin.lisp
M books/kestrel/c/syntax/code-ensembles.lisp
M books/kestrel/c/syntax/compilation-db.lisp
M books/kestrel/c/syntax/concrete-syntax.lisp
M books/kestrel/c/syntax/disambiguator.lisp
A books/kestrel/c/syntax/evaluation.lisp
M books/kestrel/c/syntax/external-preprocessing.lisp
M books/kestrel/c/syntax/file-paths.lisp
M books/kestrel/c/syntax/files.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/grammar-characters.lisp
A books/kestrel/c/syntax/grammar-operations.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/.gitattributes
R books/kestrel/c/syntax/grammar/all.abnf
A books/kestrel/c/syntax/grammar/character-constants-c17.abnf
A books/kestrel/c/syntax/grammar/character-constants-c23.abnf
A books/kestrel/c/syntax/grammar/character-constants.abnf
A books/kestrel/c/syntax/grammar/characters-c17.abnf
A books/kestrel/c/syntax/grammar/characters-c23.abnf
A books/kestrel/c/syntax/grammar/characters.abnf
A books/kestrel/c/syntax/grammar/comments.abnf
A books/kestrel/c/syntax/grammar/constants-c17.abnf
A books/kestrel/c/syntax/grammar/constants-c23.abnf
A books/kestrel/c/syntax/grammar/encoding-prefixes.abnf
A books/kestrel/c/syntax/grammar/enumeration-constants.abnf
A books/kestrel/c/syntax/grammar/floating-constants-c17-gcc.abnf
A books/kestrel/c/syntax/grammar/floating-constants-c17-nogcc.abnf
A books/kestrel/c/syntax/grammar/floating-constants-c17.abnf
A books/kestrel/c/syntax/grammar/floating-constants-c23-gcc.abnf
A books/kestrel/c/syntax/grammar/floating-constants-c23-nogcc.abnf
A books/kestrel/c/syntax/grammar/floating-constants-c23.abnf
A books/kestrel/c/syntax/grammar/floating-constants.abnf
A books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/header-names.abnf
A books/kestrel/c/syntax/grammar/identifiers-c17.abnf
A books/kestrel/c/syntax/grammar/identifiers-c23.abnf
A books/kestrel/c/syntax/grammar/identifiers.abnf
A books/kestrel/c/syntax/grammar/integer-constants-c17.abnf
A books/kestrel/c/syntax/grammar/integer-constants-c23.abnf
A books/kestrel/c/syntax/grammar/integer-constants.abnf
A books/kestrel/c/syntax/grammar/keywords-c17-clang-cheri.abnf
A books/kestrel/c/syntax/grammar/keywords-c17-clang.abnf
A books/kestrel/c/syntax/grammar/keywords-c17-gcc.abnf
A books/kestrel/c/syntax/grammar/keywords-c17.abnf
A books/kestrel/c/syntax/grammar/keywords-c23-clang-cheri.abnf
A books/kestrel/c/syntax/grammar/keywords-c23-clang.abnf
A books/kestrel/c/syntax/grammar/keywords-c23-gcc.abnf
A books/kestrel/c/syntax/grammar/keywords-c23.abnf
A books/kestrel/c/syntax/grammar/keywords.abnf
A books/kestrel/c/syntax/grammar/preprocessing-lexemes.abnf
A books/kestrel/c/syntax/grammar/preprocessing-numbers-c17.abnf
A books/kestrel/c/syntax/grammar/preprocessing-numbers-c23.abnf
A books/kestrel/c/syntax/grammar/preprocessing-tokens-c17.abnf
A books/kestrel/c/syntax/grammar/preprocessing-tokens-c23.abnf
A books/kestrel/c/syntax/grammar/punctuators-c17.abnf
A books/kestrel/c/syntax/grammar/punctuators-c23.abnf
A books/kestrel/c/syntax/grammar/simple-escapes-ext.abnf
A books/kestrel/c/syntax/grammar/simple-escapes-std.abnf
A books/kestrel/c/syntax/grammar/string-literals-c17.abnf
A books/kestrel/c/syntax/grammar/string-literals-c23.abnf
A books/kestrel/c/syntax/grammar/universal-character-names.abnf
A books/kestrel/c/syntax/hash-conditional-evaluation.lisp
M books/kestrel/c/syntax/ienv.c
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/infer-ienv.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/lexer.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/output-files-doc.lisp
M books/kestrel/c/syntax/output-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/parser-messages.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
A books/kestrel/c/syntax/positions.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-files.lisp
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-options.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/preservable-inclusions.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/reader.lisp
A books/kestrel/c/syntax/spans.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/stringization.lisp
A books/kestrel/c/syntax/tests/.sys/preprocessor-...@useless-runes.lsp
M books/kestrel/c/syntax/tests/.sys/prepro...@useless-runes.lsp
A books/kestrel/c/syntax/tests/.sys/ty...@useless-runes.lsp
M books/kestrel/c/syntax/tests/.sys/vali...@useless-runes.lsp
M books/kestrel/c/syntax/tests/compilation-db.lisp
A books/kestrel/c/syntax/tests/disamb-example1/included.c
A books/kestrel/c/syntax/tests/disamb-example1/including.c
A books/kestrel/c/syntax/tests/disamb-example2/guarded-included.h
A books/kestrel/c/syntax/tests/disamb-example2/including.c
A books/kestrel/c/syntax/tests/disamb-example2/including1.c
A books/kestrel/c/syntax/tests/disamb-example2/including2.c
A books/kestrel/c/syntax/tests/disambiguator-trans-ensembles.lisp
A books/kestrel/c/syntax/tests/disambiguator-trans-units.lisp
R books/kestrel/c/syntax/tests/disambiguator.lisp
M books/kestrel/c/syntax/tests/input-files.lisp
M books/kestrel/c/syntax/tests/lexer.lisp
M books/kestrel/c/syntax/tests/output-files.lisp
M books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/parser.lisp
M books/kestrel/c/syntax/tests/preprocess-file.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
M books/kestrel/c/syntax/tests/reader.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/token-concatenation.lisp
M books/kestrel/c/syntax/top.lisp
A books/kestrel/c/syntax/translation-unit-comparison.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/top.lisp
A books/kestrel/c/transformation/.sys/add-sectio...@useless-runes.lsp
A books/kestrel/c/transformation/.sys/add-sect...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/constant-p...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/cop...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/proof-ge...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/ren...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/simp...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/speci...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/split-...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/split-...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/spli...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/spli...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/variables-in-co...@useless-runes.lsp
M books/kestrel/c/transformation/.sys/wra...@useless-runes.lsp
M books/kestrel/c/transformation/add-section-attr.lisp
M books/kestrel/c/transformation/command-line/.sys/wrap...@useless-runes.lsp
A books/kestrel/c/transformation/command-line/tests/do-nothing.json
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/rename.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize-doc.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso-doc.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso-doc.lisp
M books/kestrel/c/transformation/split-gso.lisp
A books/kestrel/c/transformation/tests/add-section-attr/.sys/add-sect...@useless-runes.lsp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
M books/kestrel/c/transformation/tests/call-graph/call-graph.lisp
M books/kestrel/c/transformation/tests/copy-fn/copy-fn.lisp
M books/kestrel/c/transformation/tests/free-vars/.sys/free...@useless-runes.lsp
M books/kestrel/c/transformation/tests/free-vars/free-vars.lisp
M books/kestrel/c/transformation/tests/simpadd0/.sys/asg...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/asg-...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/b...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/blo...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/ca...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/cons...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/de...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/dow...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/g...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/glo...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/i...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/ife...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/log...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/lo...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/nonint...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/pa...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/pure-ex...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/retur...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/stmt...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/terna...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/un...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/vari...@useless-runes.lsp
M books/kestrel/c/transformation/tests/simpadd0/.sys/wh...@useless-runes.lsp
M books/kestrel/c/transformation/tests/split-gso/extern-struct.c
A books/kestrel/c/transformation/tests/split-gso/extern-struct2.c
A books/kestrel/c/transformation/tests/split-gso/implicit-initer.c
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp
M books/kestrel/c/transformation/tests/split-gso/static-struct2.c
A books/kestrel/c/transformation/tests/split-gso/unnamed-members.c
M books/kestrel/c/transformation/tests/subst-free/.sys/subst...@useless-runes.lsp
M books/kestrel/c/transformation/tests/subst-free/subst-free.lisp
A books/kestrel/c/transformation/utilities/.sys/add-att...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/call-...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/collect...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/free...@useless-runes.lsp
A books/kestrel/c/transformation/utilities/.sys/qualifi...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/.sys/subst...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp
M books/kestrel/c/transformation/utilities/fresh-ident.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn-doc.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
M books/kestrel/clause-processors/.sys/clause-to-...@useless-runes.lsp
M books/kestrel/clause-processors/.sys/handle-const...@useless-runes.lsp
M books/kestrel/clause-processors/.sys/simple-su...@useless-runes.lsp
M books/kestrel/clause-processors/do-nothing-to-literals.lisp
M books/kestrel/clause-processors/push-unary-fns.lisp
M books/kestrel/clause-processors/simple-subsumption.lisp
M books/kestrel/clause-processors/subst-flag.lisp
M books/kestrel/crypto/aes/.sys/aes-...@useless-runes.lsp
M books/kestrel/crypto/attachments/.sys/kecca...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake-25...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blak...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake2...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/bla...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake2s-exten...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/blake2...@useless-runes.lsp
M books/kestrel/crypto/blake/.sys/bla...@useless-runes.lsp
M books/kestrel/crypto/chacha/.sys/chac...@useless-runes.lsp
M books/kestrel/crypto/ecdsa/.sys/deterministic-...@useless-runes.lsp
M books/kestrel/crypto/ecurve/.sys/secp256k1-dom...@useless-runes.lsp
M books/kestrel/crypto/ecurve/prime-field-intro.lisp
M books/kestrel/crypto/interfaces/definterface-hmac.lisp
M books/kestrel/crypto/kdf/doc.lisp
M books/kestrel/crypto/keccak/.sys/keccak-t...@useless-runes.lsp
M books/kestrel/crypto/keccak/.sys/kec...@useless-runes.lsp
M books/kestrel/crypto/keccak/keccak.lisp
M books/kestrel/crypto/padding/.sys/pad-t...@useless-runes.lsp
M books/kestrel/crypto/padding/.sys/pad-t...@useless-runes.lsp
M books/kestrel/crypto/padding/doc.lisp
M books/kestrel/crypto/primes/.sys/baby-jubjub-s...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/bls12-3...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/bn-254-gr...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/ed25519-b...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/ed25519-g...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/goldilocks-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/jubjub-sub...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/koala...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/nist-p-256...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/nist-p-256-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/secp256k1-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/secp256k1-...@useless-runes.lsp
M books/kestrel/crypto/primes/.sys/t...@useless-runes.lsp
M books/kestrel/crypto/primes/nist-p-256-base-prime.lisp
M books/kestrel/crypto/primes/nist-p-256-group-prime.lisp
M books/kestrel/crypto/r1cs/.sys/gad...@useless-runes.lsp
M books/kestrel/crypto/r1cs/dense/.sys/example...@useless-runes.lsp
M books/kestrel/crypto/r1cs/dense/r1cs.lisp
M books/kestrel/crypto/r1cs/gadgets/.sys/xor-...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/.sys/p1...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/.sys/rule...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/doc.lisp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/bit...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/na...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/range...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/.sys/x...@useless-runes.lsp
M books/kestrel/crypto/r1cs/sparse/gadgets/range-check.lisp
M books/kestrel/crypto/r1cs/sparse/r1cs.lisp
M books/kestrel/crypto/salsa/.sys/salsa2...@useless-runes.lsp
M books/kestrel/crypto/salsa/.sys/sal...@useless-runes.lsp
M books/kestrel/crypto/salsa/salsa20.lisp
M books/kestrel/crypto/sha-2/sha-256.lisp
M books/kestrel/crypto/sha-2/sha-512.lisp
M books/kestrel/crypto/sha-3/.sys/sha-3-va...@useless-runes.lsp
M books/kestrel/crypto/sha-3/.sys/sh...@useless-runes.lsp
M books/kestrel/crypto/sha-3/.sys/sup...@useless-runes.lsp
M books/kestrel/crypto/sha-3/sha-3-validation.lisp
M books/kestrel/crypto/sha-3/sha-3.lisp
M books/kestrel/crypto/tea/.sys/inve...@useless-runes.lsp
M books/kestrel/crypto/tea/.sys/t...@useless-runes.lsp
M books/kestrel/crypto/tea/inversion.lisp
M books/kestrel/crypto/tea/tea.lisp
M books/kestrel/csv/csv.lisp
M books/kestrel/csv/parse-csv.lisp
A books/kestrel/data/.sys/d...@useless-runes.lsp
M books/kestrel/data/doc.lisp
M books/kestrel/data/hash/.sys/jen...@useless-runes.lsp
M books/kestrel/data/hash/jenkins.lisp
M books/kestrel/data/top.lisp
A books/kestrel/data/treemap/acl2-customization.lsp
A books/kestrel/data/treemap/cert.acl2
A books/kestrel/data/treemap/defs.lisp
A books/kestrel/data/treemap/delete-defs.lisp
A books/kestrel/data/treemap/delete.lisp
A books/kestrel/data/treemap/doc.lisp
A books/kestrel/data/treemap/extensionality.lisp
A books/kestrel/data/treemap/in-defs.lisp
A books/kestrel/data/treemap/in.lisp
A books/kestrel/data/treemap/internal/acl2-customization.lsp
A books/kestrel/data/treemap/internal/antisymmetry.lisp
A books/kestrel/data/treemap/internal/bst-defs.lisp
A books/kestrel/data/treemap/internal/bst.lisp
A books/kestrel/data/treemap/internal/cert.acl2
A books/kestrel/data/treemap/internal/count-defs.lisp
A books/kestrel/data/treemap/internal/count.lisp
A books/kestrel/data/treemap/internal/delete-defs.lisp
A books/kestrel/data/treemap/internal/delete.lisp
A books/kestrel/data/treemap/internal/doc.lisp
A books/kestrel/data/treemap/internal/heap-defs.lisp
A books/kestrel/data/treemap/internal/heap.lisp
A books/kestrel/data/treemap/internal/in-order-defs.lisp
A books/kestrel/data/treemap/internal/in-order.lisp
A books/kestrel/data/treemap/internal/join-defs.lisp
A books/kestrel/data/treemap/internal/join.lisp
A books/kestrel/data/treemap/internal/keys-defs.lisp
A books/kestrel/data/treemap/internal/keys.lisp
A books/kestrel/data/treemap/internal/lookup-defs.lisp
A books/kestrel/data/treemap/internal/lookup.lisp
A books/kestrel/data/treemap/internal/min-max-defs.lisp
A books/kestrel/data/treemap/internal/min-max.lisp
A books/kestrel/data/treemap/internal/restrict-defs.lisp
A books/kestrel/data/treemap/internal/restrict.lisp
A books/kestrel/data/treemap/internal/rlookup-defs.lisp
A books/kestrel/data/treemap/internal/rlookup.lisp
A books/kestrel/data/treemap/internal/rotate-defs.lisp
A books/kestrel/data/treemap/internal/rotate.lisp
A books/kestrel/data/treemap/internal/split-defs.lisp
A books/kestrel/data/treemap/internal/split.lisp
A books/kestrel/data/treemap/internal/submap-defs.lisp
A books/kestrel/data/treemap/internal/submap.lisp
A books/kestrel/data/treemap/internal/tree-defs.lisp
A books/kestrel/data/treemap/internal/tree.lisp
A books/kestrel/data/treemap/internal/update-defs.lisp
A books/kestrel/data/treemap/internal/update-star-defs.lisp
A books/kestrel/data/treemap/internal/update-star.lisp
A books/kestrel/data/treemap/internal/update.lisp
A books/kestrel/data/treemap/internal/values-defs.lisp
A books/kestrel/data/treemap/internal/values.lisp
A books/kestrel/data/treemap/keys-defs.lisp
A books/kestrel/data/treemap/keys.lisp
A books/kestrel/data/treemap/lookup-defs.lisp
A books/kestrel/data/treemap/lookup.lisp
A books/kestrel/data/treemap/map-defs.lisp
A books/kestrel/data/treemap/map.lisp
A books/kestrel/data/treemap/min-max-defs.lisp
A books/kestrel/data/treemap/min-max.lisp
A books/kestrel/data/treemap/package.lsp
A books/kestrel/data/treemap/portcullis.acl2
A books/kestrel/data/treemap/portcullis.lisp
A books/kestrel/data/treemap/restrict-defs.lisp
A books/kestrel/data/treemap/restrict.lisp
A books/kestrel/data/treemap/rlookup-defs.lisp
A books/kestrel/data/treemap/rlookup.lisp
A books/kestrel/data/treemap/size-defs.lisp
A books/kestrel/data/treemap/size.lisp
A books/kestrel/data/treemap/submap-defs.lisp
A books/kestrel/data/treemap/submap.lisp
A books/kestrel/data/treemap/to-omap-defs.lisp
A books/kestrel/data/treemap/to-omap.lisp
A books/kestrel/data/treemap/top.lisp
A books/kestrel/data/treemap/update-defs.lisp
A books/kestrel/data/treemap/update-star-defs.lisp
A books/kestrel/data/treemap/update-star.lisp
A books/kestrel/data/treemap/update.lisp
A books/kestrel/data/treemap/values-defs.lisp
A books/kestrel/data/treemap/values.lisp
M books/kestrel/data/treeset/.sys/del...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/d...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/i...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/ins...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/inte...@useless-runes.lsp
M books/kestrel/data/treeset/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treeset/benchmark/.sys/ran...@useless-runes.lsp
M books/kestrel/data/treeset/delete.lisp
M books/kestrel/data/treeset/diff.lisp
M books/kestrel/data/treeset/doc.lisp
M books/kestrel/data/treeset/extensionality.lisp
M books/kestrel/data/treeset/generic-typed.lisp
M books/kestrel/data/treeset/in.lisp
M books/kestrel/data/treeset/insert.lisp
M books/kestrel/data/treeset/internal/.sys/antisy...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/co...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/del...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/d...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/heap-...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/he...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/in-o...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/i...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/ins...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/inte...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/it...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/min...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/rot...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/sp...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/sub...@useless-runes.lsp
M books/kestrel/data/treeset/internal/.sys/un...@useless-runes.lsp
M books/kestrel/data/treeset/internal/antisymmetry.lisp
M books/kestrel/data/treeset/internal/bst.lisp
M books/kestrel/data/treeset/internal/delete.lisp
M books/kestrel/data/treeset/internal/diff.lisp
M books/kestrel/data/treeset/internal/doc.lisp
M books/kestrel/data/treeset/internal/heap-defs.lisp
M books/kestrel/data/treeset/internal/heap-order.lisp
M books/kestrel/data/treeset/internal/heap.lisp
M books/kestrel/data/treeset/internal/in-order-defs.lisp
M books/kestrel/data/treeset/internal/in-order.lisp
M books/kestrel/data/treeset/internal/in.lisp
M books/kestrel/data/treeset/internal/insert-defs.lisp
M books/kestrel/data/treeset/internal/insert.lisp
M books/kestrel/data/treeset/internal/intersect.lisp
M books/kestrel/data/treeset/internal/iter.lisp
M books/kestrel/data/treeset/internal/join.lisp
M books/kestrel/data/treeset/internal/min-max.lisp
M books/kestrel/data/treeset/internal/rotate.lisp
M books/kestrel/data/treeset/internal/split.lisp
M books/kestrel/data/treeset/internal/subset-defs.lisp
M books/kestrel/data/treeset/internal/subset.lisp
M books/kestrel/data/treeset/internal/tree-defs.lisp
M books/kestrel/data/treeset/internal/tree.lisp
M books/kestrel/data/treeset/internal/union.lisp
M books/kestrel/data/treeset/intersect.lisp
M books/kestrel/data/treeset/iter.lisp
M books/kestrel/data/treeset/min-max.lisp
M books/kestrel/data/treeset/set.lisp
M books/kestrel/data/treeset/subset.lisp
M books/kestrel/data/treeset/to-oset.lisp
M books/kestrel/data/treeset/union.lisp
M books/kestrel/data/utilities/.sys/li...@useless-runes.lsp
R books/kestrel/data/utilities/.sys/nat-...@useless-runes.lsp
R books/kestrel/data/utilities/.sys/n...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/t...@useless-runes.lsp
A books/kestrel/data/utilities/alist.lisp
R books/kestrel/data/utilities/list-defs.lisp
R books/kestrel/data/utilities/list.lisp
A books/kestrel/data/utilities/lists/acl2-customization.lsp
A books/kestrel/data/utilities/lists/cert.acl2
A books/kestrel/data/utilities/lists/defs.lisp
A books/kestrel/data/utilities/lists/equiv.lisp
A books/kestrel/data/utilities/lists/reverse.lisp
A books/kestrel/data/utilities/omap-defs.lisp
A books/kestrel/data/utilities/omap.lisp
M books/kestrel/data/utilities/oset.lisp
M books/kestrel/data/utilities/top.lisp
M books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/min...@useless-runes.lsp
M books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
M books/kestrel/data/utilities/total-order/.sys/total...@useless-runes.lsp
M books/kestrel/error-checking/def-error-checker.lisp
M books/kestrel/error-checking/top.lisp
M books/kestrel/ethereum/.sys/data...@useless-runes.lsp
M books/kestrel/ethereum/.sys/mmp-...@useless-runes.lsp
M books/kestrel/ethereum/.sys/t...@useless-runes.lsp
M books/kestrel/ethereum/addresses.lisp
M books/kestrel/ethereum/evm/.sys/e...@useless-runes.lsp
M books/kestrel/ethereum/evm/.sys/sup...@useless-runes.lsp
M books/kestrel/ethereum/evm/evm.lisp
M books/kestrel/ethereum/hex-prefix.lisp
M books/kestrel/ethereum/mmp-trees.lisp
M books/kestrel/ethereum/rlp/decodability.lisp
M books/kestrel/ethereum/rlp/decoding-executable.lisp
M books/kestrel/ethereum/semaphore/.sys/baby-...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/blake2s-mi...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/mimcsponge...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/mimcsponge...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/mimcsponge...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/.sys/r1cs-pro...@useless-runes.lsp
M books/kestrel/ethereum/semaphore/edwards2montgomery-proof.lisp
M books/kestrel/ethereum/semaphore/montgomery2edwards-proof.lisp
M books/kestrel/ethereum/semaphore/montgomeryadd-proof.lisp
M books/kestrel/ethereum/semaphore/montgomerydouble-proof.lisp
M books/kestrel/ethereum/semaphore/multimux1-2-proof.lisp
M books/kestrel/ethereum/semaphore/multimux3-2-proof.lisp
M books/kestrel/ethereum/semaphore/r1cs-proof-rules.lisp
M books/kestrel/evaluators/defevaluator-plus-tests.lisp
M books/kestrel/evaluators/defevaluator-plus.lisp
M books/kestrel/evaluators/defevaluator-theorems.lisp
M books/kestrel/evaluators/not-eval.lisp
M books/kestrel/executable-parsers/.sys/elf-...@useless-runes.lsp
M books/kestrel/executable-parsers/.sys/parse-e...@useless-runes.lsp
M books/kestrel/executable-parsers/.sys/parse-...@useless-runes.lsp
M books/kestrel/executable-parsers/.sys/parsed-exec...@useless-runes.lsp
M books/kestrel/executable-parsers/.sys/parser...@useless-runes.lsp
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-mach-o-file.lisp
M books/kestrel/executable-parsers/parse-pe-file.lisp
M books/kestrel/executable-parsers/pe-tools.lisp
M books/kestrel/file-io-light/.sys/read-bytes-...@useless-runes.lsp
M books/kestrel/file-io-light/.sys/read-file-in...@useless-runes.lsp
M books/kestrel/file-io-light/channels.lisp
M books/kestrel/file-io-light/print-object-dollar-fn.lisp
M books/kestrel/file-io-light/print-object-dollar.lisp
M books/kestrel/file-io-light/read-byte-dollar.lisp
M books/kestrel/file-io-light/write-byte-dollar.lisp
M books/kestrel/file-io-light/write-bytes-to-channel.lisp
M books/kestrel/file-io-light/write-bytes-to-file-bang.lisp
M books/kestrel/file-io-light/write-bytes-to-file.lisp
M books/kestrel/file-io-light/write-objects-to-channel.lisp
M books/kestrel/file-io-light/write-objects-to-file-bang.lisp
M books/kestrel/file-io-light/write-objects-to-file.lisp
M books/kestrel/floats/.sys/ieee-floats...@useless-runes.lsp
M books/kestrel/floats/ieee-floats.lisp
M books/kestrel/floats/round.lisp
M books/kestrel/floats/rtl.lisp
M books/kestrel/fty/.sys/any-n...@useless-runes.lsp
A books/kestrel/fty/.sys/byte-li...@useless-runes.lsp
M books/kestrel/fty/.sys/characte...@useless-runes.lsp
M books/kestrel/fty/.sys/deffold-...@useless-runes.lsp
M books/kestrel/fty/.sys/deffo...@useless-runes.lsp
M books/kestrel/fty/.sys/deffold-re...@useless-runes.lsp
M books/kestrel/fty/.sys/deffold...@useless-runes.lsp
M books/kestrel/fty/.sys/defmake-s...@useless-runes.lsp
M books/kestrel/fty/.sys/defoma...@useless-runes.lsp
M books/kestrel/fty/.sys/string-str...@useless-runes.lsp
M books/kestrel/fty/database.lisp
M books/kestrel/fty/defbyte.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce.lisp
M books/kestrel/fty/deflist-of-len.lisp
M books/kestrel/fty/defresult.lisp
M books/kestrel/fty/dependencies.lisp
M books/kestrel/fty/fty-omap.lisp
M books/kestrel/fty/map.lisp
M books/kestrel/fty/nat-natlist-result.lisp
A books/kestrel/fty/string-string-map.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/hdwallet/README.md
M books/kestrel/hdwallet/wallet-executable.lisp
M books/kestrel/hdwallet/wallet.lisp
M books/kestrel/helpers/.sys/advice-imp...@useless-runes.lsp
A books/kestrel/helpers/.sys/defrul...@useless-runes.lsp
M books/kestrel/helpers/.sys/eval-...@useless-runes.lsp
M books/kestrel/helpers/advice-implementation.lisp
M books/kestrel/helpers/auto-return-type.lisp
M books/kestrel/helpers/deps.lisp
M books/kestrel/helpers/eval-models.lisp
M books/kestrel/helpers/improve-book-implementation.lisp
M books/kestrel/helpers/linter.lisp
M books/kestrel/helpers/model-cases.lisp
M books/kestrel/helpers/model-enable.lisp
M books/kestrel/helpers/model-history.lisp
M books/kestrel/helpers/model-induct.lisp
M books/kestrel/helpers/speed-up-implementation.lisp
M books/kestrel/hints/casesx.lisp
M books/kestrel/hints/combine-hints.lisp
M books/kestrel/hints/remove-hints.lisp
M books/kestrel/hints/renaming-tests.lisp
M books/kestrel/hints/renaming.lisp
M books/kestrel/isar/defisar-doc.lisp
M books/kestrel/isar/defisar.lisp
M books/kestrel/isar/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/.sys/fold-r...@useless-runes.lsp
M books/kestrel/java/language/.sys/hexadecim...@useless-runes.lsp
M books/kestrel/java/top.lisp
M books/kestrel/json-parser/.sys/parse...@useless-runes.lsp
M books/kestrel/json-parser/parse-json.lisp
M books/kestrel/json-parser/parsed-json.lisp
M books/kestrel/json/json-bstar.lisp
M books/kestrel/jvm/.sys/array-b...@useless-runes.lsp
M books/kestrel/jvm/.sys/class-fi...@useless-runes.lsp
M books/kestrel/jvm/.sys/do-ins...@useless-runes.lsp
M books/kestrel/jvm/.sys/flo...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-f...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-r...@useless-runes.lsp
M books/kestrel/jvm/.sys/jvm-...@useless-runes.lsp
M books/kestrel/jvm/.sys/j...@useless-runes.lsp
M books/kestrel/jvm/.sys/read-and-par...@useless-runes.lsp
M books/kestrel/jvm/acl2-customization.lsp
M books/kestrel/jvm/ads2.lisp
M books/kestrel/jvm/arrays.lisp
M books/kestrel/jvm/arrays0.lisp
A books/kestrel/jvm/bindings.lisp
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-tests.lisp
M books/kestrel/jvm/control-flow.lisp
M books/kestrel/jvm/doc.lisp
M books/kestrel/jvm/events-for-class.lisp
M books/kestrel/jvm/execution-common.lisp
M books/kestrel/jvm/execution.lisp
M books/kestrel/jvm/execution2.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/get-method-info.lisp
M books/kestrel/jvm/heap.lisp
M books/kestrel/jvm/heap0.lisp
M books/kestrel/jvm/instructions.lisp
M books/kestrel/jvm/int-subtypes.lisp
M books/kestrel/jvm/intern-table.lisp
M books/kestrel/jvm/java-types.lisp
M books/kestrel/jvm/jvm-facts.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/method-indicators.lisp
M books/kestrel/jvm/methods.lisp
M books/kestrel/jvm/package.lsp
M books/kestrel/jvm/pc-designators.lisp
M books/kestrel/jvm/read-and-parse-class-file.lisp
M books/kestrel/jvm/read-class-from-hierarchy.lisp
M books/kestrel/jvm/read-class.lisp
M books/kestrel/jvm/read-jar.lisp
A books/kestrel/jvm/states.lisp
A books/kestrel/jvm/string-encoding.lisp
M books/kestrel/jvm/strings.lisp
M books/kestrel/jvm/symbolic-execution.lisp
M books/kestrel/jvm/symbolic-execution2.lisp
A books/kestrel/jvm/th.lisp
M books/kestrel/jvm/top.lisp
M books/kestrel/jvm/types.lisp
M books/kestrel/jvm/utilities.lisp
A books/kestrel/jvm/values.lisp
M books/kestrel/library-wrappers/my-make-flag-tests.lisp
A books/kestrel/lists-light/.sys/set-differen...@useless-runes.lsp
M books/kestrel/lists-light/all-eql-dollar.lisp
M books/kestrel/lists-light/all-same-eql.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/find-index.lisp
M books/kestrel/lists-light/firstn.lisp
M books/kestrel/lists-light/group-rules.lisp
M books/kestrel/lists-light/member-equal.lisp
M books/kestrel/lists-light/memberp.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/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/maps/maps.lisp
M books/kestrel/maps/maps0.lisp
M books/kestrel/memory/.sys/memo...@useless-runes.lsp
M books/kestrel/memory/.sys/memo...@useless-runes.lsp
M books/kestrel/memory/.sys/memo...@useless-runes.lsp
M books/kestrel/memory/make-memory-region-machinery.lisp
R books/kestrel/memory/memory-regions.lisp
M books/kestrel/meta/.sys/rewr...@useless-runes.lsp
M books/kestrel/meta/.sys/rewr...@useless-runes.lsp
M books/kestrel/meta/rewriter0.lisp
M books/kestrel/meta/rewriter1.lisp
M books/kestrel/number-theory/.sys/defprim...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/bv-rul...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/bv-r...@useless-runes.lsp
M books/kestrel/prime-fields/.sys/prime-field...@useless-runes.lsp
M books/kestrel/prime-fields/add.lisp
M books/kestrel/prime-fields/bitp-idioms.lisp
M books/kestrel/prime-fields/equal-of-add-move-negs-bind-free.lisp
M books/kestrel/prime-fields/fe-listp-fast.lisp
M books/kestrel/prime-fields/pow.lisp
M books/kestrel/prime-fields/prime-fields-rules.lisp
M books/kestrel/prime-fields/rules2.lisp
M books/kestrel/random/minstd-rand.lisp
M books/kestrel/random/minstd-rand0.lisp
M books/kestrel/random/top.lisp
A books/kestrel/remora/.gitattributes
A books/kestrel/remora/abstract-syntax-constructors.lisp
A books/kestrel/remora/abstract-syntax-core.lisp
A books/kestrel/remora/abstract-syntax-derived-fixtypes.lisp
A books/kestrel/remora/abstract-syntax-matching-operations.lisp
A books/kestrel/remora/abstract-syntax-structural-operations.lisp
A books/kestrel/remora/abstract-syntax-trees.lisp
A books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/abstract-syntax-well-formed.lisp
A books/kestrel/remora/abstract-syntax.lisp
A books/kestrel/remora/acl2-customization.lsp
A books/kestrel/remora/character-literal-codes.lisp
A books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/frame-flattening.lisp
A books/kestrel/remora/grammar.abnf
A books/kestrel/remora/grammar.lisp
A books/kestrel/remora/identifier-syntax.lisp
A books/kestrel/remora/ispace-equivalence.lisp
A 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
A books/kestrel/remora/parser.lisp
A books/kestrel/remora/portcullis.acl2
A books/kestrel/remora/portcullis.lisp
A books/kestrel/remora/post-parsing.lisp
A books/kestrel/remora/printer.lisp
A books/kestrel/remora/static-environments.lisp
A books/kestrel/remora/static-semantics.lisp
A books/kestrel/remora/syntax-abstraction.lisp
A books/kestrel/remora/top.acl2
A books/kestrel/remora/top.lisp
A books/kestrel/remora/type-checking.lisp
A books/kestrel/remora/type-equivalence.lisp
M books/kestrel/risc-v/executable/decoding-executable.lisp
M books/kestrel/risc-v/executable/execution-executable.lisp
M books/kestrel/sequences/defmap.lisp
M books/kestrel/sequences/top.lisp
M books/kestrel/sets/sets.lisp
M books/kestrel/simpl-imp/.sys/sema...@useless-runes.lsp
M books/kestrel/soft/defequal.lisp
M books/kestrel/soft/tests.lisp
M books/kestrel/solidity/boolean-operations.lisp
M books/kestrel/solidity/integer-operations.lisp
M books/kestrel/strings-light/add-prefix-to-strings.lisp
M books/kestrel/strings-light/collapse-whitespace.lisp
A books/kestrel/strings-light/downcase-tests.lisp
M books/kestrel/strings-light/parse-binary-digits.lisp
M books/kestrel/strings-light/parse-decimal-digits.lisp
M books/kestrel/strings-light/reverse.lisp
A books/kestrel/strings-light/split-chars-tests.lisp
M books/kestrel/strings-light/split-string-tests.lisp
M books/kestrel/strings-light/strings-starting-with.lisp
M books/kestrel/strings-light/strip-suffix-from-strings.lisp
M books/kestrel/strings-light/top.lisp
M books/kestrel/strings-light/upcase.lisp
M books/kestrel/syntheto/examples/rational-more.lisp
M books/kestrel/syntheto/examples/sort-rationals.lisp
M books/kestrel/syntheto/examples/spec-input-output.lisp
M books/kestrel/syntheto/examples/sum-squares.lisp
M books/kestrel/syntheto/examples/vanderbilt.lisp
M books/kestrel/syntheto/language/.sys/abstract-synt...@useless-runes.lsp
M books/kestrel/syntheto/language/.sys/static-sema...@useless-runes.lsp
M books/kestrel/syntheto/language/abstract-syntax.lisp
M books/kestrel/syntheto/shallow/.sys/te...@useless-runes.lsp
M books/kestrel/terms-light/.sys/make-i...@useless-runes.lsp
M books/kestrel/terms-light/arglistp1.lisp
M books/kestrel/terms-light/clearly-implies-for-disjunctionp.lisp
M books/kestrel/terms-light/combine-ifs-in-then-and-else-branches.lisp
M books/kestrel/terms-light/count-ifs-in-term.lisp
M books/kestrel/terms-light/count-ifs-in-then-and-else-branches.lisp
M books/kestrel/terms-light/drop-clearly-implied-conjuncts.lisp
M books/kestrel/terms-light/drop-unused-lambda-bindings-tests.lisp
M books/kestrel/terms-light/expand-lambdas-in-term.lisp
M books/kestrel/terms-light/filter-formals-and-actuals-proofs.lisp
M books/kestrel/terms-light/helpers.lisp
M books/kestrel/terms-light/let-vars-in-term.lisp
M books/kestrel/terms-light/logic-termp.lisp
M books/kestrel/terms-light/make-lambda-terms-simple.lisp
M books/kestrel/terms-light/serialize-lambdas-in-term-proofs.lisp
M books/kestrel/terms-light/simplify-ors.lisp
M books/kestrel/terms-light/subst-var-deep.lisp
M books/kestrel/terms-light/substitute-constants-in-lambdas-proofs.lisp
M books/kestrel/terms-light/substitute-lambda-formals.lisp
M books/kestrel/terms-light/top.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp
M books/kestrel/typed-lists-light/.sys/all-...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/decre...@useless-runes.lsp
M books/kestrel/typed-lists-light/.sys/intege...@useless-runes.lsp
M books/kestrel/typed-lists-light/keyword-listp.lisp
M books/kestrel/typed-lists-light/map-code-char.lisp
M books/kestrel/typed-lists-light/maxelem.lisp
M books/kestrel/typed-lists-light/minelem.lisp
M books/kestrel/typed-lists-light/pseudo-term-list-listp.lisp
M books/kestrel/typed-lists-light/top.lisp
M books/kestrel/unicode-light/code-point-to-utf-8-chars.lisp
M books/kestrel/unicode-light/hex-digit-chars-to-code-point.lisp
M books/kestrel/unicode-light/surrogates.lisp
M books/kestrel/untranslated-terms/bstar-helpers.lisp
M books/kestrel/untranslated-terms/conjuncts-and-disjuncts.lisp
M books/kestrel/untranslated-terms/conjuncts-of-uterm.lisp
M books/kestrel/untranslated-terms/disjuncts-of-uterm.lisp
M books/kestrel/untranslated-terms/free-vars.lisp
M books/kestrel/untranslated-terms/let-helpers.lisp
M books/kestrel/untranslated-terms/top.lisp
M books/kestrel/untranslated-terms/untranslated-terms-old.lisp
A books/kestrel/utilities/.sys/arith-fix-an...@useless-runes.lsp
A books/kestrel/utilities/.sys/arith-fix...@useless-runes.lsp
M books/kestrel/utilities/.sys/defstobj-...@useless-runes.lsp
M books/kestrel/utilities/.sys/for...@useless-runes.lsp
M books/kestrel/utilities/.sys/ld-hi...@useless-runes.lsp
M books/kestrel/utilities/.sys/redun...@useless-runes.lsp
M books/kestrel/utilities/.sys/run-json...@useless-runes.lsp
M books/kestrel/utilities/.sys/xdoc-...@useless-runes.lsp
M books/kestrel/utilities/bind-from-rules-tests.lisp
M books/kestrel/utilities/chars-and-codes.lisp
M books/kestrel/utilities/defmacrodoc.lisp
M books/kestrel/utilities/defopeners.lisp
M books/kestrel/utilities/digits-any-base/core.lisp
M books/kestrel/utilities/doublet-listp.lisp
M books/kestrel/utilities/fast-alist-set.lisp
M books/kestrel/utilities/fixup-irrelevants-tests.lisp
M books/kestrel/utilities/forcert.lisp
M books/kestrel/utilities/fresh-names.lisp
M books/kestrel/utilities/get-username.lisp
M books/kestrel/utilities/make-termination-theorem.lisp
M books/kestrel/utilities/my-get-event.lisp
M books/kestrel/utilities/osets.lisp
M books/kestrel/utilities/prove-dollar-plus.lisp
M books/kestrel/utilities/state.lisp
M books/kestrel/utilities/theory-invariants.lisp
M books/kestrel/utilities/unify.lisp
M books/kestrel/world-light/defined-fns-in-term.lisp
M books/kestrel/world-light/defs-in-world.lisp
M books/kestrel/world-light/tests.lisp
M books/kestrel/world-light/world-since-boot-strap.lisp
M books/kestrel/x86/.sys/alt-...@useless-runes.lsp
M books/kestrel/x86/.sys/assumptions...@useless-runes.lsp
M books/kestrel/x86/.sys/assumpt...@useless-runes.lsp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/.sys/assum...@useless-runes.lsp
M books/kestrel/x86/.sys/bytes-...@useless-runes.lsp
M books/kestrel/x86/.sys/canonical...@useless-runes.lsp
M books/kestrel/x86/.sys/condi...@useless-runes.lsp
M books/kestrel/x86/.sys/fl...@useless-runes.lsp
M books/kestrel/x86/.sys/flo...@useless-runes.lsp
M books/kestrel/x86/.sys/linear...@useless-runes.lsp
M books/kestrel/x86/.sys/memo...@useless-runes.lsp
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/.sys/read-an...@useless-runes.lsp
M books/kestrel/x86/.sys/read-bytes-an...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/read-over-...@useless-runes.lsp
M books/kestrel/x86/.sys/readers-an...@useless-runes.lsp
M books/kestrel/x86/.sys/register-reader...@useless-runes.lsp
M books/kestrel/x86/.sys/register-reader...@useless-runes.lsp
M books/kestrel/x86/.sys/rfl...@useless-runes.lsp
A books/kestrel/x86/.sys/run-until...@useless-runes.lsp
R books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
R books/kestrel/x86/.sys/run-unti...@useless-runes.lsp
A books/kestrel/x86/.sys/run-until...@useless-runes.lsp
M books/kestrel/x86/.sys/suppo...@useless-runes.lsp
M books/kestrel/x86/.sys/suppo...@useless-runes.lsp
M books/kestrel/x86/.sys/supp...@useless-runes.lsp
M books/kestrel/x86/.sys/supp...@useless-runes.lsp
M books/kestrel/x86/.sys/sup...@useless-runes.lsp
M books/kestrel/x86/.sys/write-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/write-over-w...@useless-runes.lsp
M books/kestrel/x86/.sys/x86-c...@useless-runes.lsp
M books/kestrel/x86/.sys/z...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions-new.acl2
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions32.acl2
M books/kestrel/x86/assumptions64.acl2
M books/kestrel/x86/bytes-loadedp.acl2
M books/kestrel/x86/bytes-loadedp.lisp
M books/kestrel/x86/canonical-unsigned.lisp
M books/kestrel/x86/canonical.acl2
M books/kestrel/x86/conditions.acl2
M books/kestrel/x86/conditions.lisp
M books/kestrel/x86/floats.acl2
M books/kestrel/x86/if-lowering.acl2
M books/kestrel/x86/linear-memory.acl2
M books/kestrel/x86/linear-memory.lisp
M books/kestrel/x86/memory32.acl2
M books/kestrel/x86/package.lsp
M books/kestrel/x86/read-and-write.acl2
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-and-write2.acl2
M books/kestrel/x86/read-and-write2.lisp
M books/kestrel/x86/read-bytes-and-write-bytes.acl2
M books/kestrel/x86/read-bytes-and-write-bytes.lisp
M books/kestrel/x86/read-over-write-rules.acl2
M books/kestrel/x86/read-over-write-rules32.acl2
M books/kestrel/x86/read-over-write-rules64.acl2
M books/kestrel/x86/register-readers-and-writers32.acl2
M books/kestrel/x86/register-readers-and-writers64.acl2
M books/kestrel/x86/register-readers-and-writers64.lisp
M books/kestrel/x86/rflags-spec-sub.lisp
M books/kestrel/x86/rflags2.acl2
M books/kestrel/x86/run-until-return.acl2
M books/kestrel/x86/run-until-return.lisp
M books/kestrel/x86/run-until-return2.acl2
M books/kestrel/x86/run-until-return2.lisp
M books/kestrel/x86/run-until-return3.acl2
M books/kestrel/x86/run-until-return4.acl2
M books/kestrel/x86/support-x86.acl2
M books/kestrel/x86/support.acl2
M books/kestrel/x86/support.lisp
M books/kestrel/x86/support2.acl2
M books/kestrel/x86/support2.lisp
M books/kestrel/x86/support32.acl2
M books/kestrel/x86/support32.lisp
M books/kestrel/x86/support64.lisp
M books/kestrel/x86/tools/.sys/lifter-...@useless-runes.lsp
M books/kestrel/x86/tools/.sys/unroll-x8...@useless-runes.lsp
M books/kestrel/x86/tools/lifter-support.acl2
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/tools/top.acl2
M books/kestrel/x86/tools/unroll-x86-code-old.acl2
M books/kestrel/x86/top.acl2
M books/kestrel/x86/write-over-write-rules.acl2
M books/kestrel/x86/write-over-write-rules32.acl2
M books/kestrel/x86/write-over-write-rules64.acl2
M books/kestrel/x86/zmm.acl2
M books/kestrel/xml/xml-parser.lisp
M books/kestrel/yul/language/.sys/abstrac...@useless-runes.lsp
M books/kestrel/yul/language/.sys/dynamic-...@useless-runes.lsp
M books/kestrel/yul/language/.sys/le...@useless-runes.lsp
M books/kestrel/yul/language/.sys/static-safe...@useless-runes.lsp
M books/kestrel/yul/language/.sys/static-s...@useless-runes.lsp
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/.sys/dead-code-elimi...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/no-function-def...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/renaming-varia...@useless-runes.lsp
M books/kestrel/yul/transformations/.sys/renaming-var...@useless-runes.lsp
M books/kestrel/yul/transformations/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/kestrel/zcash/.sys/jub...@useless-runes.lsp
M books/kestrel/zcash/.sys/pedersen-add...@useless-runes.lsp
M books/kestrel/zcash/.sys/pedersen-hash-b...@useless-runes.lsp
M books/kestrel/zcash/.sys/pedersen-hash-inje...@useless-runes.lsp
M books/kestrel/zcash/.sys/peders...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-1-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/a-3-3-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/.sys/proof-...@useless-runes.lsp
M books/kestrel/zcash/gadgets/a-3-3-1-alt-proof.lisp
M books/kestrel/zcash/gadgets/a-3-3-1-proof.lisp
M books/kestrel/zcash/gadgets/a-3-3-4-proof.lisp
M books/kestrel/zcash/gadgets/a-3-3-5-proof.lisp
M books/kestrel/zcash/gadgets/a-3-3-6-proof.lisp
M books/kestrel/zip/unzip.lisp
A books/misc/character-encoding-test.acl2.moved
M books/misc/character-encoding-test.lisp
M books/misc/check-acl2-exports.lisp
M books/projects/abnf/examples/uri.lisp
M books/projects/abnf/grammar-definer/deftreeops.lisp
M books/projects/abnf/grammar-parser/executable.lisp
M books/projects/abnf/grammar-printer/executable.lisp
M books/projects/abnf/notation/concrete-syntax-rules-validation.lisp
M books/projects/abnf/notation/concrete-syntax-validation.lisp
M books/projects/abnf/notation/convenience-constructors.lisp
M books/projects/abnf/notation/meta-circular-validation.lisp
M books/projects/abnf/notation/syntax-abstraction.lisp
M books/projects/abnf/notation/top.lisp
M books/projects/abnf/operations/ambiguity.lisp
M books/projects/abnf/operations/closure.lisp
M books/projects/abnf/operations/plugging.lisp
M books/projects/abnf/operations/renaming.lisp
M books/projects/abnf/operations/rule-utilities.lisp
M books/projects/abnf/parsing-tools/defdefparse-doc.lisp
M books/projects/abnf/parsing-tools/defdefparse.lisp
M books/projects/abnf/parsing-tools/primitives-defresult.lisp
M books/projects/abnf/top.lisp
M books/projects/abnf/tree-utilities.lisp
M books/projects/acl2-in-hol/.acl2holrc.bash
A books/projects/acl2-in-hol/Makefile
M books/projects/acl2-in-hol/README-acl2
A books/projects/acl2-in-hol/lisp/a2ml.bash
R books/projects/acl2-in-hol/lisp/a2ml.csh
A books/projects/acl2-in-hol/lisp/axioms-essence.bash
R books/projects/acl2-in-hol/lisp/axioms-essence.csh
A books/projects/acl2-in-hol/lisp/book-essence.bash
R books/projects/acl2-in-hol/lisp/book-essence.csh
A books/projects/acl2-in-hol/lisp/cert_pl_exclude
A books/projects/acl2-in-hol/lisp/obsolete-csh/a2ml.csh
A books/projects/acl2-in-hol/lisp/obsolete-csh/axioms-essence.csh
A books/projects/acl2-in-hol/lisp/obsolete-csh/book-essence.csh
M books/projects/acl2-in-hol/tests/.gitignore
M books/projects/acl2-in-hol/tests/doit
M books/projects/acl2-in-hol/tests/inputs/Makefile
M books/projects/acl2-in-hol/tests/inputs/PKGS.lsp
M books/projects/acl2-in-hol/tests/inputs/PKGS.sml
A books/projects/acl2-in-hol/tests/inputs/cert_pl_exclude
M books/projects/aleo/bft/next/.sys/author-round-pai...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/commi...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/dag-previ...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/dag-signer-...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/dag-sign...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/endorsed-...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/endorsemen...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/initial...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposal-...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-autho...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-a...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-d...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-endors...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-en...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-pre...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/proposed-roun...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/signed-i...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/signed-p...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/system...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/unequiv...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/unequivoca...@useless-runes.lsp
M books/projects/aleo/bft/next/.sys/validato...@useless-runes.lsp
M books/projects/aleo/leo/early-version/definition/execution.lisp
M books/projects/aleo/leo/early-version/definition/expressions.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/circuits/axe/.sys/blake2s-one-rou...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/blake2s-sp...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/blake2s1...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/blake2...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/keccak2...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/poseidon...@useless-runes.lsp
M books/projects/aleo/vm/circuits/axe/.sys/sup...@useless-runes.lsp
M books/projects/aleo/vm/circuits/library-extensions/.sys/om...@useless-runes.lsp
M books/projects/aleo/vm/circuits/pfcs/.sys/boolean-a...@useless-runes.lsp
M books/projects/aleo/vm/language/early-version/.sys/par...@useless-runes.lsp
M books/projects/aleo/vm/language/early-version/parser.lisp
M books/projects/bls12-377-curves/primes/.sys/bls12-377-...@useless-runes.lsp
M books/projects/bls12-377-curves/primes/.sys/bls12-3...@useless-runes.lsp
M books/projects/bls12-377-curves/primes/.sys/edwards-bls12-37...@useless-runes.lsp
M books/projects/bls12-377-curves/primes/.sys/t...@useless-runes.lsp
M books/projects/hol-in-acl2/acl2/.sys/h...@useless-runes.lsp
A books/projects/hol-in-acl2/acl2/.sys/hpp...@useless-runes.lsp
M books/projects/hol-in-acl2/acl2/.sys/lem...@useless-runes.lsp
R books/projects/hol-in-acl2/acl2/.sys/set-of-h...@useless-runes.lsp
M books/projects/hol-in-acl2/acl2/.sys/te...@useless-runes.lsp
M books/projects/hol-in-acl2/acl2/.sys/theo...@useless-runes.lsp
M books/projects/hol-in-acl2/acl2/hol.lisp
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/hol-in-acl2/examples/.sys/eval-po...@useless-runes.lsp
M books/projects/hol-in-acl2/examples/.sys/eval-pol...@useless-runes.lsp
M books/projects/hol-in-acl2/examples/.sys/eval-p...@useless-runes.lsp
A books/projects/hol-in-acl2/examples/.sys/ex1-...@useless-runes.lsp
M books/projects/hol-in-acl2/examples/.sys/ex1...@useless-runes.lsp
A books/projects/hol-in-acl2/examples/.sys/ex1...@useless-runes.lsp
M books/projects/hol-in-acl2/examples/.sys/example...@useless-runes.lsp
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval_poly.defhol
M books/projects/hol-in-acl2/examples/ex1.defhol
A books/projects/hol-in-acl2/examples/skolem-thy-exports.lisp
A books/projects/hol-in-acl2/examples/skolem-thy.lisp
A books/projects/hol-in-acl2/examples/skolem.defhol
A books/projects/hol-in-acl2/examples/skolemScript.sml
M books/projects/milawa/ACL2/bootstrap/level11/waterfall-steps.lisp
M books/projects/milawa/ACL2/bootstrap/level5/update-clause-bldr.lisp
M books/projects/milawa/ACL2/bootstrap/level9/add-equality.lisp
M books/projects/milawa/ACL2/bootstrap/level9/eqdatabasep.lisp
M books/projects/milawa/ACL2/bootstrap/logic/disjoin-formulas.lisp
M books/projects/milawa/ACL2/bootstrap/logic/proofp-3-provablep.lisp
M books/projects/milawa/ACL2/interface/pcert.lisp
M books/projects/oracle/stv-invariant-extraction-pitfall/.sys/a...@useless-runes.lsp
M books/projects/pfcs/.sys/abstract-synt...@useless-runes.lsp
M books/projects/pfcs/.sys/abstract-s...@useless-runes.lsp
M books/projects/pfcs/.sys/convenience-...@useless-runes.lsp
M books/projects/pfcs/.sys/gra...@useless-runes.lsp
M books/projects/pfcs/.sys/lif...@useless-runes.lsp
M books/projects/pfcs/.sys/parser-i...@useless-runes.lsp
M books/projects/pfcs/.sys/proof-...@useless-runes.lsp
M books/projects/pfcs/.sys/r1cs-...@useless-runes.lsp
M books/projects/pfcs/.sys/r1cs-...@useless-runes.lsp
M books/projects/pfcs/.sys/sema...@useless-runes.lsp
M books/projects/pfcs/.sys/toke...@useless-runes.lsp
M books/projects/pfcs/.sys/well-fo...@useless-runes.lsp
A books/projects/pfcs/README.md
R books/projects/pfcs/READNE.md
M books/projects/pfcs/convenience-constructors.lisp
M books/projects/pfcs/examples.lisp
M books/projects/pfcs/lexer.lisp
M books/projects/pfcs/lifting.lisp
M books/projects/pfcs/package.lsp
M books/projects/pfcs/parser-interface.lisp
M books/projects/pfcs/parser.lisp
M books/projects/pfcs/proof-support.lisp
M books/projects/pfcs/r1cs-bridge.lisp
M books/projects/pfcs/r1cs-subset.lisp
M books/projects/pfcs/semantics.lisp
M books/projects/pfcs/syntax-abstraction.lisp
M books/projects/pfcs/tokenizer.lisp
M books/projects/pfcs/top.lisp
M books/projects/poseidon/.sys/ingonya...@useless-runes.lsp
M books/projects/poseidon/.sys/instant...@useless-runes.lsp
M books/projects/python/embedding/types.lisp
M books/projects/rac/lisp/.sys/expand-r...@useless-runes.lsp
M books/projects/rac/src/program/parser/ast/statements.cpp
M books/projects/rac/src/program/parser/ast/statements.h
M books/projects/rac/src/program/parser/ast/types.cpp
M books/projects/rac/src/program/parser/ast/types.h
M books/projects/rac/src/program/parser/parser.yy
M books/projects/rac/src/program/sexpressions.h
M books/projects/rac/tests/yaml_test/data_types/basic.yml
A books/projects/rac/tests/yaml_test/data_types/mv-with-tmp-partial.cpp
A books/projects/rac/tests/yaml_test/data_types/mv-with-tmp-partial.cpp.ref.ast.lsp
A books/projects/rac/tests/yaml_test/data_types/mv-with-tmp.cpp
A books/projects/rac/tests/yaml_test/data_types/mv-with-tmp.cpp.ref.ast.lsp
A books/projects/rac/tests/yaml_test/data_types/return-mv-type-cast.cpp
A books/projects/rac/tests/yaml_test/data_types/return-mv-type-cast.cpp.ref.ast.lsp
A books/projects/rac/tests/yaml_test/data_types/typedef-redeclaration-2.cpp
A books/projects/rac/tests/yaml_test/data_types/typedef-redeclaration-2.cpp.ref.ast.lsp
M books/projects/rac/tests/yaml_test/data_types/typedef-redeclaration.cpp
M books/projects/rac/tests/yaml_test/data_types/typedef-redeclaration.ref.stderr
M books/projects/rac/tests/yaml_test/program_structure/basics.yml
M books/projects/rac/tests/yaml_test/program_structure/empty.ref.stderr
M books/projects/rp-rewriter/.sys/cl-co...@useless-runes.lsp
M books/projects/rp-rewriter/.sys/eval-fu...@useless-runes.lsp
M books/projects/rp-rewriter/.sys/extract...@useless-runes.lsp
M books/projects/rp-rewriter/.sys/rp-th...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/casesplit-f...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/casesp...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/cons-to-...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/equal...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/fast-alist...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/hons-ac...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/hons-g...@useless-runes.lsp
M books/projects/rp-rewriter/meta/.sys/mv-nt...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/apply-bind...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/apply-me...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/eval-funct...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/ex-counter...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/extract-for...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/gua...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/match-lh...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/proof-func...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/rp-co...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/rp-equa...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/rp-rw-...@useless-runes.lsp
M books/projects/rp-rewriter/proofs/.sys/rp-state-fun...@useless-runes.lsp
M books/projects/set-theory/.sys/can...@useless-runes.lsp
M books/projects/set-theory/.sys/fin...@useless-runes.lsp
M books/projects/set-theory/.sys/fo...@useless-runes.lsp
M books/projects/set-theory/.sys/injecti...@useless-runes.lsp
M books/projects/set-theory/.sys/inv...@useless-runes.lsp
M books/projects/set-theory/.sys/ordi...@useless-runes.lsp
M books/projects/set-theory/.sys/rest...@useless-runes.lsp
M books/projects/set-theory/.sys/schroeder-ber...@useless-runes.lsp
M books/projects/set-theory/.sys/set-a...@useless-runes.lsp
A books/projects/set-theory/.sys/sko...@useless-runes.lsp
M books/projects/set-theory/base.lisp
M books/projects/set-theory/cantor.lisp
M books/projects/set-theory/foldr.lisp
M books/projects/set-theory/ordinals.lisp
M books/projects/x86isa/doc.lisp
M books/projects/x86isa/linux/doc.lisp
M books/projects/x86isa/linux/init
A books/projects/x86isa/linux/init-networked
M books/projects/x86isa/machine/.sys/three-byte-op...@useless-runes.lsp
M books/projects/x86isa/machine/.sys/two-byte-opc...@useless-runes.lsp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/catalogue-doc.lisp
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/inst-doc.lisp
M books/projects/x86isa/machine/inst-listing.lisp
A books/projects/x86isa/machine/instructions/.sys/em...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/log...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/move...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/move...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/pa...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/pa...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/pc...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/pm...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/pm...@useless-runes.lsp
A books/projects/x86isa/machine/instructions/.sys/psh...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/ps...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/pun...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/.sys/rotate-a...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
A books/projects/x86isa/machine/instructions/bcd.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/cert.acl2
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
A books/projects/x86isa/machine/instructions/emms.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/.sys/log...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/fp/.sys/simd-i...@useless-runes.lsp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/cert.acl2
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
A books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
A books/projects/x86isa/machine/instructions/pack.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
A books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/state.lisp
M books/projects/x86isa/machine/syscalls.lisp
M books/projects/x86isa/machine/three-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/two-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/cert.acl2
M books/projects/x86isa/proofs/codewalker-examples/cert.acl2
M books/projects/x86isa/proofs/dataCopy/cert.acl2
M books/projects/x86isa/proofs/dissertation-examples/cert.acl2
M books/projects/x86isa/proofs/factorial/cert.acl2
M books/projects/x86isa/proofs/popcount/cert.acl2
M books/projects/x86isa/proofs/powOfTwo/cert.acl2
M books/projects/x86isa/proofs/utilities/app-view/cert.acl2
M books/projects/x86isa/proofs/utilities/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/paging-basics.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/top.acl2
M books/projects/x86isa/proofs/wordCount/cert.acl2
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/zeroCopy/marking-view/.sys/zero...@useless-runes.lsp
M books/projects/x86isa/proofs/zeroCopy/marking-view/cert.acl2
M books/projects/x86isa/proofs/zeroCopy/non-marking-view/cert.acl2
M books/projects/x86isa/tools/execution/asmtest/asmtest.lisp
M books/projects/x86isa/tools/execution/asmtest/testgen/Makefile
M books/projects/x86isa/tools/execution/init-page-tables.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
M books/projects/x86isa/tools/execution/instrument/top.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/quicklisp/bundle/software/cffi-20231021-git/grovel/asdf.lisp
M books/quicklisp/top.lisp
M books/quicklisp/update-libs.sh
M books/std/alists/alist-keys.lisp
A books/std/basic/.sys/yyy...@useless-runes.lsp
M books/std/basic/top.lisp
A books/std/basic/yyyjoin.lisp
M books/std/obags/.sys/co...@useless-runes.lsp
M books/std/obags/core.lisp
M books/std/obags/tests.lisp
A books/std/omaps/.sys/as...@useless-runes.lsp
A books/std/omaps/.sys/compa...@useless-runes.lsp
M books/std/omaps/.sys/co...@useless-runes.lsp
A books/std/omaps/.sys/del...@useless-runes.lsp
A books/std/omaps/.sys/extensi...@useless-runes.lsp
A books/std/omaps/.sys/from-...@useless-runes.lsp
A books/std/omaps/.sys/from-...@useless-runes.lsp
A books/std/omaps/.sys/sub...@useless-runes.lsp
A books/std/omaps/.sys/upd...@useless-runes.lsp
M books/std/omaps/.sys/with-fixin...@useless-runes.lsp
M books/std/omaps/assoc.lisp
M books/std/omaps/compatiblep.lisp
M books/std/omaps/core.lisp
M books/std/omaps/delete.lisp
M books/std/omaps/extensionality.lisp
M books/std/omaps/from-alist.lisp
M books/std/omaps/from-lists.lisp
M books/std/omaps/submap.lisp
M books/std/omaps/top.lisp
M books/std/omaps/update.lisp
R books/std/omaps/with-fixing-theorems.lisp
M books/std/strings/.sys/bin-digit-...@useless-runes.lsp
M books/std/strings/.sys/dec-digit-...@useless-runes.lsp
M books/std/strings/.sys/hex-digit-...@useless-runes.lsp
M books/std/strings/.sys/oct-digit-...@useless-runes.lsp
A books/std/system/.sys/impl...@useless-runes.lsp
A books/std/system/current-package-plus.lisp
M books/std/system/remove-dead-if-branches.lisp
M books/std/system/top.lisp
M books/std/util/.sys/add-io-pairs...@useless-runes.lsp
M books/std/util/.sys/add-io-pairs...@useless-runes.lsp
M books/std/util/.sys/add-io-pair...@useless-runes.lsp
M books/std/util/.sys/add-io-pa...@useless-runes.lsp
M books/std/util/defarbrec.lisp
M books/std/util/tests/.sys/defagg...@useless-runes.lsp
M books/std/util/tests/.sys/def...@useless-runes.lsp
M books/system/apply/.sys/apply...@useless-runes.lsp
M books/system/apply/apply-prim.lisp
M books/system/check-system-guards-raw.lsp
M books/system/check-system-guards.lisp
M books/system/defstobj.lisp
M books/system/doc/acl2-doc-wrap.lisp
M books/system/doc/acl2-doc.lisp
M books/system/doc/render-doc.lisp
M books/system/error1.lisp
M books/system/pseudo-good-worldp.lisp
A books/tools/.sys/elide-e...@useless-runes.lsp
A books/tools/.sys/elide...@useless-runes.lsp
A books/tools/.sys/eval-events-...@useless-runes.lsp
A books/tools/.sys/eval-events-f...@useless-runes.lsp
A books/tools/.sys/eval-event...@useless-runes.lsp
M books/tools/.sys/with-su...@useless-runes.lsp
M books/tools/flag.lisp
M books/tools/stobj-help.lisp
M books/workshops/2000/medina/polynomials/polynomial.lisp
M books/workshops/2000/medina/polynomials/term.lisp
M books/workshops/2000/ruiz/multiset/examples/ackermann/ackermann.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/confluence-v0.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/confluence.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/local-confluence.lisp
M books/workshops/2000/ruiz/multiset/examples/newman/newman.lisp
M books/workshops/2000/ruiz/multiset/multiset.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/dags.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-dags/support/terms.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/anti-unification.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/matching.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/renamings.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption-subst.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/subsumption.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/terms.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification-pattern.lisp
M books/workshops/2002/ruiz-alonso-hidalgo-martin-theory-terms/support/unification.lisp
M books/workshops/2004/ruiz-et-al/support/basic.lisp
M books/workshops/2004/ruiz-et-al/support/dag-unification-rules.lisp
M books/workshops/2004/ruiz-et-al/support/dags.lisp
M books/workshops/2004/ruiz-et-al/support/matching.lisp
M books/workshops/2004/ruiz-et-al/support/prefix-unification-rules.lisp
M books/workshops/2004/ruiz-et-al/support/q-dag-unification-rules.lisp
M books/workshops/2004/ruiz-et-al/support/q-dag-unification-st.lisp
M books/workshops/2004/ruiz-et-al/support/q-dag-unification.lisp
M books/workshops/2004/ruiz-et-al/support/subsumption-subst.lisp
M books/workshops/2004/ruiz-et-al/support/subsumption.lisp
M books/workshops/2004/ruiz-et-al/support/terms-as-dag.lisp
M books/workshops/2004/ruiz-et-al/support/terms.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/coe-fld.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-producto.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fucongruencias-suma.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuforma-normal.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fumonomio.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuopuesto.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio-normalizado.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fupolinomio.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fuproducto.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/fusuma.lisp
M books/workshops/2006/cowles-gamboa-euclid/Euclid/fld-u-poly/futermino.lisp
M books/workshops/2007/cowles-et-al/support/greve/ack.lisp
M books/workshops/2007/cowles-et-al/support/greve/defminterm.lisp
M books/workshops/2007/cowles-et-al/support/greve/defxch.lisp
M books/workshops/2007/dillinger-et-al/code/hacker-pkg.lsp
M books/workshops/2007/dillinger-et-al/code/table-guard.lisp
M books/workshops/2007/rubio/support/abstract-reductions/confluence.lisp
M books/workshops/2007/rubio/support/abstract-reductions/convergent.lisp
M books/workshops/2007/rubio/support/abstract-reductions/newman.lisp
M books/workshops/2007/rubio/support/multisets/multiset.lisp
M books/workshops/2007/rubio/support/simplicial-topology/generate-degenerate.lisp
M books/workshops/2020/peng-greenstreet/.sys/eval...@useless-runes.lsp
M books/workshops/2020/sswords-rewriter/.sys/sup...@useless-runes.lsp
M books/workshops/2020/sumners/.sys/gl-s...@useless-runes.lsp
M books/workshops/2023/coglio-mccarthy-smith/.sys/pf...@useless-runes.lsp
M books/workshops/2025/manjrekar/.sys/ctv...@useless-runes.lsp
M books/workshops/2025/manjrekar/examples/imul64/imul64-proof.lisp
M books/workshops/2025/manjrekar/examples/imul8/imul8-proof.lisp
M books/workshops/references/workshops.bib
M books/xdoc/.sys/save-c...@useless-runes.lsp
M books/xdoc/fancy/index-seo.php
M books/xdoc/save-classic.lisp
M books/xdoc/save-fancy.lisp
M books/xdoc/save-rendered.lisp
M books/xdoc/save.lisp
M books/xdoc/topics.lisp
M boot-strap-pass-2-a.lisp
M boot-strap-pass-2-b.lisp
M defpkgs.lisp
M defthm.lisp
M defuns.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M doc/home-page.lisp
M doc/write-acl2-code-size.lisp
M emacs/acl2-doc-open-url.el
M emacs/acl2-doc.el
M emacs/emacs-acl2.el
M emacs/html-to-xdoc.el
M emacs/monitor.el
M float-a.lisp
M float-b.lisp
M float-raw.lisp
M futures-raw.lisp
M history-management.lisp
M hons-raw.lisp
M hons.lisp
M induct.lisp
M init.lisp
M interface-raw.lisp
M ld.lisp
M linear-a.lisp
M linear-b.lisp
M memoize-raw.lisp
M memoize.lisp
M multi-threading-raw.lisp
M new.html
M non-linear.lisp
M openmcl-acl2-trace.lisp
M other-events.lisp
M other-processes.lisp
M parallel-raw.lisp
M parallel.lisp
M proof-builder-a.lisp
M proof-builder-b.lisp
M proof-builder-pkg.lisp
M prove.lisp
M rewrite.lisp
M save-gprof.lsp
M serialize-raw.lisp
M serialize.lisp
M simplify.lisp
M tau.lisp
M translate.lisp
M type-set-a.lisp
M type-set-b.lisp

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


Commit: b6071af120d4ba7dedba3b970785d6ab1c203e71
https://github.com/acl2/acl2/commit/b6071af120d4ba7dedba3b970785d6ab1c203e71
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/remora/static-semantics.lisp

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


Commit: 5608ecdac05752549763fa260cd08fb4d6a62f25
https://github.com/acl2/acl2/commit/5608ecdac05752549763fa260cd08fb4d6a62f25
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Avoid importing two symbols.


Commit: 00696e79111d186a8ad97410e87f78a9b2f1615d
https://github.com/acl2/acl2/commit/00696e79111d186a8ad97410e87f78a9b2f1615d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

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

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


Commit: 2f3dd1cbc6bfa8d3954cd1f13f28cc990f7dd85c
https://github.com/acl2/acl2/commit/2f3dd1cbc6bfa8d3954cd1f13f28cc990f7dd85c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

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

Log Message:
-----------
[Remora] Initial model of values.


Commit: ea96a3c87e9a80cbce63bd8e307371ca227d5f44
https://github.com/acl2/acl2/commit/ea96a3c87e9a80cbce63bd8e307371ca227d5f44
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/jvm/rules-in-rule-lists-jvm.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/x86/rule-lists.lisp
M books/kestrel/jvm/operand-stacks.lisp
M books/kestrel/x86/support32.lisp

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


Commit: 165158eb3dbf1ef7ac609f6b34d30d300659a466
https://github.com/acl2/acl2/commit/165158eb3dbf1ef7ac609f6b34d30d300659a466
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
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

Log Message:
-----------
[FTY] Extend `deffold-reduce` and `deffold-map`.

Add a mandatory `:name` input that specifies the name of the XDOC topic and the
name of the ruleset, where the latter is `<name>-rules`.

This replaces the previously hardwired `abstract-syntax-<suffix>` and
`abstract-syntax-<suffix>-rules` for the XDOC topic and for the ruleset, which
are too specific to abstract syntax, even though the folds work on any kinds of
fixtypes.

All the existing calls of these two macros will be updated, in upcoming commits,
in a way that does not change the previous names, but authors of those calls
might want to take advantage of the new capability to generate better names.


Commit: 064f50bd3590f5e846a254842c01851849378bf9
https://github.com/acl2/acl2/commit/064f50bd3590f5e846a254842c01851849378bf9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/printer.lisp

Log Message:
-----------
[Remora] Adapt to changes to `deffold-...`.


Commit: 39891202e77579d2cf4746bb5341c8f53181f95b
https://github.com/acl2/acl2/commit/39891202e77579d2cf4746bb5341c8f53181f95b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/c/language/decimal-0-to-octal-0.lisp

Log Message:
-----------
[C] Adapt to changes to `deffole-...`.


Commit: 3bce1be8ff9121571c21583c704a81b2d0ae51b5
https://github.com/acl2/acl2/commit/3bce1be8ff9121571c21583c704a81b2d0ae51b5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp

Log Message:
-----------
[C$] Adapt to changes to `deffold-...`.


Commit: 3a90b7015c2bcd9857c30eb2cffdfb3e0768f9ae
https://github.com/acl2/acl2/commit/3a90b7015c2bcd9857c30eb2cffdfb3e0768f9ae
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/c/transformation/rename.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp

Log Message:
-----------
[C2C] Adapt to changes to `deffold-...`.


Commit: 606dcae2f7b4ca694c1a3551b1cc4cfbe4a5b3ab
https://github.com/acl2/acl2/commit/606dcae2f7b4ca694c1a3551b1cc4cfbe4a5b3ab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
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/axe/.sys/get-di...@useless-runes.lsp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/bounded-dag-parent-arrayp.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/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.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/rules-in-rule-lists-jvm.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/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-common.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/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/rule-lists.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.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/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/wf-dagp.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/jvm/call-stacks.lisp
M books/kestrel/jvm/frames.lisp
M books/kestrel/jvm/operand-stacks.lisp
M books/kestrel/x86/support32.lisp

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


Commit: 3ea5d537165eaddce064fe415ed65a1f727dea00
https://github.com/acl2/acl2/commit/3ea5d537165eaddce064fe415ed65a1f727dea00
Author: Eric McCarthy <mcca...@kestrel.edu>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/syntax-abstraction.lisp

Log Message:
-----------
[remora] Allow empty escape \& in strings to match Haskell Remora parser. printer outputs \& only when needed for correctness


Commit: 9dd7ca749674c4f74b0300f6774f992877edd0d6
https://github.com/acl2/acl2/commit/9dd7ca749674c4f74b0300f6774f992877edd0d6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/c/language/decimal-0-to-octal-0.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.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/transformation/rename.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp
M books/kestrel/c/transformation/utilities/rename-fn.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/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/dynamic-semantics.lisp
M books/kestrel/remora/grammar.abnf
A books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-semantics.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/top.lisp
A books/kestrel/remora/values.lisp

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


Commit: 34655b02daba13ae24f9fa9ff22f1c4f3e6c1554
https://github.com/acl2/acl2/commit/34655b02daba13ae24f9fa9ff22f1c4f3e6c1554
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/x86/package.lsp

Log Message:
-----------
[axe/x86] Improve handling of blsi and tzcnt.


Commit: 36d0691c11bd1b05db35ea2813da4871b9a99738
https://github.com/acl2/acl2/commit/36d0691c11bd1b05db35ea2813da4871b9a99738
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/jvm/rules-in-rule-lists-jvm.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/x86/rule-lists.lisp
M books/kestrel/c/language/decimal-0-to-octal-0.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.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/transformation/rename.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp
M books/kestrel/c/transformation/utilities/rename-fn.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/jvm/operand-stacks.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/dynamic-semantics.lisp
M books/kestrel/remora/grammar.abnf
A books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-semantics.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/top.lisp
A books/kestrel/remora/values.lisp
M books/kestrel/x86/support32.lisp

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


Commit: 52bbd7610241ef48cf4f8ec6e8ca7b46ef33af0a
https://github.com/acl2/acl2/commit/52bbd7610241ef48cf4f8ec6e8ca7b46ef33af0a
Author: Eric McCarthy <mcca...@kestrel.edu>
Date: 2026-05-04 (Mon, 04 May 2026)

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

Log Message:
-----------
[remora] improve xdoc topic name for a deffold-reduce


Commit: 0055005441ef02bb73f8229a708acf621cf484e3
https://github.com/acl2/acl2/commit/0055005441ef02bb73f8229a708acf621cf484e3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

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

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


Commit: 829db9429cfb2e0bf5e74ec6453b6796298e73b1
https://github.com/acl2/acl2/commit/829db9429cfb2e0bf5e74ec6453b6796298e73b1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-04 (Mon, 04 May 2026)

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

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


Commit: 5a701f9e246a9d10800f3290fb8a597c93ca28fe
https://github.com/acl2/acl2/commit/5a701f9e246a9d10800f3290fb8a597c93ca28fe
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv/bitops.lisp

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


Commit: 656d146d9e25df9f8766d2b17a07e24174def10f
https://github.com/acl2/acl2/commit/656d146d9e25df9f8766d2b17a07e24174def10f
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Improve inference of implicit designations

This fixes a case where anonymous struct/unions were causing
designation inference to fail.


Commit: 49bba68fde9a8f0c93c571fbba5ef1118304fd7e
https://github.com/acl2/acl2/commit/49bba68fde9a8f0c93c571fbba5ef1118304fd7e
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-05-05 (Tue, 05 May 2026)

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

Log Message:
-----------
[C$] Add validator test for implicit designation inference

Add a test case that checks the validator correctly infers implicit
designations for a list of undesignated initializers. The test includes
bit-fields (named and unnamed) and an anonymous union.

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


Commit: e9fff0e868e02c98ef748b85c255b1fc558b1b47
https://github.com/acl2/acl2/commit/e9fff0e868e02c98ef748b85c255b1fc558b1b47
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

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

Log Message:
-----------
[C$] Promote function to top-level.


Commit: 640861da9c50f5e07bf1a446b31190b7ad3afe6c
https://github.com/acl2/acl2/commit/640861da9c50f5e07bf1a446b31190b7ad3afe6c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/kestrel/c/syntax/grammar/encoding-prefixes.abnf

Log Message:
-----------
[C$] Improve some doc.


Commit: fbe8f510cddfe65777c99cfef502166973ea8e63
https://github.com/acl2/acl2/commit/fbe8f510cddfe65777c99cfef502166973ea8e63
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/identifier-lists.abnf

Log Message:
-----------
[C$] Factor a grammar rule.


Commit: 15857e9a978e21fde50395803bbed94413730df3
https://github.com/acl2/acl2/commit/15857e9a978e21fde50395803bbed94413730df3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

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

Log Message:
-----------
[C$] Improve some variable names.


Commit: 0e5a9bfe3b04246884891943a96b995ca6c6d182
https://github.com/acl2/acl2/commit/0e5a9bfe3b04246884891943a96b995ca6c6d182
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

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

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


Commit: 0eb643480a0ec152e51f98510ff08d054c1afae4
https://github.com/acl2/acl2/commit/0eb643480a0ec152e51f98510ff08d054c1afae4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

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

Log Message:
-----------
[C$] Add a theorem.


Commit: 20ed5f0660eb6c45bf87dca58eb01f48ff226e2d
https://github.com/acl2/acl2/commit/20ed5f0660eb6c45bf87dca58eb01f48ff226e2d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

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

Log Message:
-----------
[C$] Change recursion structure.

This is in preparation for extensions for modular validation.


Commit: 0daddd0f19d4058effb1eaf39e78c1ad17fbe306
https://github.com/acl2/acl2/commit/0daddd0f19d4058effb1eaf39e78c1ad17fbe306
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

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

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

Have it generate an additional theorem.


Commit: 8622c9911d8282e0e83b1bee0d18c98c92c5ba91
https://github.com/acl2/acl2/commit/8622c9911d8282e0e83b1bee0d18c98c92c5ba91
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

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

Log Message:
-----------
[C$] Remove theorem now auto-generated.


Commit: d4c2403ba5bcf83e16eed475835d335f0a137253
https://github.com/acl2/acl2/commit/d4c2403ba5bcf83e16eed475835d335f0a137253
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/grammar-rest.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

Log Message:
-----------
[C$] Modularize and extend some grammar rules.

These are the rules for preprocessing directives.


Commit: cac9fb6dd05c0d7cf6a6c14201debbad9fbd8291
https://github.com/acl2/acl2/commit/cac9fb6dd05c0d7cf6a6c14201debbad9fbd8291
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

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

Log Message:
-----------
[C$] Avoid some run-time checks via guards.


Commit: 9ef84e3805e9479b966394011cb32b7bdfdc396b
https://github.com/acl2/acl2/commit/9ef84e3805e9479b966394011cb32b7bdfdc396b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

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

Log Message:
-----------
[FTY] Extend `deffold-redudce`.

Have it generate another theorem.


Commit: 69c96f47ede3ad995ba5109757fc37b392b6993f
https://github.com/acl2/acl2/commit/69c96f47ede3ad995ba5109757fc37b392b6993f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

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

Log Message:
-----------
[C$] Avoid some run-time checks via guards.


Commit: 084df6bd5793a173255b26584b1ba580c674cf4c
https://github.com/acl2/acl2/commit/084df6bd5793a173255b26584b1ba580c674cf4c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

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

Log Message:
-----------
[C$] Improve some variable names.


Commit: c656640af155fe1e16c25c669cd9e75527457eb3
https://github.com/acl2/acl2/commit/c656640af155fe1e16c25c669cd9e75527457eb3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/encoding-prefixes.abnf
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/identifier-lists.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c17.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c23.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives.abnf

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


Compare: https://github.com/acl2/acl2/compare/4ea27c7e4c39...c656640af155
Reply all
Reply to author
Forward
0 new messages