[Merged by Bors] - feat: unused tactic linter #11308
Conversation
Mathlib/Data/Seq/WSeq.lean
Outdated
There was a problem hiding this comment.
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.
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.
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 ```
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
| 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.
| 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.
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: |
mathlib-bors
bot
changed the title
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
unusedTacticlinter 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.leancontains the "only"set_optionto opt out of the linter, since it defines notation that usesdecidethat the notation itself does not use;noshake.PRs removing some unused tactics:
Zulip thread