# Zulip Chat Archive

## Stream: general

### Topic: Timeout in the kernel

#### Anne Baanen (Jul 12 2022 at 08:50):

I'm getting a timeout error in #14894 which from the profiler output appears to be thrown in the kernel typechecking stage, after elaboration finishes relatively quickly (less than half a second). Any tips on fixing a timeout in the kernel like this?

#### Anne Baanen (Jul 12 2022 at 08:52):

As far as I can tell, there is no heavy refl going on: if I replace the `show`

with a `rw`

, the same symptoms occur.

#### Anne Baanen (Jul 12 2022 at 09:02):

I've got a debug build in GDB, the timeout really comes from a kernel defeq check about 150 calls down the stack, so it's definitely the kernel going down some weird path here. Also something I learned today: apparently kernel checking starts with a fresh heartbeat counter since it's in a new thread.

#### Anne Baanen (Jul 12 2022 at 10:32):

By the way, after merging (in particular after #15251) the timeout doesn't appear in the build but it's still there in my editor.

#### Anne Baanen (Jul 12 2022 at 10:48):

I'm just going to go ahead and split the lemma into two parts since it's already dangerously close to timing out on master.

#### Kevin Buzzard (Jul 16 2022 at 13:57):

@Anne Baanen in your GitHub commit message regarding this you make claims of the form "this used to take 90k heartbeats, now it only takes 60k". How are you measuring this?

#### Anne Baanen (Jul 16 2022 at 17:20):

I used a low-tech way: write `set_option profiler true`

before the declaration and `#exit`

after, then run the command `lean -T${N} ${FILE}`

(where `${N}`

is the number of heartbeats and `${FILE}`

the file containing the declaration). When a timeout error pops up, if the profiler output mentions "decl post-processing" then the timeout is probably in the kernel. Then use binary search on `${N}`

to determine the approximate value for which the timeout occurs.

#### Junyan Xu (Jul 17 2022 at 06:42):

Here's one more presumable example of timeout in the kernel; if the final `sorry`

is there, it shows "goals accomplished", but once `sorry`

is removed it timeouts.

```
import category_theory.products.basic
import category_theory.functor.currying
import category_theory.products.associator
import category_theory.category.Cat
open category_theory
universes u₁ u₂ u₃ v₁ v₂ v₃
variables (A : Type u₁) [category.{v₁} A]
(B : Type u₂) [category.{v₂} B]
(C : Type u₃) [category.{v₃} C]
def prod_functor_to_functor_prod : (A ⥤ B) × (A ⥤ C) ⥤ A ⥤ B × C :=
curry_obj $ functor.prod'
(uncurry.obj $ category_theory.prod.fst _ _)
(uncurry.obj $ category_theory.prod.snd _ _)
def functor_prod_to_prod_functor : (A ⥤ B × C) ⥤ (A ⥤ B) × (A ⥤ C) :=
functor.prod'
(curry_obj $ uncurry.obj (𝟭 _) ⋙ category_theory.prod.fst B C)
(curry_obj $ uncurry.obj (𝟭 _) ⋙ category_theory.prod.snd B C)
@[simp] lemma eq_to_hom_fst {X Y : B × C} (h : X = Y) :
prod.fst (eq_to_hom h) = eq_to_hom (congr_arg prod.fst h) :=
eq_to_hom_map (category_theory.prod.fst B C) h
@[simp] lemma eq_to_hom_snd {X Y : B × C} (h : X = Y) :
prod.snd (eq_to_hom h) = eq_to_hom (congr_arg prod.snd h) :=
eq_to_hom_map (category_theory.prod.snd B C) h
def hom_inv_id' : prod_functor_to_functor_prod A B C ⋙ functor_prod_to_prod_functor A B C = 𝟭 _ :=
begin
dsimp [prod_functor_to_functor_prod, functor_prod_to_prod_functor, curry_obj, uncurry],
apply category_theory.functor.ext,
{ intros, ext; simp },
{ rintro ⟨⟨_⟩, ⟨_⟩⟩, simp }, sorry, -- elaboration of hom_inv_id' took 5.29s
-- remove sorry: timeout (more than one minute)
end
```

Last updated: Dec 20 2023 at 11:08 UTC