timeout fixed by changing def to lemma

Stream: general

[Kevin Buzzard]

For the third time this month someone at Imperial (this time Jujian Zhang) has a situation where a construction seems to work fine but the kernel goes into a loop when trying to accept it. In all cases this happens in a def, and if the def is changed to lemma or example then the loop does not occur (but of course this is not a workaround because it needs to be a def). @Eric Wieser expressed some surprise the first time he saw this phenomenon. One hypothesis is that Lean is getting stuck working out whether something is noncomputable or not. Is this a feasible hypothesis? What are other possibilities which might cause this issue? Jujian hasn't minimised his example yet; the other two examples are https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/another.20really.20horrible.20timeout/near/263780183 and https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/crazy.20time-out/near/263470182 .

[Johan Commelin]

Is this only while writing the decl, or also after you are completely done?

[Eric Wieser]

I'm pretty convinced of that hypothesis, because wrapping the function in something known-noncomputable makes the problem go away, but wrapping it in something known-computable does not

[Gabriel Ebner]

The noncomputability checker tries to reduce terms iirc, so I can see how that could cause timeouts. Unfortunately I don't think we have any trace options to see what whnf is doing, so debugging this might be hard. I would expect that the issue could be solved by strategically making some definitions irreducible.

[Eric Rodriguez]

we could also just add a patch to lean3 that makes something like noncomputable! which doesn't try to check if you're wrong

[Eric Rodriguez]

i'm not sure if that will carry over well on synport, however...

[Kevin Buzzard]

Johan if you want to see it with your own eyes then Amelia's example is the simplest:

import field_theory.is_alg_closed.algebraic_closure

variables (K : Type*) [field K] (Γ₀ : Type*)
  [linear_ordered_comm_monoid_with_zero Γ₀]

def hmm : valuation (algebraic_closure K) Γ₀ := sorry -- times out

[Kevin Buzzard]

Change the def to a lemma and it's fine.

[Johan Commelin]

Yes, you have a sorry right there.

[Johan Commelin]

I think that's a known bug.

[Johan Commelin]

Write the def as a lemma, and change it to def when you are done. I had to do that 50x in LTE.

[Kevin Buzzard]

No, this is worse.

[Kevin Buzzard]

Take a look at Maria's example above -- I link to it. You get timeouts even if you complete the definition.

[Johan Commelin]

Aha, that's bad.

[Mario Carneiro]

Eric Rodriguez said:

we could also just add a patch to lean3 that makes something like noncomputable! which doesn't try to check if you're wrong

i'm not sure if that will carry over well on synport, however...

I don't see why not. We can handle pretty much anything lean 3 wants to do, we just have to have a reasonable lean 4 equivalent. In this case, that might either mean stripping the ! in the lean 4 version, or adding support for it to lean 4 if the same issue manifests in lean 4.

[Eric Rodriguez]

Kevin, does it actually say "deterministic timeout" on your machine or does it just never load?

[Eric Rodriguez]

image.png this issue is weird....

[Eric Rodriguez]

ok, this is way beyond my knowledge of Lean's codebase.... it doesn't seem to be solely the noncomputableness, it seems to be stuck within the compiler_step_visitor; but at some point the memory stops climbing, so there's no actual timeout because there's not enough memory allocations

[Eric Rodriguez]

trying to find exactly where this leak/infinite loop is happening is hopeless manually because I don't have access to a profiler, and it only happens after a truly enormous amount of memory has been guzzled (+, the code is super slow at failing...)

[Gabriel Ebner]

we could also just add a patch to lean3 that makes something like noncomputable! which doesn't try to check if you're wrong

i'm not sure if that will carry over well on synport, however...

We don't even have noncomputable theory in Lean 4. The Lean 4 noncomputable works like the noncomputable! you describe:

noncomputable def x := 42

[Eric Wieser]

Does that emit any diagnostics?

[Eric Wieser]

It would be a shame for lean not to remind you that something no longer needs to be noncomputable after you computablize its dependencies.

[Gabriel Ebner]

No warnings or errors.

[Kevin Buzzard]

By the way, in Amelia's example

import field_theory.is_alg_closed.algebraic_closure

variables (K : Type*) [field K] (Γ₀ : Type*)
  [linear_ordered_comm_monoid_with_zero Γ₀]

def hmm : valuation (algebraic_closure K) Γ₀ := sorry -- times out

