Add project files with includes/excludes and options support #3851

keyboardDrummer · 2023-04-06T15:11:43Z

From the updated docs:

Commands on the Dafny CLI that can be passed a Dafny file, can also be passed a Dafny project file. Such a project file may define which Dafny files the project contains, and which Dafny options it uses. The project file must be a TOML file named dafny.toml. Here's an example of a Dafny project file:

includes = ["src/**/*.dfy"]
excludes = ["**/ignore.dfy"]
[options]
  enforce-determinism = true
  warn-shadowing = true

Options are applied to a command if they can be. Invalid options are ignored.

When using a Dafny IDE based on the dafny server command, the IDE will search for project files by traversing up the file tree, and options from the first found project file will override options passed to dafny server.

Caveats

The IDE will only use the saved-on-disk versions of project files, so unsaved changes are ignored.

Testing

Add CLI (through Lit) and dafny server tests (through XUnit)

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

robin-aws

Very important and long-awaited feature, and I'm happy we're starting off nice and small. Reviewed the feature design, docs and tests at a high level, but not the actual implementation just yet.

docs/DafnyRef/UserGuide.md

docs/dev/news/2907.feat

robin-aws · 2023-04-06T16:26:13Z

Test/cli/projectFile/projectFile.dfy

Make sure you have a test case or two where an option is specified on the command line and in a project file. The former should win, and I suspect your implementation favours the latter instead.

Also make sure you have at least one test with Dafny files nested more than one level deep. Very common bug to assume your glob handler treats ** as recursive descent when it doesn't (a trap I've fallen into on the command line myself several times :)

I suspect your implementation favours the latter instead.

Nope, it's already tested :D

Also make sure you have at least one test with Dafny files nested more than one level dee

Added

Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj

Source/DafnyLanguageServer/Workspace/ITextDocumentLoader.cs

docs/DafnyRef/UserGuide.md

…rojectFile

robin-aws

Replied to comments, will review the implementation shortly

docs/DafnyRef/UserGuide.md

Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj

robin-aws

Finished reviewing the rest

Source/DafnyCore/Options/ProjectFile.cs

robin-aws · 2023-04-11T16:41:55Z

Source/DafnyCore/Options/ProjectFile.cs

+ errorWriter.WriteLine($"The Dafny project file {uri.LocalPath} contains the following errors:");
+ var regex = new Regex(
+ @$"\((\d+),(\d+)\) : error : The property `(\w+)` was not found on object type {typeof(ProjectFile).FullName}");
+ var newMessage = regex.Replace(tomlException.Message,
+ match =>
+ $"({match.Groups[1].Value},{match.Groups[2].Value}): the property {match.Groups[3].Value} does not exist.");


Don't love having to do this, are going down the road of customizing all kinds of generic TOML errors in the future?

Until we update the TOML library to use customized error types, yes.

robin-aws · 2023-04-11T16:42:41Z

Source/DafnyCore/Options/ProjectFile.cs

