[Merged by Bors] - feat: turn on the unusedDecidableInType linter#31747
[Merged by Bors] - feat: turn on the unusedDecidableInType linter#31747thorimur wants to merge 82 commits intoleanprover-community:masterfrom
unusedDecidableInType linter#31747Conversation
unusedDecidableInType linter in MathlibunusedDecidableInType linter in Mathlib
PR summary 63af23d70cImport changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Tactic.Linter.UnusedInstancesInType | 24 | 2 | -22 (-91.67%) |
| Mathlib.Lean.Environment | 23 | 2 | -21 (-91.30%) |
| Mathlib.Lean.Expr.Basic | 26 | 4 | -22 (-84.62%) |
| Mathlib.Lean.Elab.InfoTree | 26 | 6 | -20 (-76.92%) |
| Mathlib.Init | 22 | 24 | +2 (+9.09%) |
| Mathlib.Logic.Basic | 31 | 33 | +2 (+6.45%) |
| Mathlib.Order.Heyting.Regular | 172 | 174 | +2 (+1.16%) |
| Mathlib.Logic.Encodable.Basic | 207 | 209 | +2 (+0.97%) |
| Mathlib.Data.Fintype.Quotient | 253 | 255 | +2 (+0.79%) |
| Mathlib.Computability.Halting | 430 | 432 | +2 (+0.47%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 7080 files with changed transitive imports taking up over 304814 characters: this is too many to display! | |
You can run scripts/import_trans_difference.sh all locally to see the whole output. |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
2cc8223 to
882cbb0
Compare
|
I just went ahead and made this change for you, I hope you didn't mind. Please update the PR description to match, though :-) |
|
CI errors: the first one looks related to the linter (though I wonder why it didn't show up before); the second one is probably now-missing transitive imports. |
|
Hmm, aside: I'm totally fine with this change here (and thanks @grunweg for going ahead with this—completely fine by me! :) ), but in the long run I'm not 100% sure we want to tie "functional" linters (which tell you that you might want to adjust type signatures, proof states, etc. for different functionality) to the assortment of style linters that are standard in Mathlib. They seem like they have different roles, and that downstream repos might want one but not the other. Maybe we should split off a subset? But that's not a question for this PR, just inspired by it. :) |
|
Seems like this is finally green once more! :) |
|
This pull request has conflicts, please merge |
|
24 hours passed without objections - let's get this in. A merge conflict cropped up in the meantime, though: please merge master, wait for CI to pass and then feel free to merge yourself: |
|
✌️ thorimur can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
This PR turns on the `unusedDecidableInType` syntax linter (#31142) after fixing the remaining violations in #31831, #31934, and #32153. This also imports the linter into Mathlib.Init and adds the linter to the Mathlib standard set. Given that classicality is embedded in Lean, this is probably the behavior downstream repos who use the mathlib standard set want; if they are specifically constructive repos, the linter can always be turned off in the lakefile. We exempt the entirety of [Mathlib/Data/Fintype/Quotient.lean](https://github.com/leanprover-community/mathlib4/pull/31747/files#diff-9591d2f3828bee189ea954bc33586ce451536bf00792362f7cdca4f5a8551207), [Mathlib/Order/Heyting/Regular.lean](https://github.com/leanprover-community/mathlib4/pull/31747/files#diff-af85d99e5d2f5561fe837f662f179c58f1ebe2a4ed0432a15260199883850c50), [Mathlib/Logic/Encodable/Basic.lean](https://github.com/leanprover-community/mathlib4/pull/31747/files#diff-db01c9a2d4726fe7ca0e6eb18a7cd485b5a9c6b26ba422dfbe501dcebef3cf77) and a declaration in [Mathlib/Computability/Halting.lean](https://github.com/leanprover-community/mathlib4/pull/31747/files#diff-d47323ee8b4b2321052b4be93715f8b2f3f840f76ec441d8bf75c834b8665b32) since constructivity is desired there. We also exempt `dec_em'`, which is a variant of `Decidable.em` but with the disjuncts reversed. Many prior violations have already been fixed through the use of #10235, hence the small number of violations picked up by the syntax linter. Co-authored-by: thorimur <thomasmurrills@gmail.com> Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
|
Pull request successfully merged into master. Build succeeded: |
unusedDecidableInType linterunusedDecidableInType linter
Sure, I agree that these are different things - and I wouldn't mind splitting these. Feel free to propose this on zulip. |
This PR turns on the
unusedDecidableInTypesyntax linter (#31142) after fixing the remaining violations in #31831, #31934, and #32153.This also imports the linter into Mathlib.Init and adds the linter to the Mathlib standard set. Given that classicality is embedded in Lean, this is probably the behavior downstream repos who use the mathlib standard set want; if they are specifically constructive repos, the linter can always be turned off in the lakefile.
We exempt the entirety of Mathlib/Data/Fintype/Quotient.lean, Mathlib/Order/Heyting/Regular.lean, Mathlib/Logic/Encodable/Basic.lean and a declaration in Mathlib/Computability/Halting.lean since constructivity is desired there. We also exempt
dec_em', which is a variant ofDecidable.embut with the disjuncts reversed.Many prior violations have already been fixed through the use of #10235, hence the small number of violations picked up by the syntax linter.
Decidable*instance hypothesis linter #31142Decidable*instances in theorem types #31831Decidable*instances in types #31934