Diagnostics are shown for all files in explicitly defined Dafny projects

[keyboardDrummer]

Change

Enable customers to define which .dfy files belong together as part of a Dafny 'project'. When any file in a project is opened, show diagnostics for all files in that projects.

Which files a project contains can be done by specifying a root folder. All .dfy files under the root folder are part of the project. The root folder is specified by placing a dafny.toml file in that folder. The dafny.toml file can be empty and its contents are ignored.

The Dafny IDE should watch for file changes that could affect which Dafny projects the currently opened files are in, such as the removal or addition of dafny.toml files. In this case offering to restart the LSP server with the new file contents is fine.

Related issue: dafny-lang/ide-vscode#82

Not in scope

• Using the contents of the Dafny project file
• Allow configuring file filters to select which files within a root folder are part a project.
• Enable specifying the Dafny version a project is built.
• Enable configuring all sorts of project related information such as author, version etc.

Prerequisites

• Enable configuring Dafny options through a project file #2907
• Let unsaved changes from included files be taken into account by the language server #4111

Implementation suggestions

• When the language server starts processing a file, which is done in DocumentManagerDatabase, traverse up the file's path to see if a dafny.toml is present. If such a file is found, use this file's Uri to lookup a DafnyProject (currently named DocumentManager). If no such file is found, use the file's Uri for the lookup instead. If no DafnyProject is found, create one, either using the previously found project file or using an implicit project file.
• Compilation needs to take a ProjectFile as input instead of a DocumentTextBuffer textBuffer, and the information from that is used to change which DafnyFiles are passed to ProgramParser.ParseFiles. This will also set the IsPreverified property on those DafnyFiles so that library files are not verified.
• IdeState needs to be updated so it can hold diagnostics for more than one file. Document.ToIdeState and its overrides need to be updated to fill in the extra information.
• Document will no longer hold a DocumentTextBuffer, but instead a Dictionary<Uri, DocumentTextBuffer>, and no longer a single VerificationTree, but one for each file.
• DocumentManager (which we'll rename to DafnyProject), will have its fields updated to reflect that is handles multiple files List<Position> ChangedVerifiables { get; set; } = new(); and List<Range> ChangedRanges { get; set; } = new(); need the Position and Range to include a Uri as well, and the code that uses these fields to determine the order in which verification tasks are evaluated, is updated to use the new types.

[cpitclaudel]

such as the removal or addition of dafny.toml files.

I wonder how IDEs deal with this. Does Rider get confused if you remove a csproj, for example?
I think we don't need to be too smart about this; we could simply offer to restart the server in that case.

[keyboardDrummer]

such as the removal or addition of dafny.toml files.

I wonder how IDEs deal with this. Does Rider get confused if you remove a csproj, for example? I think we don't need to be too smart about this; we could simply offer to restart the server in that case.

Some IDEs require explicitly opening a project file before they provide their full functionality. The LSP protocol however doesn't have such as open step. An LSP server is expected to respond to file system changes that affect the semantics of files that are open in the LSP client.

An example is opening a .ts file without a tsconfig.json being present. The TypeScript server starts immediately when you open the .ts file, but once you add a tsconfig.json next to it, the typechecking is restarted.