CI failing in untouched file

Stream: mathlib4

[Artie Khovanov]

https://github.com/leanprover-community/mathlib4/actions/runs/21259376489/job/61182695264?pr=33697
My PR adds a new leaf file. However it fails CI with a linter error about lemmas not being in simp normal form. These lemmas are in a random file I haven't touched. Does anyone understand what is going on?

[Junyan Xu]

simpNF imports the whole mathlib, then tries to simplify each side of every simp lemma. These simp calls may not time out in the original file the simp lemma is in, but may time out when the whole library is imported, especially if new simp lemmas are introduced or in this case, new instance (from IsRealClosed to IsSemireal). I guess trying to synthesize Field is what makes it time out.

[Artie Khovanov]

Hm OK, thanks

[Artie Khovanov]

I still don't understand what is going on here. The instance that fails times out in the original file as well. simp only works fine. It looks like some other simp lemma which doesn't end up firing has a typeclass synthesis which times out on this branch but not on master.

[Artie Khovanov]

The offending lemma is docs#FaithfulSMul.ker_algebraMap_eq_bot
The FaithfulSMul instance it's looking for doesn't exist! I don't understand what's going on.
Presumably there's a IsRealClosed -> IsSemireal -> CharZero -> ... -> FaithfulSMul chain that tips typeclass inference over the edge.

[Artie Khovanov]

But why does simp crash if typeclass inference times out, rather than simply moving on, as normal? Surely not every typeclass problem simp meets is resolved within 20k hbs?

[Kevin Buzzard]

Have you compared profiling simp traces before and after the PR? What was the timing before? Is it one of those unlucky "this took 19.9k before and 20.1k after" issues or is this a perfectly reasonable proof which now goes haywire after your PR?

[Artie Khovanov]

Not sure how to profile given that the synthesis fails

[Aaron Liu]

you set up a file with the failing synthesis and you turn on the profiler?

[Artie Khovanov]

I will try it
Maybe I misunderstood something

[Artie Khovanov]

Sure enough

import Mathlib

set_option diagnostics true
set_option diagnostics.threshold 0

set_option trace.Debug.Meta.Tactic.simp true in
example {R S T ι : Type*}
    [CommRing R] [CommRing S]
    [Algebra R S] (P : Algebra.Generators R S ι) [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) :
    RingHom.ker (algebraMap (P.ofAlgEquiv e).Ring T) = sorry := by
  simp
-- master: simp made no progress
-- #33697: failed to synthesize FaithfulSMul (P.ofAlgEquiv e).Ring T (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

variable {R S T ι : Type*}
    [CommRing R] [CommRing S]
    [Algebra R S] (P : Algebra.Generators R S ι) [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T)

#count_heartbeats in
#synth FaithfulSMul (P.ofAlgEquiv e).Ring T
-- master: Used 19452 heartbeats
-- #33697: Used 22693 heartbeats

[Artie Khovanov]

the synthesis goes on a magical mystery tour of what seems like the entirety of Mathlib
and indeed what pushes it over the edge of 20k hb is [] IsRealClosed.toIsSemireal ↦ 3, along the chain I described above

[Artie Khovanov]

so I suppose it's unlucky the way Kevin described

[Artie Khovanov]

not really sure what to do - surely I can't go on making all my new - perfectly reasonable - instances super low priority - and that won't even help here because we need the TC search to completely fail
surely something can be done about the magical mystery tour?

[Kevin Buzzard]

Yes, ideally the fix for this is to stop the tour from happening. If you switch off simp tracing and switch on trace.Meta.synthInstance or whatever it's called, can you see where things begin to go pear-shaped?

[Kim Morrison]

We're actively thinking about how to help here. But we really need standalone examples of these mystery tours, ideally still reflecting well the actual structure of the search and the current Mathlib design.

