mathlib-minimizer

Stream: mathlib4

[Kevin Buzzard]

I've been using mathlib-minimizer for the last few days in an attempt to minimize the universe issue which has been bugging me recently (my"weekend project"). It's bombed out on me twice so far. Once because it turned out that my failing test was too brittle (the error would sometimes be timed out doing IsDefEq and sometimes timed out doing whnf or whatever), which I fixed by making a better test. But the second time was this morning, for a more interesting reason: at some point in mathlib we're apparently explicitly using the name of an auto-generated instance. In Mathlib/Algebra/Algebra/Operations.lean we have

instance : NonUnitalSemiring (Submodule R A) where
  __ := toAddSubmonoid_injective.semigroup _ mul_toAddSubmonoid
...

and later on in that file (in the Submodule namespace) we have

/-- Sub-R-modules of an R-algebra form an idempotent semiring. -/
instance idemSemiring : IdemSemiring (Submodule R A) where
  __ := instNonUnitalSemiring
...

with Submodule.instNonUnitalSemiring being the name given to the instance by mathlib. Aah! But in the minimiser this instance was given the name Submodule.instNonUnitalSemiring_mathlibMinimizer! (the instance naming algorithm puts the name of the project at the end; I have a bunch of ..._fLT instances in FLT, for example). This leads to the error

FATAL: All 1 import inlining attempts failed.
Failed imports: #[Mathlib.Algebra.Algebra.Operations]
This should never happen - import inlining should always succeed.
The last failed source has been written to the output file for debugging.

in the minimiser. What should be done here?

[Jovan Gerbscheid]

I believe we can simply get rid of the line __ := Submodule.instNonUnitalSemiring, because nowadays, the instance can be inferred automatically.

[Kevin Buzzard]

But longer-term there are the questions of (a) is it OK to use automatically-generated instance names in mathlib and (b) if it is then this will break the minimiser -- will it be easy to fix?

[Michael Rothgang]

Using automatically generated instance names explicitly in the source feels bad to me. Either, we should not reference them, or we should name them by hand.

[Michael Rothgang]

Imho, we should have a linter for this and track any existing violations as technical debt (unless there are so few that we can remove them all in one go).

[Kevin Buzzard]

Proposal for finding them: change the instance-naming algorithm in core and see what breaks.

How would one lint against this though?

[Edward van de Meent]

one could try to keep track of which names are automatically generated somehow, for example by enforcing some kind of naming scheme or by keeping track in an environment extension, and then at elaboration time insert a check which raises a warning?

[Damiano Testa]

You could also write a linter that chirps out the automatically generated instance names: these are the ones that syntactically do not have a declId node. Once you have that list, you check if any of these names is referenced in the syntax of another command.