(offer to help) installation via VSCode on mac M1

[cdstanford]

I was wondering if I could help with anything to make the installation via VSCode work more smoothly on mac. Are there known tracking issues currently with this process that I may have missed?

My installation seems to be set up now, but I wasn't able to get it working initially, and I'll share some details below. I'm sure I did some things wrong, but it wasn't obvious at first.

The extension initially installed but silently produced no output (not catching assertion violations). Later it prompted that the installation of dotnet was not found. I got the following error:

/usr/local/share/dotnet/dotnet is not a compatible dotnet file. Dafny requires the ASP.NET Core Runtime 5.0 or 6.0, got Microsoft.AspNetCore.App 8.0.0-rc.1.23421.29 [/usr/local/share/dotnet/shared/Microsoft.AspNetCore.App] Microsoft.NETCore.App 6.0.11 [/usr/local/share/dotnet/shared/Microsoft.NETCore.App] Microsoft.NETCore.App 8.0.0-rc.1.23419.4 [/usr/local/share/dotnet/shared/Microsoft.NETCore.App]

The error did not go away when installing .NET via the official website, using the provided link, even after uninstalling/reinstalling extensions and restarting VSCode.

What seemed to work was running brew install dotnet-sdk, uninstalling and reinstalling all the relevant vscode extensions, and restarting VSCode. Now I am correctly finding assertion violations.

My setup: I'm running on a MacBook Air (M1 chip, 2020) with VSCode version: 1.82.3 (Universal). Additional details:

Commit: fdb98833154679dbaa7af67a5a29fe19e55c2b73
Date: 2023-10-02T11:06:17.496Z (1 wk ago)
Electron: 25.8.1
ElectronBuildId: 24153832
Chromium: 114.0.5735.289
Node.js: 18.15.0
V8: 11.4.183.29-electron.0
OS: Darwin arm64 21.4.0

Thanks!

[keyboardDrummer]

It looks like the version check in the Dafny extension is too strict. The dotnet you installed (8.0.0-rc.1.23421.29) was fine but our extension deemed it incorrect. I will mark this as a bug and we'll try to get a fix out soon.

For whomever is trying to fix this: Dafny is checking for the AspNetCore runtime even though I believe our binary only requires NETCore. Also it checks for version 5 or 6, while I think we should check for anything >= 5. Also, if the check fails, I think we should allow the user to try and start with this dotnet installation, instead of always stopping.

I was wondering if I could help with anything to make the installation via VSCode work more smoothly on mac.

Detailed bug reports like this one are a great start, thanks ! For a critical bug like this one, we'll find someone on the Dafny core team to work on it. Feature requests are also welcome. If there's a requested feature that I think we won't get to anytime soon I will let you know and give you a sketch of what it would entail to make it.

[alex-chew]

Thanks for the detailed report @cdstanford, and thanks for the tips @keyboardDrummer! I've opened a PR (#443) to check for just the .NET Runtime instead of ASP.NET Core, and to permit any major versions >= 5. On the other hand I've opted not to allow the extension to proceed despite failing the version check, as I feel that it's better to fail fast than to let users use an incompatible .NET version unwittingly.

[alex-chew]

We've just released version 3.2.1 that includes a patch for this issue. It should appear in the VS Marketplace shortly, after which restarting your IDE should cause it to install the update.

[cdstanford]

Wow, awesome -- thanks so much for the responsiveness and quick fix! I will definitely try out the most recent version. Will file another report if I notice anything else.

Detailed bug reports like this one are a great start, thanks ! For a critical bug like this one, we'll find someone on the Dafny core team to work on it. Feature requests are also welcome. If there's a requested feature that I think we won't get to anytime soon I will let you know and give you a sketch of what it would entail to make it.

Got it & sounds good!

[tchajed]

Wait, Dafny supports dotnet 7? This isn't documented anywhere, the INSTALL page asks for dotnet 6, and the Homebrew formula still depends on dotnet@6.

[keyboardDrummer]

Wait, Dafny supports dotnet 7? This isn't documented anywhere, the INSTALL page asks for dotnet 6, and the Homebrew formula still depends on dotnet@6.

It does and I think it supports .NET 8 as well. Given the backwards compatibleness of .NET I think it's likely Dafny will work with any future version.

Created a ticket to update the things you mentioned: dafny-lang/dafny#4685