Enable configuring the Dafny version in the Dafny project file

[keyboardDrummer]

Enable configuring the Dafny CLI version to use in the Dafny project file

If the CLI version matches the version specified in the project file, continue as normal. Otherwise, write to stdout that the wrong Dafny version is used, and prompt the user whether to continue with the wrong one, update to the right one, or stop.

If a project is opened using dafny server where the two don't have matching versions, dafny server will send a showMessage notification that informs the user about the problem. dafny server won't have the option to automatically update to the right version. More details on why are in the implementation sketch.

Prerequisites

• https://github.com/dafny-lang/dafny/issues/2907

Implementation sketch

Let the Dafny CLI do a call to dotnet tool install dafny --version=<version configured in the project file>, which will locally create a dotnet-tools.json file, and then do dotnet tool run dafny, after which it terminates itself.

Users will see the dotnet-tools.json show up when doing git status, and may choose to add it to their .gitignore.

---

Allowing dafny server to automatically update to the right version is complicated, since a standard LSP client will run a single dafny server for multiple open Dafny files, that may belong to different projects that use different Dafny versions. Also, it's preferable for the IDE to remain Dafny agnostic when possible, which means it should be able to start dafny server without inspecting any project files.

The best way to make dafny server upgrade versions is to let it install and start other dafny server processes and proxy LSP requests from those.

Alternatively, the IDE can use a custom LSP client that understands Dafny project files, and is able to run different dafny server instances for different files it has opened.

[robin-aws]

Interesting idea! My gut says it would be smarter to only do this only in an interactive setting, so the user could acknowledge they want this convenient behavior. In CI I could imagine folks getting really confused if they use something like setup-dafny-action to unknowingly download the wrong version and yet it still works.

How would this work in the dafny server case?

Is there precedent for this in other language tooling?

[keyboardDrummer]

My gut says it would be smarter to only do this only in an interactive setting

Sounds good, we can make it interactive.

How would this work in the dafny server case?

It wouldn't, unless you put in a lot of effort ^,^ added more details.

[robin-aws]

+1 on the new details. I think the important functionality is for dafny to check that it is the right version for the given project file and fail if not, and interactively offering to upgrade itself is just a nice cherry on top.

[robin-aws]

The best way to make dafny server upgrade versions is to let it install and start other dafny server processes and proxy LSP requests from those.

That might be the best way to pick up project files in general too, especially if the VS Code extension only gets to instantiate one top-level server. The top-level server could spawn a child server once a file is opened and a project file discovered. That would naturally support multiple windows with unrelated projects as well.

[keyboardDrummer]

The best way to make dafny server upgrade versions is to let it install and start other dafny server processes and proxy LSP requests from those.

That might be the best way to pick up project files in general too, especially if the VS Code extension only gets to instantiate one top-level server. The top-level server could spawn a child server once a file is opened and a project file discovered. That would naturally support multiple windows with unrelated projects as well.

That's what I meant 😄

But I think for some time, it'll be more practical to only warn the user that their IDE is using a newer Dafny version than what their project is configured for, and that verification results may differ for complex proofs.