+ }
+ }
+
+ public void ApplyToOptions(DafnyOptions options) {


Would add a comment/rename to indicate that this only adds files and not options

Source/DafnyCore/Options/ProjectFile.cs

Source/DafnyDriver/Commands/CommandRegistry.cs

docs/DafnyRef/UserGuide.md

robin-aws · 2023-04-11T17:08:29Z

docs/DafnyRef/UserGuide.md

+warn-shadowing = true
+```
+
+Under the section `[options]`, any options from the Dafny CLI can be specified using the option's name without the `--` prefix. When executing a `dafny` command using a project file, any options specified in the file that can be applied to the command, will be. Options that can't be applied or are misspelled, are ignored.


Hmm, not catching misspellings is unfortunate. Couldn't we check that all options resolve after parsing, even if they aren't used for the current command?

But you could also have options that are only valid when using a certain plugin, and then you overwrite the list of plugins on the CLI to disable one for which you have specified an option, but you don't want to be alerted about that option.

I guess it could be a warning.

robin-aws · 2023-04-11T17:09:39Z

Source/DafnyLanguageServer.Test/DafnyLanguageServerTestBase.cs

@@ -84,12 +84,12 @@ ensures true

 private static void ApplyDefaultOptionValues(DafnyOptions dafnyOptions) {
 var testCommand = new System.CommandLine.Command("test");
- foreach (var serverOption in new ServerCommand().Options) {
+ foreach (var serverOption in ServerCommand.Instance.Options) {


Why was this necessary?

robin-aws · 2023-04-11T17:10:29Z

Source/DafnyLanguageServer.Test/ProjectFiles/TestFiles/Nesting/dafny.toml

I'd rename at least one project file to have a base name other than dafny, just to ensure we're not assuming that anywhere

Source/DafnyLanguageServer/Workspace/DocumentManager.cs

robin-aws · 2023-04-12T23:41:58Z

I wasn't sure from previous versions whether we were going to require project files to be named dafny.toml, or if we'd support any *.toml file. It sounds like you want the former, which I'm fine with and less of a one-way door, so let's go with that, but just make sure the documentation and tests are all consistent. :)

keyboardDrummer · 2023-04-13T09:53:17Z

I wasn't sure from previous versions whether we were going to require project files to be named dafny.toml, or if we'd support any *.toml file. It sounds like you want the former, which I'm fine with and less of a one-way door, so let's go with that, but just make sure the documentation and tests are all consistent. :)

I think it's all consistent. A *.toml file is allowed on the CLI, but gives a warning that the IDE will only use dafny.toml files. The documentation says to use a dafny.toml file.

robin-aws

Looks great aside from a couple last documentation corrections!

And one more quick thing before walking through the one-way door, hopefully just a quick find-and-replace: in the style of tsconfig.json, I feel like dafnyconfig.toml would be slightly more helpful. WDYT?

robin-aws · 2023-04-13T22:13:58Z

docs/dev/news/2907.feat

@@ -0,0 +1,3 @@
+Added support for Dafny project files. For now the project file only allows specifying which Dafny files to include and exclude, and what options to use.
+The CLI commands that take Dafny files as input, such as build, run, translate, will also accept Dafny project files.
+When using an IDE based on `dafny server`, such as the Dafny VSCode extension, the IDE will look for Dafny project files by traversing up the file tree from the currently opened file. The first found project file will override options specified in the IDE. 


Should mention the file has to be called dafny.toml here.

robin-aws · 2023-04-13T22:14:23Z

docs/dev/news/2907.feat

@@ -0,0 +1,3 @@
+Added support for Dafny project files. For now the project file only allows specifying which Dafny files to include and exclude, and what options to use.


Should probably mention the supported format is *.toml here, or perhaps link to the refman section.

robin-aws · 2023-04-13T22:20:11Z

docs/DafnyRef/UserGuide.md

@@ -571,6 +571,25 @@ Most output from `dafny` is directed to the standard output of the shell invokin
 - Dafny `expect` statements (when they fail) send a message to **standard-out**.
 - Dafny I/O libraries send output explicitly to either **standard-out or standard-error**

+### 13.5.5. Project files
+
+Commands on the Dafny CLI that can be passed a Dafny file, can also be passed a Dafny project file. Such a project file may define which Dafny files the project contains, and which Dafny options it uses. The project file must be a [TOML](https://toml.io/en/) file named `dafny.toml`. Here's an example of a Dafny project file:


I think we're clear on the behaviour now, which means this should say that any *.toml file is accepted...

robin-aws · 2023-04-13T22:20:29Z

docs/DafnyRef/UserGuide.md

+
+Under the section `[options]`, any options from the Dafny CLI can be specified using the option's name without the `--` prefix. When executing a `dafny` command using a project file, any options specified in the file that can be applied to the command, will be. Options that can't be applied or are misspelled, are ignored.
+
+When using a Dafny IDE based on the `dafny server` command, the IDE will search for project files by traversing up the file tree, and options from the first found project file will override options passed to `dafny server`.


...but this should say only dafny.toml files will be found.

robin-aws

🎉

keyboardDrummer added 12 commits April 6, 2023 13:19

Draft of project file support for CLI commands

2d0a360

Add error handling and support for excludes

e84f9a4

Improvements

93a4dfb

Update documentation

fbbdd16

Add language server test for project files

c0c0705

Server project file test passes

2ddb0d4

Fix test

71acc75

Run formatter

5e4b694

Update documentation

d89e4c2

Add multiple project files check

642849a

Test for option override behavior

38a0ad3

Add test documentation

ad354ef

keyboardDrummer requested a review from robin-aws April 6, 2023 15:14

keyboardDrummer added 5 commits April 6, 2023 17:41

Added dafny server test, release notes, and removed TODO

cdf0369

Fix tests

ad7b23f

Fix crash

260fbbf

Run formatter

eb52f49

Add check against bad types

d8a96dd

robin-aws requested changes Apr 6, 2023

View reviewed changes

keyboardDrummer added 3 commits April 7, 2023 10:46

Code review

71a72b9

Add a default includes pattern

b06d4b5

Merge branch 'master' into projectFile

275b73e

keyboardDrummer enabled auto-merge (squash) April 7, 2023 08:56

keyboardDrummer requested a review from robin-aws April 7, 2023 08:57

keyboardDrummer added 6 commits April 7, 2023 17:57

Fix tests

cbbe7e6

Update customBoogie.patch

3d759e3

Merge branch 'projectFile' of github.com:keyboardDrummer/dafny into p…

29d4197

…rojectFile

Merge branch 'master' into projectFile

6804d5a

Fix test exception and remove some annoying debug log lines

bbfb98f

Turn off some logging and hopefulyl fix a Windows bug

f0bf212

robin-aws mentioned this pull request Apr 10, 2023

Support per-assertion batch maximum bounds dafny-lang/dafny-reportgenerator#18

Open

robin-aws reviewed Apr 10, 2023

View reviewed changes

docs/DafnyRef/UserGuide.md Outdated Show resolved Hide resolved

docs/DafnyRef/UserGuide.md Show resolved Hide resolved

Source/DafnyLanguageServer.Test/DafnyLanguageServer.Test.csproj Show resolved Hide resolved

keyboardDrummer added 2 commits April 11, 2023 12:16

Improve documentation

a783681

Merge branch 'master' into projectFile

eb8e799

keyboardDrummer requested a review from robin-aws April 11, 2023 10:18

robin-aws requested changes Apr 11, 2023

View reviewed changes

keyboardDrummer added 6 commits April 12, 2023 10:43

Refactoring

8fbff18

Fix and test extensions

e5acbfc

Add validation to check for options in a project file that don't exist

5f588ab

Run formatter

b30332b

Add warning about non dafny.toml project files

ae3d58e

Ran formatter

6f280c1

Undo lit tests change

f6d3b92

keyboardDrummer requested review from robin-aws April 13, 2023 09:52

Prevent crash when project files aren't file paths

7bb1ba1

robin-aws reviewed Apr 13, 2023

View reviewed changes

keyboardDrummer added 2 commits April 14, 2023 11:44

Update documentation and use dfyconfig.toml

1330d0d

Fix test

8f6da0f

robin-aws approved these changes Apr 14, 2023

View reviewed changes

Merge branch 'master' into projectFile

6cb8001

keyboardDrummer merged commit b956d23 into dafny-lang:master Apr 14, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add project files with includes/excludes and options support #3851

Add project files with includes/excludes and options support #3851

keyboardDrummer commented Apr 6, 2023 •

edited

Loading

robin-aws left a comment

robin-aws Apr 6, 2023

keyboardDrummer Apr 7, 2023 •

edited

Loading

robin-aws left a comment

robin-aws left a comment

robin-aws Apr 11, 2023

keyboardDrummer Apr 12, 2023

robin-aws Apr 11, 2023

robin-aws Apr 11, 2023

keyboardDrummer Apr 12, 2023

robin-aws Apr 11, 2023

robin-aws Apr 11, 2023

robin-aws commented Apr 12, 2023

keyboardDrummer commented Apr 13, 2023 •

edited

Loading

robin-aws left a comment

robin-aws Apr 13, 2023

robin-aws Apr 13, 2023

robin-aws Apr 13, 2023

keyboardDrummer Apr 14, 2023

robin-aws Apr 13, 2023

keyboardDrummer Apr 14, 2023

robin-aws left a comment

		@@ -0,0 +1,3 @@
		Added support for Dafny project files. For now the project file only allows specifying which Dafny files to include and exclude, and what options to use.


		Under the section `[options]`, any options from the Dafny CLI can be specified using the option's name without the `--` prefix. When executing a `dafny` command using a project file, any options specified in the file that can be applied to the command, will be. Options that can't be applied or are misspelled, are ignored.

		When using a Dafny IDE based on the `dafny server` command, the IDE will search for project files by traversing up the file tree, and options from the first found project file will override options passed to `dafny server`.

Add project files with includes/excludes and options support #3851

Add project files with includes/excludes and options support #3851

Conversation

keyboardDrummer commented Apr 6, 2023 • edited Loading

From the updated docs:

Caveats

Testing

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Apr 7, 2023 • edited Loading

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws commented Apr 12, 2023

keyboardDrummer commented Apr 13, 2023 • edited Loading

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

keyboardDrummer commented Apr 6, 2023 •

edited

Loading

keyboardDrummer Apr 7, 2023 •

edited

Loading

keyboardDrummer commented Apr 13, 2023 •

edited

Loading