Do not allow building libraries while silently not verifing included files

[keyboardDrummer]

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 a dafny migrate that automatically updates a Dafny codebase to work with an upcoming version. Creates this ticket for that: #5407)

Description

• By default, all included files are now verified as well
• The option --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?

• Updated the test Include.dfy

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

[robin-aws]

Heavily in favour of making this change in general, but I think just switching the default, although safe (since it's just verifying more code than before) could make the ad-hoc build systems for existing Dafny projects grind to a crawl, if they are relying on the fact that includes aren't verified and forking many processes to verify files in parallel.

I think the dafny migrate command idea is an excellent solution and we should build that before making this change. Will add more ideas to that issue.

[keyboardDrummer]

Heavily in favour of making this change in general, but I think just switching the default, although safe (since it's just verifying more code than before) could make the ad-hoc build systems for existing Dafny projects grind to a crawl, if they are relying on the fact that includes aren't verified and forking many processes to verify files in parallel.

I think the dafny migrate command idea is an excellent solution and we should build that before making this change. Will add more ideas to that issue.

Good callout

[robin-aws]

One other thought for when we come back to this: the option name should be more explicit that it's only skipping verification somehow - dafny test --skip-included-files ... sounds too much like it's skipping tests instead for e.g. Perhaps --dont-verify-included-files? I'm fine with it being wordy and awkward given we want to discourage it in the long term anyway. :)

[keyboardDrummer]

One other thought for when we come back to this: the option name should be more explicit that it's only skipping verification somehow - dafny test --skip-included-files ... sounds too much like it's skipping tests instead for e.g. Perhaps --dont-verify-included-files? I'm fine with it being wordy and awkward given we want to discourage it in the long term anyway. :)

I like it. I thought of --no-verify-included-files to match with --no-verify, but TBH I would prefer dont for both.