# Zulip Chat Archive

## Stream: general

### Topic: timeout fixed by changing def to lemma

#### Kevin Buzzard (Dec 09 2021 at 13:30):

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 (Dec 09 2021 at 13:44):

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

#### Eric Wieser (Dec 09 2021 at 14:08):

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 (Dec 09 2021 at 14:15):

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 (Dec 09 2021 at 14:16):

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 (Dec 09 2021 at 14:16):

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

#### Kevin Buzzard (Dec 09 2021 at 14:31):

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 (Dec 09 2021 at 14:32):

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

#### Johan Commelin (Dec 09 2021 at 14:34):

Yes, you have a `sorry`

right there.

#### Johan Commelin (Dec 09 2021 at 14:35):

I think that's a known bug.

#### Johan Commelin (Dec 09 2021 at 14:35):

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 (Dec 09 2021 at 14:35):

No, this is worse.

#### Kevin Buzzard (Dec 09 2021 at 14:36):

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

#### Johan Commelin (Dec 09 2021 at 14:39):

Aha, that's bad.

#### Mario Carneiro (Dec 09 2021 at 17:27):

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 wrongi'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 (Dec 09 2021 at 18:24):

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

#### Eric Rodriguez (Dec 09 2021 at 18:32):

image.png this issue is weird....

#### Eric Rodriguez (Dec 09 2021 at 18:58):

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 (Dec 09 2021 at 19:00):

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 (Dec 13 2021 at 09:05):

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 (Dec 13 2021 at 09:15):

Does that emit any diagnostics?

#### Eric Wieser (Dec 13 2021 at 09:16):

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 (Dec 13 2021 at 09:29):

No warnings or errors.

#### Kevin Buzzard (Dec 13 2021 at 11:11):

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 (Dec 13 2021 at 11:18):

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 (Dec 13 2021 at 11:48):

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 (Dec 13 2021 at 12:29):

@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 (Dec 13 2021 at 13:18):

```
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 (Dec 13 2021 at 13:19):

This `sorry`

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

#### Jujian Zhang (Dec 13 2021 at 13:21):

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 (Dec 13 2021 at 13:21):

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

#### Jujian Zhang (Dec 13 2021 at 13:29):

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 (Dec 13 2021 at 13:30):

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 (Dec 13 2021 at 13:34):

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 (Dec 13 2021 at 13:34):

this has exactly the same problem

#### Kevin Buzzard (Dec 13 2021 at 13:40):

Note that there are prop goals there which are being proved by `. obviously`

, this is probably what makes it slow.

#### Kevin Buzzard (Dec 13 2021 at 13:42):

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 (Dec 13 2021 at 13:57):

I filled the `sorries`

and it worked! Thank you!

#### Eric Wieser (Dec 13 2021 at 15:02):

I think `force_noncomputable`

(maybe with another name like `forbid_evaluation`

or `classicalize`

) probably belongs in mathlib somewhere

#### Kevin Buzzard (Dec 21 2021 at 20:27):

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 (Dec 21 2021 at 20:27):

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

#### Kevin Buzzard (Dec 21 2021 at 20:38):

I think everyone is importing `field_theory.tower`

so probably it can go there ;-)

#### Yaël Dillies (Dec 21 2021 at 20:40):

It sounds like it should go under `logic.`

, as those are the basic files. `logic.basic`

, maybe?

#### Yaël Dillies (Dec 21 2021 at 20:43):

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

#### Eric Rodriguez (Dec 21 2021 at 21:15):

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

#### Kevin Buzzard (Dec 21 2021 at 21:16):

Gabriel wrote a simp lemma above

#### María Inés de Frutos Fernández (Feb 14 2022 at 12:48):

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 (Mar 11 2022 at 22:30):

@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 (Mar 11 2022 at 22:40):

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 (May 11 2022 at 14:09):

Another example of a mysterious timeout fixed by `noncomputable!`

: #14071

#### Anne Baanen (May 11 2022 at 14:10):

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

#### Kyle Miller (May 11 2022 at 19:08):

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.

Last updated: Dec 20 2023 at 11:08 UTC