Deterministic timeout in CI

Stream: general

[Adam Topaz]

CI is hitting deterministic timeouts in the following PR #10303 but I can't reproduce this on my machine.
Actually, the proof that causes issues is really not that slow on my machine. Can anyone reproduce?

[Arthur Paulino]

Does anyone know what might be happening?

[Alex J. Best]

Well looks like Adam fixed his specific issue, are you asking what can cause deterministic timeout in general? Some proofs are just too slow.

[Adam Topaz]

Yeah, I fixed it.

[Arthur Paulino]

Alex J. Best said:

Well looks like Adam fixed his specific issue, are you asking what can cause deterministic timeout in general? Some proofs are just too slow.

Ah, no. I saw the topic on my phone and I noticed that nobody had said anything so I just asked. Glad it was fixed :tada:

[Xavier Roblot]

CI has been failing repeatedly for #17212. The reason being a deterministic timeout in algebraic_geometry.structure_sheaf. Now, this file is unmodified by this PR. Still I was able to track back the problem to the import of field_theory.subfield in topology.algebra.field which I guess is imported at some point in algebraic_geometry.structure_sheaf... An easy fix would be to remove the import in topology.algebra.field and move the result using it elsewhere. But this result, which proves that the closure of a subfield is a subfield, does naturally fits there in my opinion so I am looking for some other options.
FYI, it takes about 50s for Lean to compile the file algebraic_geometry.structure_sheaf on my M1 laptop.

[Anne Baanen]

I can take a look, nothing obvious jumps out from just looking at the code. Though I recall having some timeouts in this file before.

[Xavier Roblot]

Thanks. Is there anything I can do to help?

[Anne Baanen]

I traced it to the @[simps] attribute at least, so it might just be a loop in the simp lemmas or similar.

[Anne Baanen]

Thanks for the offer, I'll experiment a bit further and let you know :)

[Anne Baanen]

It looks like the following config option fixes the timeout:

@[simps {rhs_md := tactic.transparency.semireducible}]
def global_sections_iso : CommRing.of R ≅ (structure_sheaf R).1.obj (op ⊤) :=
as_iso (to_open R ⊤)

Now to figure out why...

[Anne Baanen]

Conclusion: for some reason that I don't know how to diagnose, simps does some bad unfolds and ends up unifying in the types (which is usually a bad time). Adding the semireducible transparency helps it to choose the right path. So I think that my suggestion above is the way to go.

[Xavier Roblot]

Ok. Thanks a lot. I'll add this to the PR.

[Xavier Roblot]

Well, I am getting a timeout in algebraic_geometry/Spec.lean now. It seems to be related to a simp also. I'll see if the same fix works.

[Floris van Doorn]

Without having looked into it: if you add the @[simps] attribute to a definition whose definiens is not a constructor application, the @[simps] will call the simp tactic to compute what the right-hand side of the lemmas should be. In this case, it will apply simp on something like (as_iso (to_open R ⊤)).1 and (as_iso (to_open R ⊤)).2, which might take a long time. Writing @[simps {rhs_md := semireducible}] yourself disables this, but makes me wonder how useful the simp lemma will end up being (won't the same computation then happen whenever simp uses this lemma in a proof?)

[Yaël Dillies]

Putting it out here in case someone has time to investigate, we get timeouts in

• algebraic_topology/dold_kan/normalized:118:4
• ring_theory/adjoin_root:338:0

[Yaël Dillies]

See #17949 and #18202

[Yaël Dillies]

Opened #18207 for the first

[Anne Baanen]

Let me take a look at the adjoin_root timeout.

[Anne Baanen]

Ah, it's @[simps] on a non-constructor-application. I'll probably just replace it with manually written lemmas then.

[Anne Baanen]

#18209