Enable configuring Dafny options through a project file

[keyboardDrummer]

Problems

• It's not possible to open a Dafny project in the IDE and automatically let the IDE use the correct Dafny options for this project.
• When calling the Dafny CLI on a Dafny project, the correct options for this project always have to be specified, which means most Dafny project needs to use a wrapping build tool like Make or a Bash script to enable easily invoking the Dafny CLI.

Prerequisites

• Introduce dafny server command #2906

Out of scope

• Enable specifying the Dafny version to use in the project file

Solution

Enable specifying options to the Dafny CLI in a Dafny project file, which can be passed as an argument when calling the Dafny CLI, also when using the dafny server command.

[robin-aws]

Why is #2906 a prerequisite? I would think if anything it would be in the other direction, and even then that the first version of dafny server could just accept the same style of CLI arguments as other dafny commands at first.

[robin-aws]

Some notes on requirements and scoping down the initial version of this:

• The initial target should be being able to provide some of the most common CLI options users tend to specify in their Makefiles.
• We should have a principle of configuring options for the overall project, rather than configuring individual commands.
  • Along those lines, not all possible options make sense to include in the project file. --no-verify for example, should remain a CLI option for a particular command invocation context. You shouldn't be able to say "this project is configured to never be verified".
• The design should allow for supporting more options in the future, especially those that future additional top-level Dafny commands will require, or even other third-party plugins or tools.
  • This especially applies to the dafny-reportgenerator tool, which relies heavily on configuring project-specific thresholds, and is likely to become its own dafny report command in the future.
• An interesting suggestion from @keyboardDrummer as we decide on what file format to borrow: could we use Dafny itself as the file format, just as (for example) Gradle supports Kotlin syntax via build.gradle.kts files?
  • I suspect it's not a good match since Dafny is fairly verbose and not particularly fast to "interpret", but it would be interesting to think through whether it might eventually fit this use case.

Additional features that will be nice to add AFTER the first version:

• Providing a project name of some kind would be great. If nothing else this can drive the name of the Program for the Dafny pipeline, and control the name of (for example) the DLL file dafny build produces (instead of taking the name of the first source file)
• Configuring the expected Dafny version.
• Dependency management. We could initially support the --library flag as-is, but will likely need something different in the future.

[MikaelMayer]

If we went along the route of defining a build file in Dafny, it could be great to get inspired by Mill if we went the route of having the project file defined in Dafny - which I think is an excellent idea. But Dafny lacks reflection that would be useful for a build tool.
I was using Mill even for Non-scala projects because it was so good at caching intermediate step.

However, as @robin-aws , I think it would be good to reduce the scope of the project to something manageable for now.

[keyboardDrummer]

Enable specifying options to the Dafny CLI in a Dafny project file, which can be passed as an argument when calling the Dafny CLI, also when using the dafny server command.

There's three pieces of work:

1. Introduce the dafny server command
2. Enable Dafny CLI commands that take Dafny files as input to also take a Dafny project file as input
3. Enable the dafny server command, which doesn't take input files, to locate Dafny project files for the .dfy files that it's analysing, by traversing up the file tree.

(3) depends on (1) and (2), and I scoped this issue to be (2) and (3), so it depends on (1). However, feel free to scope (3) into a separate issue and to consider this issue being just (2).

[prvshah51]

Adding list of Dafny command and arguments which I think are relevant for project file :
added value types for my understanding.

1. Resolve :

• --warn-as-errors : True/False
• --cores : string
• --show-snippets : True/False
• --prelude : string
• --unicode-char : True/False
• --function-syntax : string
• --quantifier-syntax : string
• --track-print-effects : true/false
• --warn-shadowing : true/false
• --warn-missing-constructor-parenthese : true/false

2. verify :

   • --verify-included-files : true/false
   • --relax-definite-assignment : string
   • --track-print-effects : true/false
   • --disable-nonlinear-arithmetic : true/false
   • --verification-time-limit : string
   • --solver-path : string

3. Translate :

   • --no-verify : true/false
   • --verbose : true/false
   • --output : string
   • --include-runtime : true/false
   • --optimize-erasable-datatype-wrapper : true/false
   • --enforce-determinism : true/false

4. Audit :

• --report-file: string
• --report-format: string
• --compare-report: true/false

[davidcok]

Again I would argue that we should not check options both in parsing a project file and in using it in the CLI.
To do so means that any change to options requires maintenance in two places, rather than one, and gives no particular benefit to the user.

Keep it simple. Keep it user-editable. To me a flat file with options and values would be just fine.

[keyboardDrummer]

List looks alright. I don't think it needs to be perfect in one go. You might even allow everything at first and see how that goes.

I think you're general strategy might be:

1. Parse CLI arguments once, detect that there is a project file otherwise go through the existing code path.
2. If project file, select options from the project file that are relevant for the current command, possibly discard options that were already specified on the CLI so their project file value should be ignored.
3. Build a new list of argument that includes additional options from the project file, but excludes the project file option, and parse again.

[davidcok]

Remember that a primary reason for the project file is to list the dependent files, more than the options per se. SO the UX for that use case has to be great.

[robin-aws]

Again I would argue that we should not check options both in parsing a project file and in using it in the CLI.
To do so means that any change to options requires maintenance in two places, rather than one, and gives no particular benefit to the user.

Keep it simple. Keep it user-editable. To me a flat file with options and values would be just fine.

A flat file would provide some benefit, but a project file is much more useful with some awareness of what options apply to which commands. If you want to --include-runtime when translating your project, for example, you can't just pass that flag to every command you run, because dafny verify --include-runtime ... is rejected, for example.

This is perhaps the difference between a project file and a file with a convenient batch of options to make CLI commands shorter. Personally when I feel the need for the latter, I make a shell script wrapper that prepends/appends common arguments instead, so I don't consider that a hard requirement. If the project file has a [common] section, though, you could use that for any options that are accepted by all commands (or at least all the ones you ever run :)

I do share the concern over the maintenance burden though. It would be technically possible to allow any options in a project file and just drop any that aren't supported by the current command, but then you're at risk of silently dropping a critical option. I can at least imagine an implementation strategy where we have project file sections that line up one-to-one with command and common property bags to make it easier.

[robin-aws]

Remember that a primary reason for the project file is to list the dependent files, more than the options per se. SO the UX for that use case has to be great.

Absolutely, but we should be able to provide some incremental benefit by leaning on using --library as an option instead for now. I expect when we have a clearer idea of the nature of a Dafny package/dependency, we should be able to add a dedicated dependencies section.