Update VS Code plugin gif

[robin-aws]

The super-swanky animation here needs to be updated: https://github.com/dafny-lang/dafny/wiki/INSTALL#visual-studio-code The latest version of the plugin released yesterday has much more explicit information about the download process:

starting Dafny installation
deleting previous Dafny installation at /Users/salkeldr/.vscode/extensions/correctnesslab.dafny-vscode-2.0.0/out/resources
downloading Dafny from https://github.com/dafny-lang/dafny/releases/download/v3.3.0/dafny-3.3.0-x64-osx-10.14.2.zip
0%...10%...20%...30%...40%...50%...60%...70%...80%...90%...100%
extracting Dafny to /Users/salkeldr/.vscode/extensions/correctnesslab.dafny-vscode-2.0.0/out/resources
0%...10%...20%...30%...40%...50%...60%...70%...80%...90%...100%
Dafny installation completed
starting Dafny from /Users/salkeldr/.vscode/extensions/correctnesslab.dafny-vscode-2.0.0/out/resources/dafny/DafnyLanguageServer.dll
Dafny is ready

[MikaelMayer]

How do you like the current one? I just updated it a few minutes ago.

[camrein]

Just my two cents: I like how you illustrate how the extension helps you fix the verification error. However, I think you should keep the installation terminal open so people are aware of the complete installation procedure. As an additional note. The installation messages @robin-aws mentioned will only be displayed for the automatic installation. If you have set the extension to point to a custom DafnyLanguageServer.dll, the extension will skip the installation.

[MikaelMayer]

What do you mean by "so people are aware of the complete installation procedure"? What complete installation procedure are you talking about? On my side, even after deleting the extension, sometimes it automatically suggests to install Dafny, sometimes it's not, so it's not something we should rely on. But I don't think I set it to point to a custom DafnyLanguageServer because I did not solve yet my previous problem we discussed about in the other thread.

[camrein]

What do you mean by "so people are aware of the complete installation procedure"? What complete installation procedure are you talking about?

The output Robin mentioned will only be displayed if the language server is re-installed. That's what I mean with "complete installation".

On my side, even after deleting the extension, sometimes it automatically suggests to install Dafny, sometimes it's not, so it's not something we should rely on.

Unfortunately, VSCode does not remove additional resource files created by the extension itself. That's the issue you're observing here. For clarification: If you have a completely fresh installation of VSCode (side-note: VSCode stores extensions in a profile specific dir, so it's not necessarily fresh if you uninstall VSCode before as extensions might not be removed, or at least their additional resources), you can be sure that Dafny will be automatically installed when installing the extension. If you uninstall the extension, only the extension code is removed but not its resources (Dafny in this case). Therefore, you won't see the Dafny installation procedure upon reinstalling the extension.

For reference, by default the installed VSCode extensions are located at:

# Windows
%userprofile%\.vscode\extensions

# Unix
~/.vscode/extensions

The Dafny extension installs Dafny into correctnesslab.dafny-vscode-<version>/out/resources. Therefore, if you remove this directory, you should see the automatic installation of Dafny again.

Personally, I don't like that VSCode preserves extension files even after their uninstallation. But this seems to be "accepted" behavior. For example, you see the same for the official C# extension. You'll also find some StackOverflow questions about this.

[MikaelMayer]

Your point is, if I prune the terminal of installation from the animated screenshot, users might be confused that the terminal opens?

I did remove the directory correctnesslab.dafny-vscode-<version>/out/resources, and I did not see the automatic installation of Dafny again after restarting Visual Studio Code and opening a dfy file;

[camrein]

Your point is, if I prune the terminal of installation from the animated screenshot, users might be confused that the terminal opens?

I just thought we shouldn't hide the fact that there is some procedure necessary after the extension was installed. Moreover, I think users should be aware of this more verbose installation status since there were users with problems in the past. For example, see https://github.com/dafny-lang/ide-vscode/issues/38.

I did remove the directory correctnesslab.dafny-vscode-<version>/out/resources, and I did not see the automatic installation of Dafny again after restarting Visual Studio Code and opening a dfy file;

That's strange. If that's the case, your language server might be loaded from somewhere else. You can disclose the location from where the language server is loaded by opening Output -> Dafny VSCode, you'll see something like:

starting Dafny from c:\Users\chamr\.vscode\extensions\correctnesslab.dafny-vscode-2.0.0\out\resources\dafny\DafnyLanguageServer.dll
Dafny is ready

If you see the installation output in this terminal, there might be some setting/extension that has a higher priority than the terminal created by the Dafny extension. That could explain why you only see the installation messages sporadically. (Side-note: VSCode initializes the Dafny extension only when a Dafny file is opened, otherwise it stays unloaded.)

[MikaelMayer]

I could not make the auto-installer to pop up even after full uninstall, manually deleting remaining files and full reinstall. It seems that this information has been stored somewhere else (in the registry) Anyway, I've updated the animated screenshot to display the terminal installation, and I removed the verification part because it's not part of the installation - the verification should be part of the README as per my pull request. https://github.com/dafny-lang/dafny/wiki/INSTALL