Zulip Chat Archive

Stream: general

Topic: timeout with super weird logs

Kevin Buzzard (Sep 14 2022 at 18:32):

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)) :=

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 (Sep 14 2022 at 19:23):

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 (Sep 14 2022 at 19:24):

I think this thread has the original report of the issue

Eric Wieser (Sep 14 2022 at 20:35):

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

Thomas Browning (Sep 15 2022 at 00:09):

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 (Sep 15 2022 at 08:33):

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 (Sep 15 2022 at 12:59):

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

Jireh Loreaux (Sep 16 2022 at 14:15):

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 (Sep 16 2022 at 14:19):

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 (Sep 16 2022 at 14:21):

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

Jireh Loreaux (Sep 16 2022 at 14:21):

tried, got nothing

Mauricio Collares (Sep 16 2022 at 14:22):

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

Jireh Loreaux (Sep 16 2022 at 14:23):

without simps its instant

Jireh Loreaux (Sep 16 2022 at 14:24):

Is the solution to just manually add the simps lemmas?

Mauricio Collares (Sep 16 2022 at 14:26):

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 (Sep 16 2022 at 14:32):

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 (Sep 16 2022 at 14:58):

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

Last updated: Aug 03 2023 at 10:10 UTC