Skip to content
New issue

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

Proof won't rerun lemmas unless lemmadb cleared and prover restarted by hand #77

Open
rbohrer opened this issue May 31, 2021 · 0 comments

Comments

@rbohrer
Copy link
Member

rbohrer commented May 31, 2021

When uploading a .kyx file which contains lemmas that get useLemma'd by its main proof, KeYmaera X will not detect if I've changed a lemma, specifically it will not detect that the lemmas should be rerun if I attempt a proof of the main theorem again.

On it's own, that's not surprising, but what's surprising is that it will not detect this even if I delete all proofs and models. The reason for this is (I assume) that the "need to run proofs of lemmas" check relies on the lemmadb on the filesystem, which is not cleared when running the "delete all models and proofs" button.

Sometimes it doesn't work unless I also restart the prover. I assume something is getting cached in memory (either SQLite DB or lemma DB) so it doesn't read from disk again until you restart the prover

@rbohrer rbohrer changed the title Proof won't rerun lemmas unless lemmadb cleared by hand Proof won't rerun lemmas unless lemmadb cleared and prover restarted by hand May 31, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant