runtimeverification / runtimeverification/mir-semantics
Add `--target-dir` option for `prove-rs`, do not reduce `smir.json`
Open
@palinatolmach is already working on this.
Since Nov 6, 2025.
- Dominant language
- Python
- Stars
- 52
- Forks
- 5
- PR merge metrics
- No merged PRs in 30d
Description
We should add the --target-dir option to prove-rs, similarly to how it's done for run in https://github.com/runtimeverification/mir-semantics/pull/777; it should be used instead of reduce_to. That's based on the suggestion made by @Stevengre:
Since it costs a lot of time to prepare the kmir , what do you think that we provide a file level from_kompiled_kore without reduce_to(start_symbol). Then, we can reuse the kmir for different functions in one file.
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.