Boundary for instances searching

Stream: mathlib4

[Jiang Jiedong]

Hi everyone,

While working on #6045, I encountered an interesting phenomenon. I was modifying the definition of IsLocalRingHom, which led to many instances in the algebraic geometry files breaking. I found that there is a file named Mathlib.Algebra.Category.Ring.Instances that contains all the IsLocalRingHom instances required by the algebraic geometry files. Despite the changes to the IsLocalRingHom definition, this file compiled perfectly. However, subsequent files that were supposed to depend solely on instances in this file failed to compile.

I'm curious if it would be beneficial to implement a mechanism (perhaps involving transparency or priority) that requires all instance searches within a file to first/only rely on certain predefined instances. This could potentially significantly reduce the instance search time for very late files.

[Andrew Yang]

Have you looked into why the instances are breaking? If it is not a timeout issue but that Lean cannot find them completely, I don't think the solution proposed will help here.

[Jiang Jiedong]

I agree with you, @Andrew Yang, that this approach will not solve issues beyond the timeout problem. However, I believe it could assist in more quickly identifying the real cause of the issue. If there are found instances where the search does not pass through the file Mathlib.Algebra.Category.Ring.Instances as designed, we could detect it early, potentially reducing future maintenance work.

[Matthew Ballard]

Without looking, things are probably getting filtered out by the discrimination tree here.

[Jiang Jiedong]

The current instance problem after #6045 is indeed not a timeout problem. I suspect something undesired is happening in the coercion process when one writes LocalRing.ResidueField.map (f.stalkMap x).