chore: cut compile-IR-to-machine + lift-binary crates (out of scope)#1542
Merged
Conversation
|
Warning Review limit reached
More reviews will be available in 37 minutes and 2 seconds. Learn how PR review limits work. Your organization has run out of usage credits. Purchase more in the billing tab. ⌛ How to resolve this issue?After more reviews become available, a review can be triggered using the We recommend that you space out your commits to avoid hitting the rate limit. 🚦 How do rate limits work?CodeRabbit enforces hourly rate limits for each developer per organization. Our paid plans include higher PR review limits than trial, open-source, and free plans. In all cases, reviews become available again over time. During sustained high-volume PR review activity, CodeRabbit may temporarily slow when the next review becomes available. Please see our Fair Usage Limits Policy for further information. ℹ️ Review info⚙️ Run configurationConfiguration used: Organization UI Review profile: CHILL Plan: Pro Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (95)
WalkthroughThis PR removes EVM bytecode kit support from the Provekit infrastructure by deleting the ChangesEVM bytecode kit removal
Estimated code review effort🎯 2 (Simple) | ⏱️ ~12 minutes Possibly related PRs
🚥 Pre-merge checks | ✅ 5✅ Passed checks (5 passed)
✏️ Tip: You can configure your own custom pre-merge checks in the settings. ✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 84125a3795
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
34
to
37
| "provekit-lift-quickcheck", | ||
| "provekit-lift-verus", | ||
| "provekit-lift-rust-tests", | ||
| "provekit-lift-asm-x86-64", | ||
| "provekit-lift-jvm-bytecode", | ||
| "provekit-lift-evm-bytecode", | ||
| "provekit-lift-openapi", |
There was a problem hiding this comment.
Removing the provekit-lift-jvm-bytecode and provekit-lift-evm-bytecode members here leaves currently exposed lift surfaces without buildable binaries: provekit-cli still advertises jvm-bytecode and evm-bytecode in KNOWN_SURFACES (implementations/rust/provekit-cli/src/project_config.rs), and the shipped manifests still invoke ./target/release/provekit-lift-jvm-bytecode / ...-evm-bytecode (implementations/rust/.provekit/lift/*/manifest.toml, line 5). After this commit, cargo pkgid -p provekit-lift-jvm-bytecode and -p provekit-lift-evm-bytecode fail with “did not match any packages,” so these surfaces regress to runtime failure unless the surfaces/manifests are removed in the same change.
Useful? React with 👍 / 👎.
TSavo
force-pushed
the
chore/cut-machine-compilers-and-binary-lifters
branch
from
84125a3 to
cc239cd
Compare
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 1
🧹 Nitpick comments (1)
implementations/rust/provekit-cli/src/cmd_mint.rs (1)
2315-2315: ⚡ Quick winUpdate the test function name to reflect the actual kit count.
The function name
resolve_kit_all_13_ci_kitsis now inaccurate:
- The test array contains 12 kits (not 13) after removing
evm-bytecode.- The test includes
swift, which is macOS-only and not part of the Linux CI matrix.- The test excludes
php, which is inKIT_TABLE.Consider renaming to
resolve_kit_all_12_kitsor similar to match the actual test coverage.♻️ Proposed fix
- fn resolve_kit_all_13_ci_kits() { + fn resolve_kit_all_12_kits() { let kits = [🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@implementations/rust/provekit-cli/src/cmd_mint.rs` at line 2315, Rename the test function resolve_kit_all_13_ci_kits to reflect the actual kit count and contents (e.g., resolve_kit_all_12_kits or resolve_kit_all_ci_kits), and update any references to that function; ensure the new name matches the test array (which no longer contains "evm-bytecode", includes "swift" which is macOS-only and not in the Linux CI matrix, and currently omits "php" from KIT_TABLE) so the function name accurately describes the kits being tested.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@Makefile`:
- Line 107: Update the help text in the Makefile echo that currently reads "make
prove-all all 12 Linux kits (swift excluded: macOS-only)" to reflect the
correct kit count after removing evm-bytecode; change the string to "all 11
Linux kits (swift excluded: macOS-only)" so the printed message matches the
listed kits (the echo line containing "make prove-all all 12 Linux kits
(swift excluded: macOS-only)").
---
Nitpick comments:
In `@implementations/rust/provekit-cli/src/cmd_mint.rs`:
- Line 2315: Rename the test function resolve_kit_all_13_ci_kits to reflect the
actual kit count and contents (e.g., resolve_kit_all_12_kits or
resolve_kit_all_ci_kits), and update any references to that function; ensure the
new name matches the test array (which no longer contains "evm-bytecode",
includes "swift" which is macOS-only and not in the Linux CI matrix, and
currently omits "php" from KIT_TABLE) so the function name accurately describes
the kits being tested.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: CHILL
Plan: Pro
Run ID: 4ebdb138-3311-4dd5-af24-ef0ceec49d52
⛔ Files ignored due to path filters (1)
implementations/rust/Cargo.lockis excluded by!**/*.lock
📒 Files selected for processing (93)
.github/workflows/ci.ymlMakefileimplementations/rust/.provekit/lift/evm-bytecode/manifest.tomlimplementations/rust/.provekit/lift/jvm-bytecode/manifest.tomlimplementations/rust/Cargo.tomlimplementations/rust/provekit-cli/src/cmd_mint.rsimplementations/rust/provekit-cli/tests/mint_kit_integration.rsimplementations/rust/provekit-ir-codegen/Cargo.tomlimplementations/rust/provekit-ir-codegen/src/cddl_parser.rsimplementations/rust/provekit-ir-codegen/src/compile.rsimplementations/rust/provekit-ir-codegen/src/coq.rsimplementations/rust/provekit-ir-codegen/src/emit_formula_coq.rsimplementations/rust/provekit-ir-codegen/src/emit_formula_smt.rsimplementations/rust/provekit-ir-codegen/src/emit_term.rsimplementations/rust/provekit-ir-codegen/src/emit_term_coq.rsimplementations/rust/provekit-ir-codegen/src/free_vars.rsimplementations/rust/provekit-ir-codegen/src/h.rsimplementations/rust/provekit-ir-codegen/src/lib.rsimplementations/rust/provekit-ir-codegen/src/main.rsimplementations/rust/provekit-ir-codegen/src/rust_gen.rsimplementations/rust/provekit-ir-codegen/src/smt.rsimplementations/rust/provekit-ir-codegen/tests/cddl_valid.rsimplementations/rust/provekit-ir-compiler-c/Cargo.tomlimplementations/rust/provekit-ir-compiler-c/README.mdimplementations/rust/provekit-ir-compiler-c/specs/algebra_to_c.spec.jsonimplementations/rust/provekit-ir-compiler-c/src/generated.rsimplementations/rust/provekit-ir-compiler-c/src/lib.rsimplementations/rust/provekit-ir-compiler-c/src/main.rsimplementations/rust/provekit-ir-compiler-c/tests/byte_for_byte.rsimplementations/rust/provekit-ir-compiler-c/tests/fixtures/foo.expected.cimplementations/rust/provekit-ir-compiler-c/tests/fixtures/foo.term.jsonimplementations/rust/provekit-ir-compiler-c/tests/smoke.rsimplementations/rust/provekit-ir-compiler-jvm-bytecode/Cargo.tomlimplementations/rust/provekit-ir-compiler-jvm-bytecode/README.mdimplementations/rust/provekit-ir-compiler-jvm-bytecode/specs/algebra_to_jvm.spec.jsonimplementations/rust/provekit-ir-compiler-jvm-bytecode/src/generated.rsimplementations/rust/provekit-ir-compiler-jvm-bytecode/src/lib.rsimplementations/rust/provekit-ir-compiler-jvm-bytecode/src/main.rsimplementations/rust/provekit-ir-compiler-jvm-bytecode/tests/byte_for_byte.rsimplementations/rust/provekit-ir-compiler-jvm-bytecode/tests/fixtures/foo.expected.jimplementations/rust/provekit-ir-compiler-jvm-bytecode/tests/fixtures/foo.term.jsonimplementations/rust/provekit-ir-compiler-jvm-bytecode/tests/smoke.rsimplementations/rust/provekit-ir-compiler-stub/Cargo.tomlimplementations/rust/provekit-ir-compiler-stub/src/lib.rsimplementations/rust/provekit-ir-compiler-stub/tests/stub.rsimplementations/rust/provekit-ir-compiler-wasm/Cargo.tomlimplementations/rust/provekit-ir-compiler-wasm/README.mdimplementations/rust/provekit-ir-compiler-wasm/fixtures/foo.watimplementations/rust/provekit-ir-compiler-wasm/specs/algebra_to_wasm.spec.jsonimplementations/rust/provekit-ir-compiler-wasm/src/generated.rsimplementations/rust/provekit-ir-compiler-wasm/src/lib.rsimplementations/rust/provekit-ir-compiler-wasm/src/main.rsimplementations/rust/provekit-ir-compiler-wasm/tests/byte_for_byte.rsimplementations/rust/provekit-ir-compiler-wasm/tests/smoke.rsimplementations/rust/provekit-ir-compiler-x86-64/Cargo.tomlimplementations/rust/provekit-ir-compiler-x86-64/README.mdimplementations/rust/provekit-ir-compiler-x86-64/specs/algebra_to_x86_64.spec.jsonimplementations/rust/provekit-ir-compiler-x86-64/src/generated.rsimplementations/rust/provekit-ir-compiler-x86-64/src/lib.rsimplementations/rust/provekit-ir-compiler-x86-64/src/main.rsimplementations/rust/provekit-ir-compiler-x86-64/tests/byte_for_byte.rsimplementations/rust/provekit-ir-compiler-x86-64/tests/fixtures/foo.expected.simplementations/rust/provekit-ir-compiler-x86-64/tests/fixtures/foo.term.jsonimplementations/rust/provekit-ir-compiler-x86-64/tests/smoke.rsimplementations/rust/provekit-lift-asm-aarch64/Cargo.tomlimplementations/rust/provekit-lift-asm-aarch64/README.mdimplementations/rust/provekit-lift-asm-aarch64/src/lib.rsimplementations/rust/provekit-lift-asm-aarch64/src/main.rsimplementations/rust/provekit-lift-asm-aarch64/tests/fixtures/foo.simplementations/rust/provekit-lift-asm-aarch64/tests/smoke.rsimplementations/rust/provekit-lift-asm-x86-64/Cargo.tomlimplementations/rust/provekit-lift-asm-x86-64/README.mdimplementations/rust/provekit-lift-asm-x86-64/manifest.tomlimplementations/rust/provekit-lift-asm-x86-64/specs/x86_64_sysv_signature.spec.jsonimplementations/rust/provekit-lift-asm-x86-64/src/lib.rsimplementations/rust/provekit-lift-asm-x86-64/src/main.rsimplementations/rust/provekit-lift-asm-x86-64/tests/fixtures/foo.gnu-objdump.txtimplementations/rust/provekit-lift-asm-x86-64/tests/fixtures/foo.simplementations/rust/provekit-lift-asm-x86-64/tests/smoke.rsimplementations/rust/provekit-lift-evm-bytecode/Cargo.tomlimplementations/rust/provekit-lift-evm-bytecode/src/lib.rsimplementations/rust/provekit-lift-evm-bytecode/src/main.rsimplementations/rust/provekit-lift-evm-bytecode/tests/fixtures/add.evmimplementations/rust/provekit-lift-evm-bytecode/tests/smoke.rsimplementations/rust/provekit-lift-jvm-bytecode/Cargo.tomlimplementations/rust/provekit-lift-jvm-bytecode/README.mdimplementations/rust/provekit-lift-jvm-bytecode/src/lib.rsimplementations/rust/provekit-lift-jvm-bytecode/src/main.rsimplementations/rust/provekit-lift-jvm-bytecode/tests/fixtures/foo.jimplementations/rust/provekit-lift-jvm-bytecode/tests/fixtures/instance_method.jimplementations/rust/provekit-lift-jvm-bytecode/tests/fixtures/static_read_after_write.jimplementations/rust/provekit-lift-jvm-bytecode/tests/fixtures/static_read_only.jimplementations/rust/provekit-lift-jvm-bytecode/tests/smoke.rs
💤 Files with no reviewable changes (91)
- implementations/rust/provekit-ir-compiler-x86-64/tests/smoke.rs
- implementations/rust/provekit-ir-compiler-x86-64/tests/fixtures/foo.term.json
- implementations/rust/provekit-ir-compiler-c/tests/fixtures/foo.term.json
- implementations/rust/provekit-lift-asm-x86-64/tests/fixtures/foo.gnu-objdump.txt
- implementations/rust/provekit-ir-codegen/src/emit_formula_smt.rs
- implementations/rust/provekit-lift-asm-aarch64/src/main.rs
- implementations/rust/provekit-lift-evm-bytecode/Cargo.toml
- implementations/rust/provekit-ir-compiler-wasm/fixtures/foo.wat
- implementations/rust/provekit-ir-compiler-wasm/README.md
- implementations/rust/provekit-ir-codegen/src/emit_term.rs
- implementations/rust/provekit-ir-compiler-c/src/lib.rs
- implementations/rust/provekit-ir-compiler-wasm/specs/algebra_to_wasm.spec.json
- implementations/rust/provekit-lift-jvm-bytecode/tests/fixtures/foo.j
- implementations/rust/provekit-ir-compiler-c/tests/fixtures/foo.expected.c
- implementations/rust/provekit-ir-compiler-x86-64/tests/byte_for_byte.rs
- implementations/rust/provekit-ir-codegen/src/main.rs
- implementations/rust/provekit-lift-asm-aarch64/README.md
- implementations/rust/provekit-ir-compiler-c/README.md
- implementations/rust/provekit-ir-codegen/Cargo.toml
- implementations/rust/provekit-ir-compiler-x86-64/tests/fixtures/foo.expected.s
- implementations/rust/provekit-ir-compiler-jvm-bytecode/src/generated.rs
- implementations/rust/provekit-ir-compiler-jvm-bytecode/src/main.rs
- implementations/rust/provekit-ir-codegen/src/free_vars.rs
- implementations/rust/provekit-lift-jvm-bytecode/tests/fixtures/static_read_after_write.j
- implementations/rust/provekit-ir-compiler-wasm/Cargo.toml
- implementations/rust/provekit-ir-compiler-wasm/tests/byte_for_byte.rs
- implementations/rust/provekit-ir-compiler-jvm-bytecode/tests/fixtures/foo.expected.j
- implementations/rust/provekit-lift-jvm-bytecode/tests/fixtures/instance_method.j
- implementations/rust/provekit-ir-codegen/src/lib.rs
- implementations/rust/provekit-ir-compiler-x86-64/README.md
- implementations/rust/provekit-lift-asm-aarch64/tests/fixtures/foo.s
- implementations/rust/provekit-lift-evm-bytecode/src/main.rs
- implementations/rust/provekit-lift-asm-x86-64/tests/fixtures/foo.s
- implementations/rust/provekit-ir-compiler-wasm/src/main.rs
- implementations/rust/provekit-ir-compiler-c/tests/smoke.rs
- implementations/rust/provekit-lift-asm-aarch64/tests/smoke.rs
- implementations/rust/provekit-ir-compiler-x86-64/Cargo.toml
- implementations/rust/provekit-lift-asm-x86-64/Cargo.toml
- implementations/rust/provekit-ir-codegen/src/cddl_parser.rs
- implementations/rust/provekit-lift-jvm-bytecode/README.md
- implementations/rust/.provekit/lift/evm-bytecode/manifest.toml
- implementations/rust/provekit-ir-codegen/tests/cddl_valid.rs
- implementations/rust/provekit-ir-codegen/src/emit_term_coq.rs
- implementations/rust/provekit-ir-codegen/src/coq.rs
- implementations/rust/provekit-ir-compiler-c/src/generated.rs
- implementations/rust/.provekit/lift/jvm-bytecode/manifest.toml
- implementations/rust/provekit-ir-compiler-jvm-bytecode/specs/algebra_to_jvm.spec.json
- .github/workflows/ci.yml
- implementations/rust/provekit-ir-compiler-wasm/src/generated.rs
- implementations/rust/provekit-lift-asm-aarch64/src/lib.rs
- implementations/rust/provekit-lift-jvm-bytecode/src/main.rs
- implementations/rust/provekit-ir-codegen/src/emit_formula_coq.rs
- implementations/rust/provekit-ir-compiler-jvm-bytecode/Cargo.toml
- implementations/rust/provekit-lift-asm-x86-64/src/lib.rs
- implementations/rust/provekit-ir-compiler-c/Cargo.toml
- implementations/rust/provekit-ir-compiler-wasm/tests/smoke.rs
- implementations/rust/provekit-ir-compiler-stub/tests/stub.rs
- implementations/rust/provekit-ir-compiler-wasm/src/lib.rs
- implementations/rust/provekit-ir-compiler-c/specs/algebra_to_c.spec.json
- implementations/rust/provekit-lift-jvm-bytecode/tests/fixtures/static_read_only.j
- implementations/rust/provekit-ir-compiler-c/src/main.rs
- implementations/rust/provekit-ir-compiler-stub/Cargo.toml
- implementations/rust/provekit-ir-compiler-jvm-bytecode/tests/smoke.rs
- implementations/rust/provekit-lift-asm-x86-64/src/main.rs
- implementations/rust/provekit-lift-asm-aarch64/Cargo.toml
- implementations/rust/provekit-ir-compiler-jvm-bytecode/tests/byte_for_byte.rs
- implementations/rust/provekit-lift-asm-x86-64/specs/x86_64_sysv_signature.spec.json
- implementations/rust/provekit-lift-asm-x86-64/manifest.toml
- implementations/rust/provekit-lift-jvm-bytecode/Cargo.toml
- implementations/rust/provekit-ir-compiler-jvm-bytecode/tests/fixtures/foo.term.json
- implementations/rust/provekit-lift-asm-x86-64/README.md
- implementations/rust/provekit-ir-compiler-x86-64/src/lib.rs
- implementations/rust/provekit-ir-codegen/src/smt.rs
- implementations/rust/provekit-ir-codegen/src/h.rs
- implementations/rust/provekit-ir-compiler-c/tests/byte_for_byte.rs
- implementations/rust/provekit-ir-compiler-x86-64/specs/algebra_to_x86_64.spec.json
- implementations/rust/provekit-ir-compiler-stub/src/lib.rs
- implementations/rust/provekit-ir-compiler-x86-64/src/generated.rs
- implementations/rust/provekit-lift-jvm-bytecode/tests/smoke.rs
- implementations/rust/provekit-lift-jvm-bytecode/src/lib.rs
- implementations/rust/Cargo.toml
- implementations/rust/provekit-lift-evm-bytecode/tests/fixtures/add.evm
- implementations/rust/provekit-lift-evm-bytecode/tests/smoke.rs
- implementations/rust/provekit-ir-codegen/src/compile.rs
- implementations/rust/provekit-ir-compiler-jvm-bytecode/src/lib.rs
- implementations/rust/provekit-lift-evm-bytecode/src/lib.rs
- implementations/rust/provekit-ir-compiler-jvm-bytecode/README.md
- implementations/rust/provekit-lift-asm-x86-64/tests/smoke.rs
- implementations/rust/provekit-ir-codegen/src/rust_gen.rs
- implementations/rust/provekit-ir-compiler-x86-64/src/main.rs
- implementations/rust/provekit-cli/tests/mint_kit_integration.rs
| @@ -105,7 +105,7 @@ help: | |||
| @echo "" | |||
| @echo "Per-kit conformance gate (C1-C8 lift-plugin-protocol verifiers):" | |||
| @echo " make prove-all all 12 Linux kits (swift excluded: macOS-only)" | |||
There was a problem hiding this comment.
Update the kit count to match the actual number.
The help text states "all 12 Linux kits" but lines 108-109 enumerate only 11 kits (rust, go, cpp, ts, csharp, clr-bytecode, java, python, ruby, zig, c). After removing evm-bytecode, the count should be 11.
📝 Proposed fix
- `@echo` " make prove-all all 12 Linux kits (swift excluded: macOS-only)"
+ `@echo` " make prove-all all 11 Linux kits (swift excluded: macOS-only)"📝 Committable suggestion
‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.
Suggested change
| @echo " make prove-all all 12 Linux kits (swift excluded: macOS-only)" | |
| `@echo` " make prove-all all 11 Linux kits (swift excluded: macOS-only)" |
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@Makefile` at line 107, Update the help text in the Makefile echo that
currently reads "make prove-all all 12 Linux kits (swift excluded:
macOS-only)" to reflect the correct kit count after removing evm-bytecode;
change the string to "all 11 Linux kits (swift excluded: macOS-only)" so the
printed message matches the listed kits (the echo line containing "make
prove-all all 12 Linux kits (swift excluded: macOS-only)").
…tecode kit Out-of-scope per the honest-spike census (A: compile ProofIR to a machine target; B: lift a compiled binary, not library sugar). Deletes 10 crates (ir-compiler-x86-64/wasm/c/ stub/jvm-bytecode + ir-codegen; lift-asm-aarch64/x86-64 + lift-evm-bytecode/jvm-bytecode) and unwires the evm-bytecode KIT that rode the deleted lifter: KIT_TABLE entry, the round-trip test, the CI conformance-matrix slot, the prove-evm-bytecode Makefile target, and the orphan evm/jvm lift manifests. Keeps the ir-compiler parent + the smt-lib/coq/ lean/maude solver backends. Verification: cargo build --workspace clean; cargo test --workspace --no-run clean (no dangling refs in any test target). Full `make test-rust` could not complete on this host (PEP 668 externally-managed pip for build-python; pnpm no-TTY) — env, not this change; CI is the authoritative runtime gate. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
TSavo
force-pushed
the
chore/cut-machine-compilers-and-binary-lifters
branch
from
cc239cd to
fd01307
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Per the honest-spike scope census (
CODE-VS-DICTIONARY.md), the A (compile-ProofIR-to-machine-target) and B (lift-a-binary) experiment families. The product lifts sugar→contract and discharges against solvers — it does not compile IR to machine code or lift assembly/bytecode.Confirmed orphans: depended on by nothing but the workspace member list. The verifier/cli/linker use the
ir-compilerparent abstraction and the smt-lib/coq/lean/maude solver backends — all kept.Delete (10 crates):
provekit-ir-compiler-{x86-64,wasm,c,stub,jvm-bytecode},provekit-ir-codegenprovekit-lift-{asm-aarch64,asm-x86-64,evm-bytecode,jvm-bytecode}Keep:
provekit-ir-compiler(parent) +-smt-lib/-coq/-lean/-maude(discharge backends, in scope).cargo check --workspaceclean; ~17.8K lines removed. Independent of the.invariantPR (#1541).🤖 Generated with Claude Code
Summary by CodeRabbit