-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add project files with includes/excludes and options support #3851
Add project files with includes/excludes and options support #3851
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 :)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Replied to comments, will review the implementation shortly
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Finished reviewing the rest
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."); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Don't love having to do this, are going down the road of customizing all kinds of generic TOML errors in the future?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Until we update the TOML library to use customized error types, yes.
} | ||
} | ||
|
||
public void ApplyToOptions(DafnyOptions options) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Would add a comment/rename to indicate that this only adds files and not options
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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
@@ -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) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why was this necessary?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
I wasn't sure from previous versions whether we were going to require project files to be named |
I think it's all consistent. A |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
docs/dev/news/2907.feat
Outdated
@@ -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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should mention the file has to be called dafny.toml
here.
docs/dev/news/2907.feat
Outdated
@@ -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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Should probably mention the supported format is *.toml
here, or perhaps link to the refman section.
docs/DafnyRef/UserGuide.md
Outdated
@@ -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: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we're clear on the behaviour now, which means this should say that any *.toml
file is accepted...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Updated
docs/DafnyRef/UserGuide.md
Outdated
|
||
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`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
...but this should say only dafny.toml
files will be found.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Updated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
🎉
Fixes #2907
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: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 todafny server
.Caveats
Testing
dafny server
tests (through XUnit)By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.