Do not allow building libraries while silently not verifing included files #5406
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.
Fixes #4762 (actually, it's only truly fixed until we remove
--verify-included files
, but our migration policy prevents doing this until we do another release. IMO the migration policy of always requiring a Dafny codebase to be forward compatible with an upcoming release is quite harmful to effective development of Dafny. We should drive towards being able to drop that. I'm guessing we can do that once we add adafny migrate
that automatically updates a Dafny codebase to work with an upcoming version. Creates this ticket for that: #5407)Description
--verify-included-files
is replaced by--skip-included-files
. For backwards compatibility purposes,--verify-included-files
is still kept, although hidden and marked as deprecated.How has this been tested?
Include.dfy
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.