deterministic timeout

Stream: general

[Zesen Qian]

In general, how to solve "(deterministic) timeout" error?

[Zesen Qian]

I have tried increasing the timeout limit, so it must be my code.

[Simon Hudon]

Yes and it depends on the tactics that you use. Often, simp is the offender. When you give it a list of rules that do not converge, it will just keep going.

[Jeremy Avigad]

I am working on a program verification project that automatically generates Lean files with large proofs. They use the simplifier in an essential way, and elaboration often takes on the order of 30 seconds or more.

Now I have a large proof that fails with a deterministic timeout. By manually breaking it into smaller proofs, I can get it to elaborate. By commenting out parts of the original proof, I can find the part that puts Lean over the edge.

I tried putting set_option timeout 300000 before the proof (and using other big numbers), but it still fails at exactly the same place. Is there anything else I can do to get Lean to try harder? Or is it possible that the deterministic timeout message is standing proxy for some other problem?

[Gabriel Ebner]

set_option timeout is completely ignored as far I can remember. The timeout setting is set by a command line argument. In vscode you can configure it using the Lean: Time Limit setting.

[Jeremy Avigad]

That worked! Many thanks.

[Eric Rodriguez]

getting some in #12836 which adds zero new simp lemmas - does anyone know what's going on? I'm trying to reerun CI as I can't reproduce locally

[Kyle Miller]

On my machine, set_option profiler true for docs#topological_vector_bundle.trivialization.prod gives

662:5: parsing took 373ms

662:5: elaboration of prod took 20.9s

662:5: type checking of prod took 345ms

662:5: decl post-processing of prod took 344ms

I don't know how the deterministic timeout system works, but 20.9s is pretty long and maybe you were just unlucky and by chance it timed out.

I wonder if it's worth splitting that definition up somehow so that it elaborates proofs and the definition separately.

[Eric Rodriguez]

I re-ran and it went away, so it doesn't seem very deterministic :/ but maybe it's worth splitting up that proof anyways

[Oleksandr Manzyuk]

A Lean n00b here. I'm working through the exercises for LFTCM2020, which are a lot of fun! (I was a mathematician before making a career switch 10 years ago and starting working as a software developer. I've started picking up Lean recently as a hobby at the intersection of mathematics and computer science/type theory/functional programming.) Unfortunately, once I've reached the exercises in category theory, things have become very slow and I often get "(deterministic) timeout", which significantly degrades the experience interacting with the theorem prover making it a lot less responsive and sometimes I simply don't know how to make progress because the obvious thing doesn't work.

For example, here is my attempt at exercise 4. At line 56, the goal is as follows:

R : CommRing,
f : (coyoneda.obj (op (CommRing.of (polynomial ℤ)))).obj R
⊢ eval₂ (algebra_map ℤ ↥R) (f.to_fun X) X = f.to_fun X

which seems to match the polynomial.eval₂_X lemma, but applying or rewriting with it causes the dreaded deterministic timeout. Does anyone have an idea what might be going on here? Am I missing anything?

[Thomas Browning]

I have no idea why, but it seems that hom := { app := λ R, λ r, polynomial.eval₂_ring_hom (algebra_map ℤ R) r },is a major contributor to the timeout.

[Junyan Xu]

If that's the case then probably it's because the tactic that automatically fils in the naturality' fields runs too slowly, and you might consider supplying an explicit proof.

You may also split out the individual fields hom, inv etc. as individual defs.

[Oleksandr Manzyuk]

Thank you. I suspected that the automation was to blame. I'll try providing explicit proofs. I'm curious what the approach to working with the category theory part of the library should be. Should one begin by writing out every proof manually and then try and see which of those could be filled in by automation? Or should one try to leave out as much as possible and only manually fill in the proofs that the automation is failing to provide? I'm leaning towards the former option but I'm curious to hear about other people's experience with the category theory library. (I was a category theorist in the previous life, and I was hoping to eventually contribute something to mathlib, e.g., formalisation of multicategories, so I'm trying to learn and understand how the existing category theory library is structured.)

[Ruben Van de Velde]

It seems like mostly the latter approach looking in from the outside

[Oleksandr Manzyuk]

Interesting. Filling in the proof of naturality of hom did indeed allow me to finish the proof of inv_hom_id' and complete the definition of CommRing_forget_representable. At the moment, the proof of naturality also relies on automation but apparently fleshes out enough structure to prune the search? I just did intros R S f, and then the goal is equality of two morphisms, so I used ext, which created two subgoals. I tried to use simp to clean them up a little but it just solved them (after some crunching). Once simp succeeded, is it useful to use simp? to get a list of simplification lemmas used and replace simp with simp only [...]?

