You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
The text was updated successfully, but these errors were encountered:
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
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
The text was updated successfully, but these errors were encountered: