feat: add `Decidable` linter

[urkud]

---

• [x] depends on: #10237
• [x] depends on: #10249
• [x] depends on: #10250
• [x] depends on: #10251
• [x] depends on: #10253
• [x] depends on: #10254
• [x] depends on: #10255
• [x] depends on: #10257
• [x] depends on: #10261
• [x] depends on: #10262

[github-actions[bot]]

PR summary bf35bd39a0

Import changes exceeding 2%

%	File
+7.69%	Mathlib.Logic.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Logic.Basic	65	70	+5 (+7.69%)

Import changes for all files

Files	Import difference
There are 6581 files with changed transitive imports taking up over 282677 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ checkUnusedAssumptionInType + decidableClassical + encodableCountable + finiteFintype + inhabitedNonempty

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 relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

FYI: #15278, #15279, #15280 (edit: and #15283) fix some easy linter errors; I don't have further fixes in the pipeline

[urkud]

We should skip constructors of inductive types as well (at least, for now).

[grunweg]

Do you know how to do this? (You can also leave a pointer here and I'll try to add this to the linter, when I find time. This week, and probably the next, I'm also rather busy with moving places, so cannot make promises about my available Lean time.)

[grunweg]

!bench

[grunweg]

(I worry if the linter implementation is too slow right now, and the linters should rather be merged... let's benchmark to find out!)

[leanprover-bot]

Here are the benchmark results for commit fea856fdba2eaa624916afa8611ee0493e694001. The entire run failed. Found no significant differences.

[grunweg]

!bench

[leanprover-bot]

Here are the benchmark results for commit 83c41915e1d0bd5603f23bdd11c268338e2b7a22. The entire run failed. Found no significant differences.

[grunweg]

!bench

[grunweg]

@kmill Thanks for commenting about the GeneralizeProofs change; I'm learning something new every day! The linter ignores partial declarations now; I just verified that the change could be reverted. Would you prefer that change?

[leanprover-bot]

Here are the benchmark results for commit 678b68b12f96cc94afb870c499f26e99ec2e091f. The entire run failed. Found no significant differences.

[urkud]

@grunweg Linter flags GeneralizeProofs now. I can't find the relevant @kmill's comment. Was it here or on Zulip?

[grunweg]

It was on a dependent PR.

[grunweg]

I'm also open to reverting this commit, or rather, just the second half. (The first half is fine now.)

[urkud]

Is there a way to test for a function being partial? If yes, then we should do it.

[kmill]

partial definitions create opaque definitions, so it could check for that (though theoretically there could be intentional opaque definitions in the library, but this has not been observed yet).

Here are some checks I found:

partial def foo (n : Nat) : Nat := foo n

open Lean

def isOpaque (n : Name) : MetaM Bool := do
  let ci ← getConstInfo n
  return ci matches .opaqueInfo ..

def isUnsafe (n : Name) : MetaM Bool := do
  let ci ← getConstInfo n
  return ci.isUnsafe

def isPartial (n : Name) : MetaM Bool := do
  let ci ← getConstInfo n
  return ci.isPartial

With these:

• isOpaque `foo is true
• isUnsafe `foo is false (though this becomes true with the unsafe modifier, which also makes isOpaque become false)
• isPartial `foo is false (I think these are only used internally and no user definitions are this kind of partial)

[grunweg]

@kmill Thanks for the explanations. I had tried isPartial, but that did not do what I wanted (or did not go far enough?). I've tried to check for opaqueInfo now; let's see if that works.

[kmill]

(My cursory understanding of isPartial is that it's for "pre definitions" for (mutually) recursive functions, letting them be added to the environment for future processing. As far as I know, this option is irrelevant to us — it has no relation to partial — and we'd never see it unless we're really digging around into internal details.)

[grunweg]

:bulb: That is helpful. Would you like to file PR adding this docstring? Or should I create one, so you can get help fixing it more easily :-)?

[kmill]

Feel free to create a pr and ping me and/or Joachim. He's more familiar with this part of Lean.

[grunweg]

!bench

[leanprover-bot]

Here are the benchmark results for commit 5e620ae419bc239d2bb10b17f87fe918c918487e.Found no runs to compare against.

[urkud]

!bench

[urkud]

Should we merge it now?

[leanprover-bot]

Here are the benchmark results for commit 8b01daa371e7baa30a69c3cfeae0d1fa619bfffb. The entire run failed. Found no runs to compare against.

[grunweg]

I'm happy with merging it, and looking at post-merge benchmarking output.

[grunweg]

I am not confident there will be no regression in linting times - but as there are further such linters in the pipeline, I am not worried about that item dropping of everybody's radar.

[grunweg]

Thanks for the fixes; they look good to me.

[urkud]

!bench