We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Tell us what version of K you are using.
Example:
% kompile --version K version: 5.1.161 Build date: Thu Aug 26 17:10:51 UTC 2021
Running kprovex with the --debugger and/or --debug-script options does not put the Haskell backend into kore-repl mode.
kprovex
--debugger
--debug-script
Example spec file test.k:
test.k
requires "domains.md" module TEST imports INT imports BOOL configuration <k> $PGM:Step </k> syntax Step ::= run ( Bool ) | done ( Bool ) // -------------------------------------------- rule <k> run(true) => done(true) ... </k> rule <k> run(_) => done(true) ... </k> [owise] endmodule module TEST-SPEC imports TEST claim <k> run(false) => done(true) ... </k> endmodule
Kompile and run the proof with kprovex:
% kompile test.k --main-module TEST --syntax-module TEST --backend haskell % kprovex test.k --spec-module TEST-SPEC #Top
The proof passes.
We should be dropped into the kore-repl instead, to be able to debug the proof.
kore-repl
The text was updated successfully, but these errors were encountered:
radumereuta
Successfully merging a pull request may close this issue.
K Version
Tell us what version of K you are using.
Example:
Description
Running
kprovex
with the--debugger
and/or--debug-script
options does not put the Haskell backend into kore-repl mode.Input Files
Example spec file
test.k
:Reproduction Steps
Kompile and run the proof with
kprovex
:The proof passes.
Expected Behavior
We should be dropped into the
kore-repl
instead, to be able to debug the proof.The text was updated successfully, but these errors were encountered: