VS extension crashes

Sep 28, 2016 at 12:27 AM
When I create a text file in Visual Studio and then rename it with a .dfy suffix, the Dafny extension throws an exception and stops working as soon as I edit the file. Shutting down and restarting VS seems to correct the problem.
  • Is this a known bug?
  • Is there a way to stop this from happening?
  • Is there a better way to create Dafny files from within VS?
This is with version 1.9.7 of Dafny and several versions of VS.

The exception appears to be
System.Collections.Generic.KeyNotFoundException: The given key was not present in the dictionary. at System.Collections.Generic.Dictionary`2.get_Item(TKey key) at Microsoft.VisualStudio.Text.Editor.Implementation.GlyphMarginVisualManager.AddGlyph(IGlyphTag tag, SnapshotSpan span) at Microsoft.VisualStudio.Text.Editor.Implementation.GlyphMargin.RefreshGlyphsOver(ITextViewLine textViewLine) at Microsoft.VisualStudio.Text.Editor.Implementation.GlyphMargin.OnBatchedTagsChanged(Object sender, BatchedTagsChangedEventArgs e) at Microsoft.VisualStudio.Text.Utilities.GuardedOperations.RaiseEvent[TArgs](Object sender, EventHandler`1 eventHandlers, TArgs args)
Coordinator
Nov 29, 2016 at 1:28 AM
I have not heard of this bug before. Can you please file it on https://github.com/Microsoft/dafny?

You asked if there's a better way to create a .dfy file from within VS. I don't know of a simple way to do it. My (possibly mistaken) understanding is that this functionality requires building a project system plug-in. It's embarrassing that the hardest step in writing a simple Dafny program inside VS is the creation of the file. The best way I know to do it is to create a new text file and then do a Save As. In the Save As dialog, be sure to select "All types" as the type of file, since it will let you add the .dfy extension without VS adding yet another .txt after that.

Hmm, I was able to recreate your bug (in the most up-to-date version of Dafny). And also find a workaround: don't save the file as an empty file, but instead add an empty comment to the file before saving it:
//
Rustan