this can be fixed by changing def to lemma, then generating the skeleton for the structure under construction, then filling in the non-Prop fields, sorrying the Prop fields, and then changing the lemma back to def. This was a trick Johan told me, he said he'd used it a ton in LTE. Maria's example (the subtype.val example) is nastier (and doesn't quite compile with mathlib master: the line noncomputable instance : field (K_v K v) := @field_completion K _ (us' v) (tdr' v) _ (ug' v) _ needs to have the last _ removed nowadays) because all definitions are there (and the variant she had had no sorrys at all IIRC). The timeout is extremely brittle -- Gabriel suggests fixing it by making things irreducible and I can't get this to work, but you can just add more things (e.g. making a new declaration P so that the subtype is {x // P x} "fixes" it). What scares me a bit about the latter approach is that the timeout might reappear the moment P is unfolded. But I've not seen this happening in practice.

...
-- name the killer predicate
def P (x : K_hat R K) := ∃ (v : maximal_spectrum R), (x v)⁻¹ = 37

-- safe subtype
def foo1 := { x : K_hat R K // P R K x }

-- bad subtype
def foo2 := { x : K_hat R K // ∃ (v : maximal_spectrum R), (x v)⁻¹ = 37 }

example : @foo1 = @foo2 := rfl -- fine

def bar1 : foo1 R K → K_hat R K := λ x, x.1 -- fine

def bar2 : foo2 R K → K_hat R K := λ x, x.1 -- times out

[Kevin Buzzard]

Minimising (i.e. removing all mathlib imports) would be a bunch of work because I would have to set up a chunk of the algebra hierarchy and also there is a bunch of topology happening (completion of a topological field is a topological field) which seems to be important. Even extremely innocuous changes such as changing ∃ to ∀ in foo2 make the problem go away, so it's not even clear that I would succeed; furthermore Gabriel has suggested that even if I did succeed then it might be very hard to figure out the problem, so I am minded to leave this for now. Initially I was worried that doing things like defining P above were just postponing the problem (i.e. that it would blow up in our face at the next definition), but perhaps they really should be regarded as a solution.

[Gabriel Ebner]

Sorry, my theory turned out to be wrong. It's not the noncomputable check that's timing out, but the VM compilation (in case you ever wanted to execute your hmm function).

I don't think there's any way to disable VM compilation in Lean 3 except for marking things as noncomputable. So this works as a workaround:

import field_theory.is_alg_closed.algebraic_closure

noncomputable def force_noncomputable {α : Sort*} (a : α) : α :=
  function.const _ a (classical.choice ⟨a⟩)

@[simp]
lemma force_noncomputable_def {α} (a : α) : force_noncomputable a = a := rfl

variables (K : Type*) [field K] (Γ₀ : Type*)
  [linear_ordered_comm_monoid_with_zero Γ₀]

noncomputable def hmm : valuation (algebraic_closure K) Γ₀ :=
  force_noncomputable sorry  -- no longer times out

[Kevin Buzzard]

@Jujian Zhang can you get your code working with this? I've checked and it seems to solve both Amelia and Maria's problems. But with your sheaf I get

-- still (deterministic) timeout
example (X : Top) (ℱ : @presheaf BundledModule BundledModule.is_cat X) [PresheafOfModules2 ℱ]:
PresheafOfModules1 X :=
force_noncomputable { 𝒪 := { obj := λ U, (ℱ.obj U).R,
         map := λ _ _ h, (ℱ.map h).1 },
  ℱ :=
    force_noncomputable { obj := λ U, AddCommGroup.of (ℱ.obj U).M,
      map := λ U V h, force_noncomputable (@AddCommGroup.of_hom (AddCommGroup.of (ℱ.obj U).M) (AddCommGroup.of (ℱ.obj V).M) _ _
        { to_fun := force_noncomputable (ℱ.map h).2,
          map_zero' :=  linear_map.map_zero _,
          map_add' := λ m m', begin
            simp,
          end, }), },
  is_module := λ U, begin
    dsimp only [AddCommGroup.coe_of], apply_instance,
  end,
  res_compatible := λ U V h r m, begin
    dsimp only [AddCommGroup.coe_of, linear_map.map_zero, functor.map_comp, functor.map_id] at *,
    erw PresheafOfModules2.res_compatible U V h r m,
    erw [smul_def'],
  end}

As you can see I just threw in force_noncomputable here there and everywhere and it didn't fix it (unless now it's actually timing out because the proof was already slow). But I know that you refactored the code after you showed it me. If you're interested in following this up can you create an example which depends only on mathlib rather than on your sheaf of modules work? I would be very interested to see if Gabriel's approach can be used to avoid your timeout!

[Jujian Zhang]

noncomputable def force_noncomputable {α : Sort*} (a : α) : α :=
  function.const _ a (classical.choice ⟨a⟩)

@[simp]
lemma force_noncomputable_def {α} (a : α) : force_noncomputable a = a := rfl

set_option pp.implicit true

noncomputable def test (X : Top) (ℱ : @presheaf BundledModule BundledModule.is_cat X) : presheaf AddCommGroup X :=
force_noncomputable
{ obj := λ U, AddCommGroup.of (ℱ.obj U).M,
  map := λ U V h, @AddCommGroup.of_hom (AddCommGroup.of (ℱ.obj U).M) (AddCommGroup.of (ℱ.obj V).M) _ _
        { to_fun := (ℱ.map h).2,
          map_zero' :=  linear_map.map_zero _,
          map_add' := λ m m', begin
            rw [linear_map.map_add],
            sorry
          end, }, }

Unfortunately, it still gives me a timeout.

[Jujian Zhang]

This sorry will still make lean complain that there is no more goals, but removing it gives a time out.

[Jujian Zhang]

The strange thing is that for map_zero', rw linear_map.map_zero works, but linear_map.map_add doesn't work for map_add'

[Gabriel Ebner]

Can you post a #mwe (i.e., with imports, etc.) please?

[Jujian Zhang]

I am sorry about this. The context is that I am trying to work out if (opens X)\op \functor BundledModule is a sensible definition for sheaf of modules. So I had to define the category of bundled modules first. So the #mwe is really not minimal at all:

import algebra.category.CommRing
import algebra.category.Module.basic
import topology.sheaves.sheaf
import topology.category.Top.opens

open category_theory Top topological_space opposite

instance restriction_of_scalar.has_scalar {R S : CommRing.{0}} (f : R ⟶ S) (N : Module.{0} S) :
   has_scalar R N :=
{ smul := λ r m, f r • m }

@[reducible] def restriction_of_scalar.restrict {R S : CommRing.{0}} (f : R ⟶ S) (N : Module.{0} S) :
  Module R :=
{ carrier := N,
  is_module :=
  { one_smul := λ b, begin
      unfold has_scalar.smul,
      rw [ring_hom.map_one, one_smul],
    end,
    mul_smul := λ _ _ _, begin
      unfold has_scalar.smul,
      rw [ring_hom.map_mul, mul_smul],
    end,
    smul_add := λ _ _ _,by { unfold has_scalar.smul, rw [smul_add] },
    smul_zero := λ _, by { unfold has_scalar.smul, rw [smul_zero] },
    add_smul := λ _ _ _, begin
      unfold has_scalar.smul,
      rw [ring_hom.map_add, add_smul],
    end,
    zero_smul := λ _, begin
      unfold has_scalar.smul,
      rw [ring_hom.map_zero, zero_smul],
    end,
    ..(restriction_of_scalar.has_scalar f N) } }

instance restriction_of_scalar.has_scalar' {R S : CommRing.{0}} (f : R ⟶ S) (N : Module.{0} S) :
  has_scalar S (restriction_of_scalar.restrict f N) :=
{ smul := λ r n, r • n }

open restriction_of_scalar

@[simp] lemma restriction_of_scalar.smul_def' {R S : CommRing.{0}} (f : R ⟶ S)
  (r : R) (N : Module.{0} S)
  (n : restriction_of_scalar.restrict f N) :
  (r • n) = (f r • n) := rfl

def restriction_of_scalar.functor
  {R S : CommRing.{0}} (f : R ⟶ S) : Module.{0} S ⥤ Module.{0} R :=
{ obj := λ m, restriction_of_scalar.restrict f m,
  map := λ m1 m2 l,
    { to_fun := l,
      map_add' := λ x y, by rw [linear_map.map_add],
      map_smul' := λ r y, begin
        simp only [restriction_of_scalar.smul_def', ring_hom.id_apply],
        convert linear_map.map_smul l (f r) y,
      end } }

structure BundledModule :=
(R : CommRing.{0})
(M : Module.{0} R)

def restriction_of_scalar {M1 M2 : BundledModule} (f : M1.R ⟶ M2.R) : BundledModule :=
{ R := M1.R,
  M := restriction_of_scalar.restrict f M2.M }

@[simp] lemma restriction_of_scalar.R {M1 M2 : BundledModule} (f : M1.R ⟶ M2.R) :
  (restriction_of_scalar f).R = M1.R := rfl
@[simp] lemma restriction_of_scalar.M {M1 M2 : BundledModule} (f : M1.R ⟶ M2.R) :
  (restriction_of_scalar f).M = restriction_of_scalar.restrict f M2.M := rfl

def bundledMap (M1 M2 : BundledModule) : Type 0 :=
Σ (f : M1.R ⟶ M2.R), M1.M ⟶ (restriction_of_scalar f).M

instance BundledModule.is_cat : category BundledModule :=
{ hom := λ M1 M2, bundledMap M1 M2,
  id := λ M, ⟨𝟙 M.R, { to_fun := λ m, m,
                       map_add' := λ _ _, rfl,
                       map_smul' := λ _ _, rfl }⟩,
  comp := λ M1 M2 M3 f g,
    ⟨f.1 ≫ g.1,
     { to_fun := λ m, g.2 (f.2 m),
       map_add' := λ m1 m2, by simp only [linear_map.map_add],
       map_smul' := λ r m, begin
        rcases f with ⟨f, f'⟩,
        rcases g with ⟨g, g'⟩,
        dsimp only,
        rw [ring_hom.id_apply, linear_map.map_smulₛₗ, ring_hom.id_apply,
          restriction_of_scalar.smul_def', restriction_of_scalar.smul_def', comp_apply],
        convert linear_map.map_smul g' (f r) (f' m),
      end }⟩,
  comp_id' := λ M1 M2 f, begin
    ext, refl, rw heq_iff_eq, ext, refl,
  end,
  id_comp' := λ M1 M2 f, begin
    ext, refl, rw heq_iff_eq, ext, refl,
  end }


noncomputable def force_noncomputable {α : Sort*} (a : α) : α :=
  function.const _ a (classical.choice ⟨a⟩)

@[simp]
lemma force_noncomputable_def {α} (a : α) : force_noncomputable a = a := rfl

noncomputable example (X : Top.{0}) (ℱ : @presheaf BundledModule BundledModule.is_cat X) : presheaf AddCommGroup.{0} X :=
force_noncomputable
{ obj := λ U, AddCommGroup.of (ℱ.obj U).M,
  map := λ U V h, @AddCommGroup.of_hom (AddCommGroup.of (ℱ.obj U).M) (AddCommGroup.of (ℱ.obj V).M) _ _
        { to_fun := (ℱ.map h).2,
          map_zero' :=  linear_map.map_zero _,
          map_add' := λ m m', begin
            -- the goal is :
            -- ⇑((ℱ.map h).snd) (m + m') = ⇑((ℱ.map h).snd) m + ⇑((ℱ.map h).snd) m'
            rw [linear_map.map_add],
            -- sorry
          end, }, }

[Jujian Zhang]

I was trying to see if I can write down a sheaf of modules like in textbook (a sheaf of abelian groups that are modules).

[Jujian Zhang]

I though that maybe AddCommGroup.of_hom is causing trouble, but

noncomputable example (X : Top.{0}) (ℱ : @presheaf BundledModule BundledModule.is_cat X) : presheaf AddCommGroup.{0} X :=
force_noncomputable
{ obj := λ U, AddCommGroup.of (ℱ.obj U).M,
  map := λ U V h,
    { to_fun := λ m, (ℱ.map h).2 m,
      map_zero' := by rw linear_map.map_zero,
      map_add' := λ m m', begin
        rw linear_map.map_add,
        sorry
      end } }

[Jujian Zhang]

this has exactly the same problem

[Kevin Buzzard]

Note that there are prop goals there which are being proved by . obviously, this is probably what makes it slow.

[Kevin Buzzard]

In fact this works:

noncomputable example (X : Top.{0}) (ℱ : @presheaf BundledModule BundledModule.is_cat X) : presheaf AddCommGroup.{0} X :=
{ obj := λ U, AddCommGroup.of (ℱ.obj U).M,
  map := λ U V h,
    { to_fun := λ m, (ℱ.map h).2 m,
      map_zero' := by rw linear_map.map_zero,
      map_add' := λ m m', begin
        rw linear_map.map_add,
      end },
  map_id' := sorry,
  map_comp' := sorry
   }

I claim that this timeout might be being caused by an unrelated issue. Hence I claim that Gabriel has solved all our problems! Thank you Gabriel!

[Jujian Zhang]

I filled the sorries and it worked! Thank you!

[Eric Wieser]

I think force_noncomputable (maybe with another name like forbid_evaluation or classicalize) probably belongs in mathlib somewhere

[Kevin Buzzard]

Boom! And a 4th person at Imperial (@Sebastian Monnet , a Lean learner trying to do Galois theory of infinite extensions) just ran into the same issue. It's happening all the time with people doing algebra.

import tactic
import field_theory.galois

open_locale classical

-- Adjoin roots
noncomputable def root_finset {K : Type*} [field K] (p : polynomial K) (L : Type*) [field L]
  [algebra K L] : finset L :=
(p.map (algebra_map K L)).roots.to_finset


noncomputable def min_polys {K E : Type*} [field K] [field E] [algebra K E]
(h_findim : finite_dimensional K E) : finset (polynomial K) :=
finset.univ.image (minpoly K ∘ (finite_dimensional.fin_basis K E))

noncomputable def prod_min_polys {K E : Type*} [field K] [field E] [algebra K E]
(h_findim : finite_dimensional K E) : polynomial K :=
finset.prod (min_polys h_findim) (λ p, p)

--noncomputable def force_noncomputable {α : Sort*} (a : α) : α :=
--  function.const _ a (classical.choice ⟨a⟩)

noncomputable def adj_roots {K L : Type} [field K] [field L] [algebra K L]
{E : intermediate_field K L} (h_findim : finite_dimensional K E) :
intermediate_field K L :=
--force_noncomputable
intermediate_field.adjoin K (coe (root_finset (prod_min_polys h_findim) L) : set L)

Completely random deterministic timeout on perfectly type-correct code which can be fixed by uncommenting force_noncomputable. @Gabriel Ebner thank you so much for this fix. Will someone PR it to mathlib? It's genuinely fast becoming an essential trick for people working in the kind of algebraic number theory we're trying to do at Imperial.

[Kevin Buzzard]

I can do it if someone tells me where the heck to put it -- I have no idea.

[Kevin Buzzard]

I think everyone is importing field_theory.tower so probably it can go there ;-)

[Yaël Dillies]

It sounds like it should go under logic., as those are the basic files. logic.basic, maybe?

[Yaël Dillies]

Stranding it in a random file towards what you're using it for seems like the safest way to forget about it.

[Eric Rodriguez]

I think we should make it its own file & some simp lemmas just to simplify working with it

[Kevin Buzzard]

Gabriel wrote a simp lemma above

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

Eric Wieser said:

I think force_noncomputable (maybe with another name like forbid_evaluation or classicalize) probably belongs in mathlib somewhere

Did force_noncomputable make it into mathlib? I haven't found it under any of these names.

[Kevin Buzzard]

@Kyle Miller (moving this conversation from #rss ) above are some examples of timeouts fixed by force_noncomputable. The other issue I saw (some code of Ashvni's) was a definition where Lean complained whether or not you marked it noncomputable, so you couldn't get it make it un-noisy. I think @Yakov Pechersky had a mathlib-free example of this?

[Kyle Miller]

Issue lean#451 has an example of a function that's neither computable nor noncomputable. If Ashvni's issue is "rec_fn_macro only allowed in meta definitions", then doing both noncomputable theory and noncomputable might be a workaround. If I understand it right, the first command tells lean to not complain that you put noncomputable on a definition it thinks is computable, and the second command will cause Lean to compile recursive definitions using a different strategy, so you might luck out.

[Anne Baanen]

Another example of a mysterious timeout fixed by noncomputable!: #14071

[Anne Baanen]

I came across this in the subobject refactor #11759, even though this declaration should have absolutely nothing to do with subobjects...

[Kyle Miller]

My (limited) understanding is that the vm compiler starts with some very aggressive whnf calculations, which I believe has exponential behavior when typeclasses are many and deep. I don't know if that applies here.