[Arthur Paulino]

Yes, and you can also try squeeze_simp, which might be slower but gets it right more often

[Oleksandr Manzyuk]

Arthur Paulino said:

Yes, and you can also try squeeze_simp, which might be slower but gets it right more often

Thank you, I didn't know about squeeze_simp! I tried to use it and something amusing happened: when proving naturality of hom, after intros R S f, ext r c, the first goal is

RS: CommRing
f: R ⟶ S
r: (forget CommRing).obj R
c: ℤ
⊢ ⇑(ring_hom.comp (((forget CommRing).map f ≫ λ (r : (forget CommRing).obj S), eval₂_ring_hom (algebra_map ℤ ↥S) r) r) C) c = ⇑(ring_hom.comp (((λ (r : (forget CommRing).obj R), eval₂_ring_hom (algebra_map ℤ ↥R) r) ≫ (coyoneda.obj (op (CommRing.of (polynomial ℤ)))).map f) r) C) c

and squeeze_simp suggested simp only [ring_hom.eq_int_cast]. My first thought when looking at that goal was "That's a mouthful, let me clean it up first to see what's going on." So, I tried to insert dsimp before simp only [ring_hom.eq_int_cast], and the proof stopped working! It took me a while to realise that the original goal was of the form ⇑g c = ⇑h c, where g and h are two homomorphisms from ℤ, so that ring_hom.eq_int_cast could be applied directly, whereas dsimp destroyed this property of the goal (even though it made it look simpler).

[Scott Morrison]

Unless I have some reason to be confident or optimistic that the automation will fill in fields, I tend to fill them in with sorries while I write the data fields (and any proof fields which I know will need human attention). After that, you can try deleting the sorried fields to see if automation handles them.

[Oleksandr Manzyuk]

Thank you very much, @Scott Morrison I was hoping to hear your take on this.

[Violeta Hernández]

I'm getting one on Dedekind domains: https://github.com/leanprover-community/mathlib/pull/14442/files

[Anne Baanen]

This is probably related to https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/normalized_factors/near/284291719. I'd like to investigate this, but my schedule the coming week is very full...

[Violeta Hernández]

Hasn't been fixed, and it's affecting various of my PRs

[Violeta Hernández]

This is the lemma in question:

lemma ideal.count_normalized_factors_eq {p x : ideal R} (hp0 : p ≠ ⊥) [hp : p.is_prime] {n : ℕ}
  (hle : x ≤ p^n) (hlt : ¬ (x ≤ p^(n+1))) :
  (normalized_factors x).count p = n :=
count_normalized_factors_eq ((ideal.prime_iff_is_prime hp0).mpr hp).irreducible (normalize_eq _)
  (ideal.dvd_iff_le.mpr hle) (mt ideal.le_of_dvd hlt)

[Violeta Hernández]

I have no idea how to golf this, it looks very concise?

[Violeta Hernández]

I have no idea why it's even timing out

[Violeta Hernández]

This is purely term-mode, right? So why does it take so long?

[Violeta Hernández]

And why do unrelated changes push it over the edge? It's not like this is calling some simp lemma or whatever

[Damiano Testa]

I do not know the source of the timeout, but I would start looking at instance searches, if you've added typeclasses.

Regarding term-mode: such proofs tend to be faster, but that is not a rule. I've seen situations where a lemma application form in term mode times out, but by apply <same lemma> works instantly. Again, I think that it usually has to do with instance search.

[Damiano Testa]

Try seeing if by apply/exact/convert make the lemma faster. Sometimes it works...

[Violeta Hernández]

None of them seem to make it significantly faster

[Violeta Hernández]

In fact, apply and convert cause it to time-out on master

[Violeta Hernández]

By testing with a few sorries, it seems like all of the three arguments take up a lot of the runtime

[Violeta Hernández]

By the way, is it intentional that we have the hypotheses (hle : x ≤ p^n) and (hlt : ¬ (x ≤ p^(n+1)))? These seem to imply p < 1 which seems weird, but I don't know what ideal exponentiation nor comparison is supposed to be so...

[Violeta Hernández]

(not to mention, hlt should be written p^(n+1) < x instead)

[Ruben Van de Velde]

I \le J means J dvd I, iirc

[Kevin Buzzard]

What happens if you fill in the hole?

