Warn when using non doo file as a library #5313
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
robin-aws
requested changes
Apr 10, 2024
docs/dev/news/5297.feat
Outdated
| @@ -0,0 +1,2 @@ | |||
| - Warn when passing something other than a doo file to `--library` | |||
| - Allow using project files in the same places as `.dfy` files. They behave as if they are a Dafny source file that includes all the sources and library files defined in the project file | |||
There was a problem hiding this comment.
Suggested change
| - Allow using project files in the same places as `.dfy` files. They behave as if they are a Dafny source file that includes all the sources and library files defined in the project file |
(or rather move to #5297 :)
| } | ||
|
|
||
| result.Add(DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, DafnyMain.StandardLibrariesDooUri, Project.StartingToken)); | ||
| var file = await DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, DafnyMain.StandardLibrariesDooUri, Project.StartingToken); | ||
| if (file != null) { |
There was a problem hiding this comment.
This is a bit dangerous though, isn't it? If there's some packaging error and the main stdlib doo file is missing, we'll silently ignore it. Better to throw a description internal exception I think.
There was a problem hiding this comment.
Oof, I don't recall why this was needed. Well, fastest way to remember is to remove it again ^,^
There was a problem hiding this comment.
Without it, the tests fail:
Failed stdlibs/StandardLibraries_Errors.dfy [52 s]
Error Message:
System.AggregateException : One or more errors occurred. (Command returned non-zero exit code (1): DiffCommand TestFiles/LitTests/LitTest/stdlibs/StandardLibraries_Errors.dfy.expect /home/runner/work/dafny/dafny/dafny/Source/IntegrationTests/bin/Debug/net6.0/TestFiles/LitTests/LitTest/stdlibs/Output/StandardLibraries_Errors.dfy.tmp
Output:
AssertEqualWithDiff() Failure
Diff (changing expected into actual):
Dafny program verifier finished with 1 verified, 0 errors
Dafny program verifier finished with 1 verified, 0 errors
StandardLibraries_Errors.dfy(20,20): Error: module Std does not exist (position 0 in path Std.Wrappers)
1 resolution/type errors detected in StandardLibraries_Errors.dfy
CLI: Error: cannot load DafnyStandardLibraries-notarget.doo: --unicode-char is set locally to False, but the library was built with True
CLI: Error: cannot load DafnyStandardLibraries.doo: --unicode-char is set locally to False, but the library was built with True
+Encountered internal compilation exception: Object reference not set to an instance of an object.
Please use the '--check' and/or '--print' option as doo files cannot be formatted in place.
Please use the '--check' and/or '--print' option as doo files cannot be formatted in place.
Seems there is no custom check to prevent --unicode-char false and --standard-libraries from being used together. This is discovered and reported in the call to DafnyFile.CreateAndValidate, after which it still returns null and should not crash because of that.
There was a problem hiding this comment.
Ah that's fair, if the file is missing it should fail more loudly. I forgot that CreateAndValidate only returns null if the file wasn't valid.
Comment on lines
191
to
194
| $"The file '{Options.GetPrintPath(unverifiedLibrary)}' was passed to --library. " + | ||
| $"Verification previously done for that file might not be sufficient, " + | ||
| $"because it might have used options incompatible with the current ones. " + | ||
| $"Use a .doo file to enable Dafny to check that compatible options were used"); |
There was a problem hiding this comment.
Suggested change
| $"The file '{Options.GetPrintPath(unverifiedLibrary)}' was passed to --library. " + | |
| $"Verification previously done for that file might not be sufficient, " + | |
| $"because it might have used options incompatible with the current ones. " + | |
| $"Use a .doo file to enable Dafny to check that compatible options were used"); | |
| ```suggestion | |
| $"The file '{Options.GetPrintPath(unverifiedLibrary)}' was passed to --library. " + | |
| $"Verification for that file might have used options incompatible with the current ones, or might have been skipped entirely. " + | |
| $"Use a .doo file to enable Dafny to check that compatible options were used."); |
robin-aws
previously approved these changes
Apr 10, 2024
MikaelMayer
approved these changes
Apr 11, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Changes
How has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.