This project is read-only.


Frustrating wait for Dafny IDE to process changes


The new Dafny Visual Studio plugin waits for a noticeable amount of time (2 seconds?) before re-verifying newly written code, but I've come to find this delay frustrating. I'd like a button I can press (e.g., F11?) that will tell the plugin to start re-verifying right away rather than waiting.

Also, when I load a new file, or reload a file that I changed in another editor (say, emacs), I'd like to not have to wait for the 2-second delay. After all, the 2-second delay was introduced to avoid conflict with subsequent keystrokes, but a load or reload shouldn't be expected to be followed by keystrokes. So, if possible, I'd like the plugin to react to a notification that the file was loaded or reloaded by re-verifying immediately.
Closed Jun 16, 2016 at 7:47 PM by qunyanm


rustanleino wrote Jan 28, 2016 at 12:22 AM

I have noticed some longer delays, too, but I was too busy to investigate and just assumed my poor laptop's CPU was tied up. Now that you point it out, I'm looking at the remedy for Issue #122. I agree with what you said. I think we should switch this back.


parno wrote Jan 28, 2016 at 4:54 AM

It's tricky, because there have definitely been times with the new mode when I appreciated being able to type "in peace" without feeling like I was fighting to keep Dafny from rushing off prematurely. But there are also times when the lag is annoying. Seems like we need to think more about how to strike the right balance here.

parno wrote Feb 11, 2016 at 4:45 AM

We discussed various options in today's meeting. It sounds like the consensus is that we should go back to the shorter time limits that we used before, rather than the current 5 second delay before the resolver is invoked. We'll test it out to see if Qunyan's previous performance optimizations have eliminated the lag we saw previously. Frustrations with the decreased time limits may be mitigated by adding support for a key binding (e.g., F5) that would kill the current resolver/verifier process and start it fresh. This may require making the spawned processes part of a Windows "Job" object, rather than just raw threads/processes.

lexicalscope wrote Feb 11, 2016 at 9:37 AM

Personally, I would like an option to disable the automatic verifier invokation. Instead I would like to be able to always manually start the verifier by pressing a key (such as F5). There are often long periods where I know that the program will not verify - and during those times running the verifier is pointless and wastes my laptop battery.

It would be nice to still be informed of syntax or type errors during the time the verifier is disabled.

Another, perhaps related, feature that would be really helpful for me, would be to have a way to find out how long each lemma/function/method/etc took to verify. I usually want my proof to not only verify, but also to do so reasonably quickly. A few seconds per lemma quickly adds up to a proof that takes a long time to verify competely.

qunyanm wrote Jun 16, 2016 at 7:47 PM

The delay has been removed. You can also use F5 to stop/start verifier and F11 to stop/start resolver (including the verifier) manually.