Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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
Changes from 36 commits
2d0a360
e84f9a4
93a4dfb
fbbdd16
c0c0705
2ddb0d4
71acc75
5e4b694
d89e4c2
642849a
38a0ad3
ad354ef
cdf0369
ad7b23f
260fbbf
eb52f49
d8a96dd
71a72b9
b06d4b5
275b73e
cbbe7e6
3d759e3
29d4197
6804d5a
bbfb98f
f0bf212
a783681
eb8e799
8fbff18
e5acbfc
5f588ab
b30332b
ae3d58e
6f280c1
f6d3b92
7bb1ba1
1330d0d
8f6da0f
6cb8001
File filter
Filter by extension
Conversations
Jump to
There are no files selected for viewing
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.
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.
Was this always wrong before?
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 guess so. It produced an exception in the CI log that's how I found it. Guess it didn't break the tests.
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.
Do you have a test case with a project file and explicit files passed on the CLI, especially with duplicates? Especially including a file on the CLI that the project file
excludes
?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.
Added those two tests
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