[Damiano Testa]

Which in turn should mean contain. You can probably interpret the order as containment of sets.

[Damiano Testa]

If the timeout is due to zero_le_one_class, then I would look for typeclass issues having to do with the order.

[Damiano Testa]

(not to mention, hlt should be written p^(n+1) < x instead)

I'm not sure that follows: the order is not linear. It is more like the order on order_dual (set α).

[Violeta Hernández]

Yet another one of my PRs, a very big one no less, has succumbed to this same timeout

[Violeta Hernández]

I wonder if the best solution here is to make the last three arguments into separate private lemmas

[Violeta Hernández]

I'm not familiar with the file, so I don't know if these lemmas are anything of standalone interest

[Junyan Xu]

convert ideal.dvd_iff_le.mpr hle seems faster than exact

[Junyan Xu]

same for convert mt ideal.le_of_dvd hlt

[Junyan Xu]

potential diamond?

type mismatch at application
  normalize_eq
term
  ideal.unique_units
has type
  unique (@ideal ?m_1 (@comm_semiring.to_semiring ?m_1 ?m_2))ˣ : Type ?
but is expected to have type
  unique (@ideal ?m_1 (@ring.to_semiring ?m_1 (@comm_ring.to_ring ?m_1 ?m_2)))ˣ : Type ?

[Junyan Xu]

from

lemma ideal.count_normalized_factors_eq {p x : ideal R} (hp0 : p ≠ ⊥) [hp : p.is_prime] {n : ℕ}
  (hle : x ≤ p^n) (hlt : ¬ (x ≤ p^(n+1))) :
  (normalized_factors x).count p = n :=
begin
  apply count_normalized_factors_eq ((ideal.prime_iff_is_prime hp0).mpr hp).irreducible,
  apply @normalize_eq _ ideal.cancel_comm_monoid_with_zero ideal.unique_units,
end

[Junyan Xu]

lemma ideal.count_normalized_factors_eq {p x : ideal R} (hp0 : p ≠ ⊥) [hp : p.is_prime] {n : ℕ}
  (hle : x ≤ p^n) (hlt : ¬ (x ≤ p^(n+1))) :
  (normalized_factors x).count p = n :=
begin
  apply count_normalized_factors_eq ((ideal.prime_iff_is_prime hp0).mpr hp).irreducible,
  { haveI : unique (ideal R)ˣ := ideal.unique_units, apply normalize_eq },
  convert ideal.dvd_iff_le.mpr hle,
  convert mt ideal.le_of_dvd hlt,
end

This seems fast enough (1-2s), so I'm gonna PR it! #14590

[Eric Wieser]

Doesn't look like a diamond in the usual sense, lean just can't guess what ring you're talking about.

[Yaël Dillies]

Does anyone know what's up with #14683? I'm getting a timeout on docs#intermediate_field.intermediate_field_map. It's decls post-processing that takes 39s and nothing I tried did anything.

[Yaël Dillies]

Update, I'm htting it in #14686 as well :confused:

[Junyan Xu]

Remove @[simps]: compiles in an instant
Use @[simps] noncomputable!: decl post-processing of intermediate_field_map took 19.5s

[Junyan Xu]

@Yaël Dillies

[Yaël Dillies]

noncomputable! still timed out for me :thinking:

[Yaël Dillies]

Can you see what simps generates? simps? timed out as well for me.

[Junyan Xu]

generated with [simps?] noncomputable!

[simps] > The given definition is not a constructor application:
        >   e.subalgebra_map E.to_subalgebra
        > Retrying with the options { rhs_md := semireducible, simp_rhs := tt}.
[simps] > adding projection intermediate_field.intermediate_field_map_apply_coe:
        > ∀ {K : Type u_1} {L : Type u_2} [_inst_1 : field K] [_inst_2 : field L] [_inst_3 : algebra K L]
{L' : Type u_3} [_inst_4 : field L'] [_inst_5 : algebra K L'] (e : L ≃ₐ[K] L') (E : intermediate_field K L)
(ᾰ : ↥(E.to_subalgebra.to_subsemiring)), ↑(⇑(intermediate_field_map e E) ᾰ) = ⇑e ↑ᾰ
[simps] > adding projection intermediate_field.intermediate_field_map_symm_apply_coe:
        > ∀ {K : Type u_1} {L : Type u_2} [_inst_1 : field K] [_inst_2 : field L] [_inst_3 : algebra K L]
{L' : Type u_3} [_inst_4 : field L'] [_inst_5 : algebra K L'] (e : L ≃ₐ[K] L') (E : intermediate_field K L)
(ᾰ : ↥(subsemiring.map e.to_ring_equiv.to_ring_hom E.to_subalgebra.to_subsemiring)),
  ↑(⇑((intermediate_field_map e E).symm) ᾰ) = ⇑(↑↑e.symm) ↑ᾰ

