Skip to content
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 --filter option to dafny verify #4816

Closed
fzaiser opened this issue Nov 22, 2023 · 5 comments · Fixed by #5008
Closed

Add --filter option to dafny verify #4816

fzaiser opened this issue Nov 22, 2023 · 5 comments · Fixed by #5008
Assignees
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Comments

@fzaiser
Copy link

fzaiser commented Nov 22, 2023

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.

@fzaiser fzaiser added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Nov 22, 2023
@seebees
Copy link

seebees commented Nov 22, 2023

I think that another alternative is {:only}

@keyboardDrummer
Copy link
Member

keyboardDrummer commented Nov 23, 2023

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
Copy link

+1

@kjx
Copy link

kjx commented Dec 30, 2023

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
Copy link
Member

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?

@keyboardDrummer keyboardDrummer changed the title Make it easier to filter what should be verified Add --filter option to dafny verify Jan 15, 2024
@keyboardDrummer keyboardDrummer self-assigned this Jan 23, 2024
keyboardDrummer added a commit that referenced this issue Jan 25, 2024
Fixes #4816 

### Description
Add an option `--filter-position` to the `dafny verify` command, that
allows verifying a single function or method, based on a file path and a
line number. For example, `dafny verify dfyconfig.toml
--filter-position=source1.dfy:5` will only verify something if it ranges
over line 5 in the file `source1.dfy`.

### How has this been tested?
Add a littish test `filter.dfy`

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Projects
None yet
Development

Successfully merging a pull request may close this issue.

5 participants