feat(Tactic/Linter): lint against exposed defs with Classical.choose (or equivalent) body - #42572
Conversation
Only preliminary: currently, the linter doesn’t handle structure constructors whose fields have a forbidden head.
…ondSet` This instance is defined from the fact that a finite product preserving functor is monoidal for cartesian monoidal category structures: it doesn’t have to be exposed.
robin-carlier
added
t-meta
✅ PR Title Formatted CorrectlyThe title of this PR has been updated to match our commit style conventions. |
PR summary 66200c9016
|
| Files | Import difference |
|---|---|
| ../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all | |
| There are 8239 files with changed transitive imports taking up over 359441 characters: this is too many to display! | |
You can run this locally from your mathlib4 directory: |
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
Declarations diff (regex)
+ aNonExposedDef
+ aPrivateNonExposedDef
+ anExposedDef
+ anotherExposedDef
+ forbiddenExposed
+ forbiddenExposed.forbiddenHeads
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
Declarations diff (Lean -- pending)
Computed after the build finishes.
No changes to strong technical debt.
No changes to weak technical debt.
Current commit 66200c9016
Reference commit 9d302fc708
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).
robin-carlier
changed the title
Classical.choose (or equivalent) body.Classical.choose (or equivalent) body
|
This pull request is now in draft mode. No active bors state needed cleanup. While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like |
| unless c.isDefinition && !(← isAutoDecl declName) && env.hasExposedBody declName do return none | ||
| let some body := c.value? | return none | ||
| let h := body.getAppFn | ||
| if forbiddenExposed.forbiddenHeads.any (· == h.constName) then |
There was a problem hiding this comment.
Rather than just the head constant, can you search through all constants? See Expr.getUsedConstants for an efficient way to get these.
The idea is that we don't want the choice functions to be exposed in any value at all.
There was a problem hiding this comment.
I’m a bit iffy on having something too strong here: there are cases I can imagine (mostly structures) where certain fields have defeqs you want to expose (e.g., the obj field of a CategoryTheory.Functor), while others would have Classical.choice-constructed values. (for instance, the CategoryTheory.Functor.map field could be some non-constructively defined morphism between the objects; that happens), then you don’t want to no_expose the entire definition to keep the defeq info on the objects.
Of course, in cases like this, you can take the choice-dependent part, abstract it as its own no-exposed definition and use that in the field, but this adding is a bit of gymnastic to get it to work.
But feel free to insist! A huge part of the library won’t pass this linter right away anyway.
There was a problem hiding this comment.
Indeed in some cases it will take a bit more effort to not expose the choice part, having to abstract it into a separate no_exposed definition, but I think that it is still beneficial to do this.
…ToLightCondSet`" This reverts commit 25b3592.
The linter could only check definitions without parameters without this.
|
It seems there is a big problem here: |
|
Ah yes I was a bit worried about this. This is something that I had asked for before, because other environment linters like For now, maybe it would be possible to use some lower level API than |
I’d be glad to have pointers on how to do this if this is possible. Maybe @thorimur also has some insights here? |
2 participants
Definitional properties of definitions made through
Classical.choice(orClassical.choose, orNonempty.some, etc.) should not matter. Hence, it makes sense to systematicallyno_exposesuch definitions. This PR adds an environment linter that checks definitions with an exposed body and tests their body against a known list of "forbidden" head constants.Currently, the linter is very simple and it does not try recursing into structures. For instance, if
Foois a one-field structure (such asInhabited), this linter will not fire on something defined asmk (Classical.choose _)while it arguably should. (Do we want this for multi-fields structures? I can see some issues if we want to keep defeqs of certain fields but not for the others, e.g. for some functors in category theory).Happy to try to implement this if asked to.
It seems the current implementation is broken.