Enable configuring the Dafny version in the Dafny project file #3848
Labels
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: CLI
interacting with Dafny on the command line
status: needs-approval
Issue that needs approval from Dafny team members before moving to designed
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
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 adotnet-tools.json
file, and then dodotnet tool run dafny
, after which it terminates itself.Users will see the
dotnet-tools.json
show up when doinggit 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 singledafny 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 startdafny server
without inspecting any project files.The best way to make
dafny server
upgrade versions is to let it install and start otherdafny 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.The text was updated successfully, but these errors were encountered: