Cannot disable downloading precompiled Dafny

[tchajed]

I'm on an Apple Silicon mac. I wanted to use Dafny through Docker, which is Linux on arm64, and the extension fails to set up Dafny because this isn't a platform that Dafny provides a binary release for. I have Dafny compiled within this Docker image, but I don't know how to direct the extension to use this local copy.

The README mentions dafny.languageServerRuntimePath but it isn't actually used by the extension.

I also tried setting the Dafny version to "custom" but then it just tries to install a URL that includes vcustom so I suspect this feature is buggy.

[furioncycle]

I actually was running into this, when I was wanting to package the extension in nixpkgs.

I was able to pull the extension but errors due to try to make a directory for the compiler to be downloaded. I tried to use the user settings but it seemed it was ignored and still tried to download a compiler.

[keyboardDrummer]

If you set the version to custom:

And configure a CLI path:

Then the extension will use the Dafny executable that you've pointed to.

[furioncycle]

Adding custom worked to my user settings and adding dafny bin but I seem to now get the following

Dafny Language Server client: couldn't create connection to server. Launching server using command /tmp/vscode-dafny-dlls-0969fE/dafny failed. Error: spawn /tmp/vscode-dafny-dlls-0969fE/dafny ENOENT

Do you know why this might be the case?

[keyboardDrummer]

Error: spawn /tmp/vscode-dafny-dlls-0969fE/dafny ENOENT

Indicates that node could not find the executable file /tmp/vscode-dafny-dlls-0969fE/dafny. Is that file there?

Here's a thread about this type of error: https://stackoverflow.com/questions/27688804/how-do-i-debug-error-spawn-enoent-on-node-js

What operating system are you on?

[furioncycle]

Error: spawn /tmp/vscode-dafny-dlls-0969fE/dafny ENOENT

Indicates that node could not find the executable file /tmp/vscode-dafny-dlls-0969fE/dafny. Is that file there?

Here's a thread about this type of error: https://stackoverflow.com/questions/27688804/how-do-i-debug-error-spawn-enoent-on-node-js

What operating system are you on?

I noticed that folder location is made in my vscode workspace. Why would it need to spawn that?

I am running Nixos

[keyboardDrummer]

I noticed that folder location is made in my vscode workspace. Why would it need to spawn that?

That is meant to make it easier to use a Dafny built from source using the custom option. By copying the binary to a fresh location before running it, the binary can be rebuilt while VSCode is using the copy.

@MikaelMayer I'm not a big fan of this approach. I use the DAFNY_DEV_SERVER environment variable instead of custom when running against builds from source, which doesn't do the copying anyways. Do you think we could remove the copying for the 'custom' option?

[RiscadoA]

Error: spawn /tmp/vscode-dafny-dlls-0969fE/dafny ENOENT

Indicates that node could not find the executable file /tmp/vscode-dafny-dlls-0969fE/dafny. Is that file there?
Here's a thread about this type of error: https://stackoverflow.com/questions/27688804/how-do-i-debug-error-spawn-enoent-on-node-js
What operating system are you on?

I noticed that folder location is made in my vscode workspace. Why would it need to spawn that?

I am running Nixos

I had the exact same problem, also on NixOS. After reading the extension's source code I managed to find the source of the error - take a look at #502. A bit off topic to the actual issue here, but there might be other people with the same issue.

[keyboardDrummer]

Closing this since I think the two underlying issues (lack of documentation and in-extension hints), and an incorrect file filter, are resolved. Big kuddos to @RiscadoA for contributing.