VS code Dafny broken - will no longer install

[kjx]

Dafny-VScode will no longer install. On MacOS at least, it stops at 4% "Extracting Dafny" with the following error - Seems related to #29. With no option to specify a different Dafny, there's no way to get a working system, or get back a working system after agreeing to an "upgrade".

Extracting files...
Error extracting /Users/kjx/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/dafny.zip: Error: Unsupported file type "undefined"
Error: Unsupported file type "undefined"
at DecompressZip.extractFile (/Users/kjx/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/server/node_modules/decompress-zip/lib/decompress-zip.js:320:11)
at /Users/kjx/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/server/node_modules/decompress-zip/lib/decompress-zip.js:253:28
at Array.forEach ()
at DecompressZip.extractFiles (/Users/kjx/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/server/node_modules/decompress-zip/lib/decompress-zip.js:252:11)
at /Users/kjx/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/server/node_modules/decompress-zip/lib/decompress-zip.js:132:21
at _fulfilled (/Users/kjx/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/server/node_modules/q/q.js:854:54)
at /Users/kjx/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/server/node_modules/q/q.js:883:30
at Promise.promise.promiseDispatch (/Users/kjx/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/server/node_modules/q/q.js:816:13)
at /Users/kjx/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/server/node_modules/q/q.js:624:44
at runSingle (/Users/kjx/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/server/node_modules/q/q.js:137:13)
errrroooorrr: Error: Unsupported file type "undefined"

[prashantbarca]

Yes, I am facing the same issue on VSCode 1.47.3 as well as 1.48.

[brady-ds]

In a class I'm teaching, we found that this was a problem for many students on Windows and macOS.

Our workaround on Windows was:

1. Delete the contents of %HOMEPATH%\.vscode\extensions\correctnesslab.dafny-vscode-0.17.2\dafny, if any.
2. Manually download Dafny from its "Releases" page on GitHub.
3. Right-click on the archive in File Explorer, choose "Properties", and under the "General" tab tick the "Unblock" checkbox in the "Security" section at the bottom.
4. Extract the contents of the archive and copy the dafny folder so that it becomes %HOMEPATH%\.vscode\extensions\correctnesslab.dafny-vscode-0.17.2\dafny\dafny.
5. In VSCode, manually change the "Dafny: Base Path" setting to %HOMEPATH%\.vscode\extensions\correctnesslab.dafny-vscode-0.17.2\dafny\dafny (filling in %HOMEPATH% with the actual absolute path to your home directory).

Similarly, our workaround on macOS was:

1. Delete the contents of ~/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/dafny, if any.
2. Manually download Dafny from its "Releases" page on GitHub.
3. Extract the contents of the archive and copy the dafny folder so that it becomes ~/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/dafny/dafny.
4. In VSCode, manually change the "Dafny: Base Path" setting to ~/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/dafny/dafny (replacing ~ with the actual absolute path to your home directory).
5. Try verifying a program. macOS will complain that one of the Dafny binaries is not trusted. When that happens, open "System Preferences" → "Security & Privacy", and on the "General" tab click the button to allow the binaries to run. You may have to repeat this process for several binaries until Dafny can run successfully.

[kjx]

so I've tried that just now - I'm glad it works for you but it doesn't work for me.

I can unpack the dafny.zip myself alright, or copy from the main installation zip
either way, when I restart VS Code, I get asked to install dafny again.
If I say yes, we're back to where we started;
if I say no, the highlighting works but not the actual checking.
I'm on VScode 1.48 and macos 10.15.6 - J

[fabianhauser]

Thanks for your reports!

I assume this is related to the release of the latest preview release of Dafny and the automatic downloader. We will look into pinning the version to the latest stable release for the time beeing...

[fabianhauser]

Related Issue: #29

[kjx]

@fabianhauser - no problem, it's a great tool, and we have 90 students depending on it in our course in NZ.
It's worked out really well so far!

I assume this is related to the release of the latest preview release of Dafny and the automatic downloader. > We will look into pinning the version to the latest stable release for the time beeing..

yes that seems to be it. ideally Rustan would have a "stable" release branch or whatever git does for that.

the right thing™ is probably to make ReleaseURL an extension setting like the existing Dafny path etc;
that way people can point the plugin at whichever release they need...

[fabianhauser]

@RustanLeino is it okay if I mark the 3.0.0 release on in the dafny-lang/dafny Repo as a "Preview Release"? We could filter out pre-releases on our part. (This is a checkbox on the Github Releases page).

[fabianhauser]

the right thing™ is probably to make ReleaseURL an extension setting like the existing Dafny path etc;
that way people can point the plugin at whichever release they need...

