-
Notifications
You must be signed in to change notification settings - Fork 331
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
[Merged by Bors] - feat: unused tactic linter #11308
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Wow super cool!
Mathlib/Data/Seq/WSeq.lean
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The error message looks quite suboptimal. Could the tactic offer a Try this: <tactic call without the useless tactic
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, It probably could, although the cure is typically to simply remove the underlined code.
I'll try it, though and see how the formatting goes.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I tried a bit and I find it tricky: I do not know how to consistently remove the "unused" syntax. I could make it work when you have a very basic sequence of tactics, but as soon as there are combinators or any non-trivial nesting, I fail to produce well-formed syntax robustly.
Just FWIW, when I read the PR title "pointless linter", at first I thought (apart from the pun, which I like!) it was about missing focusing dots... If/when this is running in CI, being clearly about pointless tactics will really help. (You mostly already do this.) |
You are right: maybe calling it a more sober "unused tactic linter" might be better. I'll leave it as is while I clean up the "useless" tactics and will maybe have a poll later on. EDIT: I've done just that now. The linter is now called the "unused tactic linter". |
As said on the other PR, I'm not sure what the point of eradicating "purposely pointless" tactics like |
I have not yet found a way to nolint With respect to |
The removal of some pointless tactics flagged by #11308.
I removed some of the tactics that were not used and are hopefully uncontroversial arising from the linter at #11308. As the commit messages should convey, the removed tactics are, essentially, ``` push_cast norm_cast congr norm_num dsimp funext intro infer_instance ```
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks pretty straighforward now.
maintainer merge
end | ||
|
||
/-- Gets the value of the `linter.unusedTactic` option. -/ | ||
def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.unusedTactic o |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
def getLinterHash (o : Options) : Bool := Linter.getLinterValue linter.unusedTactic o | |
def getLinterHash (o : Options) : Bool := linter.unusedTactic.getLinterValue o |
no?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you very much for the reviews, Yaël!
I tried this suggestion, but it does not work: the type of linter.unusedTactic
is Lean.Option Bool
. The Linter
itself is the following declaration, unusedTacticLinter
.
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
1 similar comment
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
bors d+ |
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
…ity/mathlib4 into adomani/useless_tactic
Two more unused tactics had snuck in since the last time I merged master! Thanks for the reviews! bors r+ |
The `unusedTactic` linter emits a warning if a tactic does nothing. Previous PRs (see below) removed all the "unused tactics" that the linter flagged. Here is an overview of this PR: * the linter is defined in `Mathlib/Tactic/Linter/UnusedTactic.lean`; * the file `Mathlib/GroupTheory/Perm/Cycle/Concrete.lean` contains the "only" `set_option` to opt out of the linter, since it defines notation that uses `decide` that the notation itself does not use; * 17 test files that have surgically opted out of the linter; * noise to import the new file, place it low in the import hierarchy and update `noshake`. PRs removing some unused tactics: * #11333 * #11351 * #11365 * #11379 [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/pointless.20tactic.20linter)
Pull request successfully merged into master. Build succeeded: |
The `unusedTactic` linter emits a warning if a tactic does nothing. Previous PRs (see below) removed all the "unused tactics" that the linter flagged. Here is an overview of this PR: * the linter is defined in `Mathlib/Tactic/Linter/UnusedTactic.lean`; * the file `Mathlib/GroupTheory/Perm/Cycle/Concrete.lean` contains the "only" `set_option` to opt out of the linter, since it defines notation that uses `decide` that the notation itself does not use; * 17 test files that have surgically opted out of the linter; * noise to import the new file, place it low in the import hierarchy and update `noshake`. PRs removing some unused tactics: * #11333 * #11351 * #11365 * #11379 [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/pointless.20tactic.20linter)
The
unusedTactic
linter emits a warning if a tactic does nothing.Previous PRs (see below) removed all the "unused tactics" that the linter flagged.
Here is an overview of this PR:
Mathlib/Tactic/Linter/UnusedTactic.lean
;Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
contains the "only"set_option
to opt out of the linter, since it defines notation that usesdecide
that the notation itself does not use;noshake
.PRs removing some unused tactics:
Zulip thread