If you have time to investigate making minimizations of examples like this (either manually, or using https://github.com/kim-em/mathlib-minimizer), that would be really helpful!

[Junyan Xu]

Does changing Field R to CommRing R in IsRealClosed help a little?

[Artie Khovanov]

I mean, even if it did, it wouldn't be an acceptable fix, right?

[Artie Khovanov]

But I'll try all these things next time I get a chance, thanks all!

[Junyan Xu]

I don't think it's unacceptable? Many mathlib definitions allow more generality than intended (e.g. docs#MonoidHom only requires MulOne, and you don't even have Field in the decl name), and if you're not interested in generalizing the lemmas, just switch back to the Field assumption when stating them.

You might also consider adding docs#IsField as a field of IsRealClosed.

[Artie Khovanov]

Because it might lead to a mathematically incorrect definition! I have no idea about the analogous theory over rings. Indeed, we have frequently had to make refactors as a result of this sort of misformalised definition.

[Aaron Liu]

but surely if every odd degree polynomial has a root then every polynomial of the form a * X - 1 has a root so it's a field after all

[Artie Khovanov]

that's a good point
it would still be a bad formalisation of the definition; it should be a constructor
I think it's a bad idea to formalise according to essentially arbitrary typeclass inference constraints!
I will focus on fixing the underlying problem

[Junyan Xu]

I don't know what's the tour happening in your case, but notice even synthesizing something as simple as Nonempty can be heavy (goes up to NormedField etc.). The following trace was what prompted me to introduce a dedicated class IsGCDMonoid in #34179 rather than reusing Nonempty:
image.png

[Yaël Dillies]

Aaron Liu said:

but surely if every odd degree polynomial has a root then every polynomial of the form a * X - 1 has a root so it's a field after all

Maybe real closed rings should be defined as "Every monic odd degree polynomial has a root" + other stuff?

[Yaël Dillies]

This condition is obviously equivalent to the usual definition for fields. My point is that the naive definition not generalizing doesn't mean it's impossible to generalise

[Artie Khovanov]

In my opinion, the discussion about the right generality to state this definition in should be largely independent of the typeclass synthesis issue I am having. If my definition of real closed field is genuinely technically infeasible, Mathlib has much bigger problems.

[Edward van de Meent]

Technically, a * X - 1 having a root for all Nonzero a doesn't mean the ring is a field, the ring can still be trivial...

[Aaron Liu]

it's also semireal

[Aaron Liu]

so -1 isn't a sum of squares

[Artie Khovanov]

Sorry but this is quite a lot of noise to me. Does anybody have any technical suggestions about the typeclass synthesis?

[Kevin Buzzard]

What does your trace look like? Can you generate something like Junyan just posted?

[Artie Khovanov]

If you'd like to generalise the definition of real closed fields, I'd really welcome suggestions - at this other topic

[Kevin Buzzard]

The reason I'm asking about the trace is that when typeclass inference was going nuts when doing integers of number fields, we looked at the traces, saw what the problem was, and fixed it by making a definition irreducible.

[Junyan Xu]

It's possible to add the nolint simpNF attribute but I was told it's the last resort. IMO the 20000-heartbeat threshold for instance synthesis is too low; it only takes a split of a second. We could increase it for the simpNF linter, or globally.
Another idea is that Lean could introduce anti-instances to terminate typeclass searches early if the goal is impossible within a particular context. That would massively encourage inclusion of counterexamples in mathlib.

[Artie Khovanov]

Kevin Buzzard said:

Yes, ideally the fix for this is to stop the tour from happening. If you switch off simp tracing and switch on trace.Meta.synthInstance or whatever it's called, can you see where things begin to go pear-shaped?

Yeah so: FaithfulSMul R M -> Module.Invertible R M -> Module.FaithfullyFlat R M -> Nontrivial M and Module.Free R M
and then we're off to the races with that Nontrivial M :frowning:

[Artie Khovanov]

now, a characteristic zero ring is nontrivial, so it's enough to be a real closed field (!) and that tips the synthesis over the edge of a timeout
but of course every silly thing like this anywhere in Mathlib gets tried

[Artie Khovanov]

.

[Artie Khovanov]

.

[Artie Khovanov]

.

[Artie Khovanov]

Oh it gets so much worse: (P.ofAlgEquiv e).Ring can be viewed as a quotient(?) of MvPolynomial ι R, so showing nontriviality can apparently be reduced to showing ι is nontrivial. But ι is just a random type we know literally nothing about! So it does the full search but it can't possibly get anywhere because there are literally zero instances on ι!

[Artie Khovanov]

image.png

[Artie Khovanov]

And the Nontrivial (P.ofAlgEquiv e).Ring appears from "Nontrivial R and PreValuationRing R implies IsLocalRing R", which comes from "IsSimpleRing R and Nontrivial M implies FaithfulSMul R M." All very silly when you think about it.

[Artie Khovanov]

I think these instances would fail much faster if Nontrivial appeared last in the list of arguments.

[Artie Khovanov]

Bad instances: docs#Module.FaithfullyFlat.instOfNontrivialOfFree, docs#ValuationRing.isLocalRing
I wonder what would happen if we literally just swapped the arguments?

[Artie Khovanov]

#34475

[Artie Khovanov]

-- #34475: Used 15502 heartbeats
progress!

[Artie Khovanov]

here's the whole-Mathlib benchmark

[Yaël Dillies]

Also note that I hit the exact same timeout in #34203. Sorry for not noticing earlier

[Artie Khovanov]

Oh lol well that fixes my original problem (because you added the nolints)
But I still want to PR a robust fix for these timeouts
What do people think of my attempt?

[Artie Khovanov]

The trace still goes on a bit of a tour but it's not as egregious

[Yaël Dillies]

Your attempt looks very promising indeed

[Yaël Dillies]

Hopefully Nontrivial isn't so expensive to (fail to) synthesize though?

[Artie Khovanov]

Well it's not just one Nontrivial instance; it's at least 2 and probably more. The trace gets 5x shorter lol.

[Artie Khovanov]

But yeah it seems relatively expensive!

[Yaël Dillies]

My opinion is that your PR should be merged, but also we should separately investigate making TC search fail faster on Nontrivial

[Artie Khovanov]

I'll have a look when I get time to see if the remaining trace can be improved much

[Artie Khovanov]

I think we should merge #34475 for now, I made the obvious changes
edit: doesn't seem to work on latest master, looking into it

[Artie Khovanov]

For a robust fix I think we might need to encapsulate some defs better; see #mathlib4 > JacobiZariski is slow.

[Artie Khovanov]

How do I get a typeclass synthesis trace that also tells me how long each step took?

[Aaron Liu]

try set_option profiler true

[Artie Khovanov]

nah that gives me the total time
I want the time for each bit in the trace
image.png

[Artie Khovanov]

I've seen it in other threads but I don't know the command for it

[Artie Khovanov]

Proposal : make IsArtinian into a def.

abbrev IsArtinian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop :=
  WellFoundedLT (Submodule R M)

There are lots of ways to synthesise well-foundedness, and they take you into category theory and all sorts of other inappropriate parts of the library.

[Artie Khovanov]

image.png

[Artie Khovanov]

this change would probably cause a lot of instances to be duplicated, unfortunately

[Snir Broshi]

Perhaps

set_option trace.Meta.synthInstance true in

or

set_option trace.profiler.useHeartbeats true in
set_option trace.profiler.threshold 1 in
set_option trace.profiler true in

?

[Artie Khovanov]

First one is what gives me the screenshot I posted

[Artie Khovanov]

Junyan Xu said:

I don't know what's the tour happening in your case, but notice even synthesizing something as simple as Nonempty can be heavy (goes up to NormedField etc.). The following trace was what prompted me to introduce a dedicated class IsGCDMonoid in #34179 rather than reusing Nonempty:
image.png

What profiler settings are you using here? I haven't been able to get the heartbeat count on the left!

[Kevin Buzzard]

Artie Khovanov said:

nah that gives me the total time
I want the time for each bit in the trace
image.png

Click on those little triangles to unfold them! (with the profiler on)

[Junyan Xu]

I just used

set_option trace.profiler true
set_option trace.profiler.useHeartbeats

which is what Kevin taught me.

I think it's a good idea to change IsArtianian and perhaps also IsNoetherian; you can refer to #27427 as an examplar.

[Violeta Hernández]

FTR I'm the one responsible for making IsArtinian into an abbrev, mostly as a way to dogfood the then-new WellFoundedLT typeclass: #15797

[Violeta Hernández]

docs#IsNoetherian isn't actually defined as WellFoundedGT (Submodule R M), it's instead defined as all submodules being finitely generated. I don't know enough ring theory to tell if we could/should do something analogous for IsArtinian.

[Artie Khovanov]

The proposal is to change abbrev to class extends ie keep the instance in the good direction but not the bad one

[Violeta Hernández]

The good direction being IsArtinian → WellFoundedLT, right?

[Junyan Xu]

Oh yeah thanks, I forgot how IsNoetherian is defined :man_facepalming:

[Artie Khovanov]

import Mathlib

set_option trace.profiler true
set_option trace.profiler.useHeartbeats true

example {R S T ι : Type*}
    [CommRing R] [CommRing S]
    [Algebra R S] (P : Algebra.Generators R S ι) [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T) :
    RingHom.ker (algebraMap (P.ofAlgEquiv e).Ring T) = sorry := by
  simp

variable {R S T ι : Type*}
    [CommRing R] [CommRing S]
    [Algebra R S] (P : Algebra.Generators R S ι) [CommRing T] [Algebra R T] (e : S ≃ₐ[R] T)

#count_heartbeats in
#synth FaithfulSMul (P.ofAlgEquiv e).toExtension.Ring T
-- #32984 : 20223 hb
-- master : 23311 hb

(pasting my test code here for later)