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