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.

Sign up for GitHub

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

Jump to bottom

--tests option for dafny test #3221

Closed
davidcok opened this issue Dec 19, 2022 · 1 comment
Closed

--tests option for dafny test #3221

davidcok opened this issue Dec 19, 2022 · 1 comment
Assignees
@davidcok
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Comments

@davidcok
Copy link
Collaborator

Summary

dafny test executes all methods annotated with {:test}. There is no way to be selective.
Add an option --tests that takes a regex pattern as its value. Then have dafny test just run the methods whose fully-qualified name (by the containing module names) matches that pattern.

Background and Motivation

Can't be selective about which tests are run.

Proposed Feature

As described in the summary

Alternatives

No response
@davidcok davidcok added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Dec 19, 2022
@keyboardDrummer keyboardDrummer removed their assignment Dec 20, 2022
@davidcok davidcok mentioned this issue Dec 21, 2022
Closed
@davidcok davidcok self-assigned this Mar 7, 2023
@davidcok
Copy link
Collaborator Author

davidcok commented Apr 4, 2023

Implemented in PR #3769

@davidcok davidcok closed this as completed Apr 4, 2023
@tchajed tchajed mentioned this issue May 10, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@davidcok davidcok

Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@keyboardDrummer @davidcok