[Junyan Xu]

Sorry, it seems decl post-processing of intermediate_field_map takes 18-20s on my machine no matter whether there's noncomputable! or not, and [simps?] gives the same output. But I do get a deterministic timeout without the noncomputable!. So it seems @[simps] takes 18-20s, and computability related stuff (VM code generation?) takes much longer and yields a timeout. But why removing @[simps] makes it instant? There should still be VM code generation, no?

[Junyan Xu]

Anyway, it's easy enough to add the two auto-generated simp lemmas manually.

[Junyan Xu]

I increased time limit so that the timeout goes away, and it seems it just take 1-2 more seconds (19-20s total) for the whole declaration to compile.

[Yaël Dillies]

Do you mind filing the fix as a PR?

[Junyan Xu]

I'll attend this exhibition this afternoon (leaving in 1 hour) and don't have the time at the moment. You are welcome to submit the PR! So we've decided to go with the manual simp lemmas approach?

[Junyan Xu]

I've got some time to work out the proper forms of the two auto-generated simp lemmas in the context, but I'm leaving soon!

lemma intermediate_field_map_apply_coe (e : L ≃ₐ[K] L') (E : intermediate_field K L) (a : E) :
  ↑(intermediate_field_map e E a) = e a := rfl

lemma intermediate_field_map_symm_apply_coe (e : L ≃ₐ[K] L') (E : intermediate_field K L)
  (a : subsemiring.map e.to_ring_equiv.to_ring_hom E.to_subalgebra.to_subsemiring) :
  ↑((intermediate_field_map e E).symm a) = e.symm a := rfl

[Yaël Dillies]

Is the second one really ever going to fire?

[Junyan Xu]

I don't know if it's going to fire but it looks like a reasonable simp lemma. I just pushed to branch#intermediate_field_map_timeout without simp attribute on either lemma to see if and where they fire.

On master, removing the simps from intermediate_field_mapalso reduces
decl post-processing of intermediate_field_map from 18.3s to 46.4ms on my machine.

[Junyan Xu]

Seems the build already succeded in 4m 53s...

[Junyan Xu]

#14725

[Yaël Dillies]

Yet another timeout in file#algebraic_geometry/function_field this time. It's docs#algebraic_geometry.function_field.algebra. Any idea?

[Junyan Xu]

first observation: apply structure_sheaf.to_stalk R is about 2x faster (11.1s) than exact structure_sheaf.to_stalk R _ (29.3s). Will try to speed up it further.

Interestingly convert structure_sheaf.to_stalk R _ (11.3s) is similar to apply (but probably bad for building data instance).

[Junyan Xu]

ring_hom.to_algebra $ by { change CommRing.of R ⟶ _, apply structure_sheaf.to_stalk }

about 0.4s now!

[Junyan Xu]

#14830

[Violeta Hernández]

One of my PRs is getting a timeout on docs#exterior_algebra.graded_algebra

[Violeta Hernández]

@Eric Wieser

[Eric Wieser]

Which PR?

[Violeta Hernández]

#14884

[Violeta Hernández]

Got this on #14707 too

[Violeta Hernández]

I'm not at all familiar with this API or even the math here

[Eric Wieser]

I guess this might have been made worse by the exterior_algebra R M = clifford_algebra 0 refactor

[Eric Wieser]

Does replacing either begin/end block with sorry help?

[Junyan Xu]

No, it's typechecking graded_algebra.ι R M that is slow.

by { fapply graded_algebra.of_alg_hom, apply lift _ _, fsplit, convert graded_algebra.ι R M }

is very fast, but we certainly don't want to convert data ...

[Junyan Xu]

It's weird that the types look exactly the same but exact takes so long (10+ seconds) ...

[Junyan Xu]

It seems Lean is spending time checking the following defeq:

import algebra.direct_sum.algebra
import algebra.direct_sum.internal

open_locale direct_sum
example {S R} [comm_semiring S] [semiring R] [algebra S R] (p : submodule S R) :
  non_unital_non_assoc_semiring.to_add_comm_monoid (⨁ i : ℕ, ↥(p ^ i)) =
  direct_sum.add_comm_monoid _ _ := rfl

This rfl is fast (typechecking 15ms, elaboration 200ms), but maybe Lean is unfolding too much in the exterior algebra situation.
(cf. docs#submodule.nat_power_graded_monoid, docs#direct_sum.algebra )

[Junyan Xu]

Wow, let := graded_algebra.ι R M, exact this, is also super fast! Why is it different from exact graded_algebra.ι R M??
I see the produced term is different:

 exact let this : M →ₗ[R] ⨁ (i : ℕ), ↥((ι R).range ^ i) := graded_algebra.ι R M
in this

[Kevin Buzzard]

With the let version, laan is free to let the type be whatever it wants, so unification is happening in a different order

[Junyan Xu]

I hope terms lilke exact let this : ... in this won't pose much an annoyance? If so then maybe that's the solution to be PR'd...

[Junyan Xu]

Or maybe there's some easy change that can be inserted ..

[Junyan Xu]

OK, apply works, as easy as that!

[Junyan Xu]

Another fix needs to be applied to the proofs: graded_algebra.ι_apply needs to be replaced by graded_algebra.ι_apply R M at two places (reduces from 10-12s to 3s).

[Junyan Xu]

#14967

[Eric Wieser]

Thanks!

[Eric Wieser]

A new one in file#number_theory/cyclotomic/primitive_roots here (and some other builds): https://github.com/leanprover-community/mathlib/runs/7120067385?check_suite_focus=true#step:6:12

[Riccardo Brasca]

I am going to sleep now, but I bet this is caused by simps.

[Paul Lezeau]

I'm running into a timeout on #15000 when working with polynomial rings. An mwe would be something like

import ring_theory.dedekind_domain.ideal
import ring_theory.ideal.operations
import ring_theory.polynomial.basic
import ring_theory.unique_factorization_domain

open ideal polynomial unique_factorization_monoid
open_locale classical

variables {R : Type*} [comm_ring R] [is_domain R]  [is_dedekind_domain R]

noncomputable instance {I: ideal R} [hI : is_maximal]  : field (R ⧸ I) :=
 ((ideal.quotient.maximal_ideal_iff_is_field_quotient I).mp hI).to_field

--deterministic timeout
def problematic_definition {I : ideal R}  (f : polynomial R)
 (hI : is_maximal I) :
  {J : ideal (polynomial $ R ⧸ I ) |
    J ∈ normalized_factors (ideal.span ({ map I^.quotient.mk f } : set (polynomial $ R ⧸ I))) }
:= sorry

The issue seems to come from normalized_factors, since removing it makes the statement work fine.
For context, I am trying to construct an equiv of the form

def normalized_factors_equiv [is_domain R] [is_dedekind_domain R] (f : polynomial R) (I : ideal R)
  (hI : is_prime I) (hI' : I  ≠ ⊥ ) :
  {J : ideal S | J ∈ normalized_factors (I.map (algebra_map R S)) } ≃
  {J : ideal (polynomial $ R ⧸ I ) |
    J ∈ normalized_factors (ideal.span ({ map I^.quotient.mk f } : set (polynomial $ R ⧸ I))) }
:= sorry

[Paul Lezeau]

Does anyone know what might be causing this?

[Alex J. Best]

Did you try adding noncomputable! def?

[Paul Lezeau]

I'll try that now!

[Riccardo Brasca]

You can also make it a lemma until it is sorry free, this sometimes helps.

[Paul Lezeau]

The noncomputable! def fix worked, thanks !

[Paul Lezeau]

Riccardo Brasca said:

You can also make it a lemma until it is sorry free, this sometimes helps.

I'll keep that in mind!

[Moritz Doll]

Sorry, stupid question time: how do I increase the time limit in VSCode, the tips and tricks say there is a setting Lean Time Limit, but ctrl+shift+p and Lean: Time Limit does not work

[Moritz Doll]

less stupid question: why does squeeze_simp take so much longer than simp?

[Moritz Doll]

answer to first question is ctrl+, and then searching for lean time limit

[Floris van Doorn]

It should be "Settings (ctrl+,) -> search for lean time limit"

[Floris van Doorn]

(please also make a PR to tips and tricks fixing the tip)

[Floris van Doorn]

I believe squeeze_simp does some work after the simp is done minimizing the list lemmas it found (maybe it rewrote with foo, but the simp will result in the same state if foo was never applied).

[Floris van Doorn]

Oh, I should have read your third message before answering your first :-)