Timeout in the kernel

Stream: general

[Anne Baanen]

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]

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]

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]

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]

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]

@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]

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]

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