This repository has been archived by the owner on Apr 25, 2024. It is now read-only.
Add proof exploration and display options to CLI #1043
Closed
Conversation
This file contains 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
…ng execution depth
…ng off proof artifacts
… kprove --dry-run
…ss needs to be made on proof
ehildenb
force-pushed
the
proof-functionalities
branch
from
2a3b4fe to
17e88ae
Compare
ehildenb
changed the title
ehildenb
changed the title
rv-jenkins
pushed a commit
to runtimeverification/k
that referenced
this pull request
Apr 16, 2024
Transfer of: runtimeverification/pyk#1043 This PR is for making it easier to work on proofs with default `pyk prove ...` functionalities. - Factor out and reuse `SpecOptions` in `ProveOptions` class. - Add options to `pyk prove`: - `--max-iterations`: control how many iterations of proof extension to do. - `--max-depth`: control the maximum number of steps to take in an `execute` request. - `--save-directory`: allow saving off the proof state after executing it. - `--temp-directory`: allow setting the temporary directory to use for intermediate artifacts. - `--show-kcfg`: display the resulting proof KCFG after executing the proof. - Handle the `RuntimeError` thrown by crashes of the call to `kprove --dry-run ...` directly and more gracefully, instead of printing a stack trace. - Add command `pyk show` which reuses a lot of the same options as `pyk prove`, and calls `pyk prove` in a way that it just loads the proof from disk and displays the KCFG. - Changes to the `KProve.prove_rpc` functionality: - Source many of the options from the `ProveOptions` class, which contains the above options and more. - Only initialize a `CTermSymbolic` (and thus an RPC server) if it's needed (will take more than 0 proof steps, and the proof isn't already passed). - Allow setting the prefix of the temporary file parsed to for `get_claims_modules`. - Modify a test in `regression-new` to exercise the new `pyk prove --show-kcfg ...` option. --------- Co-authored-by: Everett Hildenbrandt <[email protected]>
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.
This PR is for making it easier to work on proofs with default
pyk prove ...functionalities.SpecOptionsinProveOptionsclass.pyk prove:--max-iterations: control how many iterations of proof extension to do.--max-depth: control the maximum number of steps to take in anexecuterequest.--save-directory: allow saving off the proof state after executing it.--temp-directory: allow setting the temporary directory to use for intermediate artifacts.--show-kcfg: display the resulting proof KCFG after executing the proof.RuntimeErrorthrown by crashes of the call tokprove --dry-run ...directly and more gracefully, instead of printing a stack trace.pyk showwhich reuses a lot of the same options aspyk prove, and callspyk provein a way that it just loads the proof from disk and displays the KCFG.KProve.prove_rpcfunctionality:ProveOptionsclass, which contains the above options and more.CTermSymbolic(and thus an RPC server) if it's needed (will take more than 0 proof steps, and the proof isn't already passed).get_claims_modules.regression-newto exercise the newpyk prove --show-kcfg ...option.