Add --filter option to dafny verify

[fzaiser]

Summary

There should be an easy command --filter to which I can pass which files/lemmas I want to Dafny to verify.

Background and Motivation

Before project files, people could run dafny verify onefile.dfy to only verify a subset of the project. With a project file, this is no longer possible if people have removed includes from their files. Instead they have to use --boogie-filter, which is less ergonomic and less documented. Related discussion in #4624.

Proposed Feature

Add a command line option dafny verify --filter to restrict the set of files/lemmas that Dafny verifies. It might use --boogie-filter under the hood, but provides a more ergonomic interface to the user and has good documentation.

Alternatives

One alternative for users is not to use project files. But it would be a shame if the lack of such a feature deterred people from using project files.

For restricting verification to just one function, users can use the {:only} attribute (thanks @seebees for pointing this out!). But I'm not aware of an equivalent for restricting verification to just one file.

[seebees]

I think that another alternative is {:only}

[keyboardDrummer]

I suggest not letting --filter work on files directly, so that the compiler can stay agnostic to files, but to let it work on modules as well as other simples, and to also let files implicitly declare modules, as described here: #3027

[markrtuttle]

+1

[kjx]

Would also live a command-line option equivalent to "only" (suggestion: "--only" or --verify-only")
as I'm often running both CLI and IDE in parallel, and sometimes the CLI will verify but the IDE will not...
I don't want to poke an "only' into the code, I just want the IDE equivalent of pressing the green triangle

[keyboardDrummer]

Contrary to what I said before, I'll add a filter option that allows specifying both a file and line number, so when using --isolate-assertions, you can use the CLI to verify only the assertion at a specific line:

dafny verify <project.file> --filter "fileImWorkingOn.dfy:23"

@seanmcl does that work for you as well?