timeout with super weird logs

Stream: general

[Kevin Buzzard]

Maria Ines showed me the following crazy timeout this morning. I've never seen anything like it.

import field_theory.normal
import field_theory.is_alg_closed.algebraic_closure

variables (K : Type*) [field K] {L : Type*} [field L] [algebra K L]
  (E : intermediate_field K L)

def foo1 : is_scalar_tower K E E := infer_instance

-- comment this out for the fun to start
local attribute [instance] foo1

-- uncomment this to view the fun
-- set_option trace.class_instances true

def foo2 : is_scalar_tower K E (algebraic_closure E) := infer_instance

The above code, as it stands, works fine and compiles quickly. But Lean needs the instance shortcut foo1 to make this quick. If you comment out local attribute instance [foo1] then Lean spends a long time on foo2. I've set my "Lean : time limit" in VS Code to be 800000 (I think the default is 100000?) and foo2 does manage to compile when foo1 is commented out, but it's very slow. But if you switch trace.class_instances on and click on infer_instance (the proof of foo2) then instead of seeing what I expected (Lean just getting lost and trying a bunch of crazy things) the vast vast majority of the logs comprises of around 47,000 repeated occurrences of the same two lines:

[class_instances] cached failure for @algebra L ↥E (@semifield.to_comm_semiring L (@field.to_semifield L _inst_2))
  (@ring.to_semiring ↥E (@division_ring.to_ring ↥E (@field.to_division_ring ↥E E.to_field)))
[class_instances] cached failure for @algebra L ↥E (@semifield.to_comm_semiring L (@field.to_semifield L _inst_2))
  (@ring.to_semiring ↥E (@division_ring.to_ring ↥E (@field.to_division_ring ↥E E.to_field)))
[class_instances] cached failure for @algebra L ↥E (@semifield.to_comm_semiring L (@field.to_semifield L _inst_2))
  (@ring.to_semiring ↥E (@division_ring.to_ring ↥E (@field.to_division_ring ↥E E.to_field)))
...

-- literally the same thing, again and again and again. Maria's original example was

lemma foo : algebra.is_algebraic K (normal_closure K E (algebraic_closure E)) :=
begin
  sorry
end

and for me, if I put logging trace class instances on for that, then it takes my machine down (it becomes unresponsive and I have to wait for the OS to announce that VS Code isn't responding).

Whatever is going on?

[Anne Baanen]

I've seen this before where there's a nontrivial equality in the type, and for a reason that I didn't quite understand the elaborator doesn't look up things in the cache...

[Anne Baanen]

I think this thread has the original report of the issue

[Eric Wieser]

47000 repetitions is a rookie number, I got up to 2.5 million last time!

[Thomas Browning]

Is this at all related to the algebraic closure and splitting field refactors that were discussed in the FLT regular chat?

[María Inés de Frutos Fernández]

I think the problem has to do with intermediate_field. The following code is very quick, but if you invert the order of foo and bar, elaboration of bar takes 18.5s on my laptop:

import field_theory.normal
import field_theory.is_alg_closed.algebraic_closure

variables (K : Type*) [field K] (L : Type*) [field L] [algebra K L]
  (h_alg_L : algebra.is_algebraic K L) (E : intermediate_field K L)

instance foo : is_scalar_tower K L (algebraic_closure L) := infer_instance
instance bar : is_scalar_tower K E (algebraic_closure E) := infer_instance

[Eric Wieser]

Does making it an old-style structure make things better?

[Jireh Loreaux]

I'm also hitting a really weird timeout, and if someone could help, I would really appreciate it; I saw a bunch of repeated things, similar to the above issue when I trace the class instances. It's on branch#j-loreaux/refactor-alg-equiv on the declaration docs#hahn_series.of_power_series_alg. This declaration is a bit slow on master too. If I increase the timeout high enough (500000 seemed to work), then it does eventually compile.

For some context: on this branch I am refactoring alg_equiv so that it takes a map_smul field instead of commutes; this allows to unify non-unital and unital algebra equivalences, similar to ring_equiv. (Note: alg_hom is untouched.) The only new instance I introduce is alg_equiv_class.to_smul_hom_class with a super low priority (50).

[Jireh Loreaux]

Also weird: if you put a sorry after the last tactic, then the previous line results in "goals accomplished" virtually instantaneously, and but complains at the sorry about "no goals" for obvious reasons. I assume this behavior has something to do with tactic mode not doing the same checks as the kernel, thinking it's finished, and then because of the sorry the term never gets passed to the kernel.

[Damiano Testa]

While this does not address the issues, recover may give you access to the "hidden" goal. :shrug:

[Jireh Loreaux]

tried, got nothing

[Mauricio Collares]

Do you still get timeouts if you remove the [simps] attribute? Other stuff will break, of course.

[Jireh Loreaux]

without simps its instant

[Jireh Loreaux]

Is the solution to just manually add the simps lemmas?

[Mauricio Collares]

I don't know if it is the correct solution, but at least it's a workaround I've seen used a few times before

[Jireh Loreaux]

Thanks. I spent longer on that than I care to admit last night trying to figure out what the problem was. I thought I was just being stupid, or else some weird type class inference issue.

[Anne Baanen]

You can also try some of the docs#simps_cfg options, e.g. @[simps {simp_rhs := ff}]