Feature request: Dafny project file

[robin-aws]

This has come up in several contexts and I think the time is ripe to figure this out. The benefits include but are not limited to:

• Making it easier to define the set of Dafny files to build (meaning verify, compile, etc.)
• Documenting/locking down the version of Dafny your codebase should be built with.
• Maintaining the switches the codebase requires (for many codebases a switch like /definiteAssignment:3 is particularly critical)
• Providing more rigour around the different requirements between source and test code (as per this comment: Function by method bodies should not be allowed to contain expect statements #1376 (comment))
• Enabling a more standard build system for Dafny (rather than relying on things like Makefiles)

The dafny.msbuild task provides some of this functionality, but I suspect it's worth defining a separate if similar format rather than permanently squatting on a .NET-specific (or at least C#-specific) *.csproj file format.

[robin-aws]

Note also this is follow-up from #1426, as having a project file that declared the supported Dafny version would have prevented the plugin from "silently" (or at least fairly quietly) upgrading Dafny.

[parno]

@jaybosamiya also had some relevant thoughts on how this could impact the include system: #1236 (comment)

[keyboardDrummer]

I feel this ticket specifies a 'how' (use a project file) instead of 'what' (Enable a more standard build system for Dafny).

I think the benefits mentioned in the issue can be gotten by script file with a Dafny CLI call as well, given changes to the Dafny CLI. However, I can think of one thing that a project file can do that a script file with a Dafny CLI call can not, which is to provide an interface for sharing Dafny configuration between different Dafny tools, for example the CLI and the language server. This benefit isn't listed in this issue, but I think it's the most important reason to introduce a project file for Dafny.

A secondary reason for introducing a project file is I think to improve the UX of configuring a Dafny project. Configuration files allows specifying complex configuration in a readable way through textual tree structures, while specifying such information through the CLI can look clunky. More discussion can be found here.

[davidcok]

Completed with PR 3851