@kjx Absolutely, I agree. We are currently working on a major new release of the plugin, were this should be supported 🙂

[brady-ds]

@kjx I failed to mention that we were downloading version 2.3.0, not the prerelease. Sorry about that. Given the discussion above, perhaps my omission was why the workaround didn't work for you?

[kjx]

pretty sure I tried with both 2.3.0 & 3.0.0 pre.
the problem seems to be that VS doesn't recognise that the installation is complete,
even after I manually replace the subdirectory. So it just asks me to install Dafny again.

[prashantbarca]

I can verify that the solution @brady-ds suggested does work on Ubuntu versions 16.04, 18.04, and 20.04! Thanks!

[kjx]

I bet it's Mac weirdness I don't have time to hunt down now.

there seems to be stuff in ~/Library/Application Support/Code/User/ too, but I don't know how that works,
nor why that would let restoring a .vscode directory works but patching it doesn't.

I can restore from a time machine backup, or a cp -r of that backup of the whole vscode.
I haven't managed to slice individual extensions.

I'm on VScode 1.48 and macos 10.15.6. I had a student say a version of that workaround did work OK, but he was on 10.12.something. Dunno if I'm just missing something, or what.

[brady-ds]

@kjx For one of my students on macOS just now we had to

$ cd ~/.vscode/extensions/correctnesslab.dafny-vscode-0.17.2/dafny/dafny
$ ./dafny /?
$ # Click "Cancel" on the popup and allow z3 to run in "System Preferences" → "Security and Privacy".
$ ./dafny /?
$ # Click "Open" on the popup.

and then restart VSCode. Maybe worth trying?

[hmijail]

@brady-ds 's solution worked for me with Dafny 3.0.0 pre-release 0a on macOS 10.15.6.
Note that ./dafny /? fails in macOS 10.15's zsh because it tries to parse the /? as a wildcard. ./dafny and ./dafny "/?" worked for me.

For completeness, I also tried directing the Dafny Extension's path to a Dafny 2.3.0 installed by Homebrew. It didn't work, no idea why.

[hmijail]

Correction: Dafny 3.0.0. pre-release seems to work, but looks like there is some weirdness going on - proofs that worked now fail. I'm too newbie to make sense of it.
Dafny 2.3.0 doesn't show that weirdness. VSCode will suggest updating on startup, but you can just answer "no".

[kjx]

So I tried again on a fresh account; same problem. I unpack dafny but the extension still doesn't recognise dafny is there. dunno why

[kjx]

@hmijail I also tried to point to other dafnys - also didn't work.

[kjx]

So: I'm back going again! Reinstalling VS Code or just the plugin doesn't seem to work on the Mac, but this worked repeatably for me, based on https://www.thetopsites.net/article/53839847.shtm, and having a working dafny installed somewhere else (2.3.0 from home-brew, or 3.0.0.20820 from GitHub zip)

1. Quit vscode
2. Clear our all user information I could find
   rm -fr ~/Library/Preferences/com.microsoft.VSCode.helper.plist
   rm -fr ~/Library/Preferences/com.microsoft.VSCode.plist
   rm -fr ~/Library/Caches/com.microsoft.VSCode
   rm -fr ~/Library/Caches/com.microsoft.VSCode.ShipIt/
   rm -fr ~/Library/Application\ Support/Code/
   rm -fr ~/Library/Saved\ Application\ State/com.microsoft.VSCode.savedState/
   rm -fr ~/.vscode/
3. Install the Extension on the command line
   /Applications/Visual\ Studio\ Code.app/Contents/Resources/app/bin/code --install-extension ~/Downloads/correctnessLab.dafny-vscode-0.17.2.vsix
4. Restart VSCode
5. Say "No" to downloading Dafny, but update extension setting for the Dafny Server Path to the directory holding DafnyServer.exe

[fabianhauser]

I just released Dafny-VSCode v1.18.0 with a pinned Dafny Version 2.3.0 (and created an issue to remove the fix once 3.0.0 is stable: #67).

That should suffice to fix the error for the time being - when we release the new language server / vscode plugin, this will be solved differently either way.

@kjx @prashantbarca @hmijail @brady-ds could you try if that solved the error for you? It's possible you have to roll back some manual changes you did to the extension configuration (and/or reinstall the extension.)

[kjx]

@fabianhauser @RustanLeino I've tried this in several different ways across two mac accounts.
seems to work every time - even managing to unwedge the schrödinger's installation
(both installed and not installed...) although I had to muck around a bit first to get back to
the wedged configuration...

trick for young players is that at least half the time it upgrades the VS extn without asking first
which isn't great if things somehow end up wedged again, but should be great to get us out of this mess