Dafny lag when typing

Apr 8, 2014 at 12:39 PM
Hi,

I am experiencing some lag when typing into a dfy file in visual studio with Dafny 1.8.1.10324

My file is 877 lines, including perhaps 20% comments and is split into 3 modules. Sometimes it is several seconds after I type that the characters appear on the screen.

I guess the lag has something to do with either the parser or the type checking or the verification kicking in whilst I am typing, but I do not know how to diagnose it further.

Cheers,

Tim
Apr 9, 2014 at 12:52 PM
Edited Apr 9, 2014 at 12:54 PM
Hi,

I think that perhaps it is related to some kind of leak. If I restart visual studio the lag goes away, but then after about 1-2 hours of using Dafny the lag starts to increase again.

I have noticed that, when I type, before the characters appear on the screen I can see the "Col" and "Ch" counters in the visual studio editor incrementing slowly. Then eventually all the characters appear on the screen at once.

If I do not restart visual studio the lag seems to get progressively worse and worse as I make more edits.

Cheers,

Tim
Developer
Apr 9, 2014 at 6:25 PM
We've noticed this problem as well. I agree that it's probably a resource leak inside the VS extension somewhere. The one useful tip I can offer is that typically closing and reopening the file resets the performance; you don't need to restart VS itself.
Apr 10, 2014 at 8:43 AM
OK thanks.

When I close the file and reopen it (or restart VS) then Dafny is unable to verify various parts of my program due to time outs. What I have to do is put "assume false" in the top of some of the larger methods/lemmas, wait for it to verify everything else then remove each "assume false" one at a time. Then everything verifies. Is this an OK thing to do?

Is sharing my experiences of using the Dafny extension here useful for you at all?
Developer
Apr 10, 2014 at 10:29 PM
To keep things interactive, the extension has a fixed time limit for how long it will spend attempting to verify your code. It also does some intelligent caching, so if you only change one method, it re-verifies that method, and those that depend on it, but not the whole file. Your strategy is making use of these two items to get the whole file to verify, which is fine, though tedious, I imagine. You may want to consider breaking up your methods and lemmas into smaller pieces and/or trying out the calc statement to speed up some of the proofs. I might also suggest using "assert false;" instead of "assume false". You'll get the same effect, but you'll get one error on the assert, which will keep you from accidentally leaving an assume in.
Apr 29, 2014 at 5:02 PM
Edited Apr 29, 2014 at 5:02 PM
Some further notes on techniques I am using to work around the verification timeouts in the VS extension:
  1. I am using "method {:verify false} myMethod()" to disable verification for parts of the proof that I am not currently working on.
  2. I am using refinement, includes and imports to split the proof across multiple modules and files.
  3. If a lemma takes too long to verify, I mark it with {:verify false} in VS whilst working interactively. At the end I do a global find and replace of {:verify false} with {:verify true} and run everything through the command line verifier.