Timeout issues with auto_params

Stream: general

[Eric Wieser]

In https://github.com/leanprover-community/mathlib/pull/4908#issuecomment-721985117, I found that a seemingly innocuous change resulted in a deterministic timeout in a field that I couldn't even see: it was popuated by an auto_param!

Two questions then:

• Is it possible to make it more obvious where the timeout is actually occuring?
• How can I work out why my change made things so much slower?

[Adam Topaz]

Concerning the file in question, another option is to change adj using the following code:

@[simps]
def adj_unit : 𝟭 (Type*) ⟶ free R ⋙ forget (Algebra R) :=
{ app := λ S, free_algebra.ι _ }

@[simps]
def adj_counit : forget (Algebra R) ⋙ free R ⟶ 𝟭 (Algebra R) :=
{ app := λ S, (free_algebra.lift _ id),
  naturality' := by {intros, ext, simp} }

@[simps]
def adj : free R ⊣ forget (Algebra R) :=
{ hom_equiv := λ X A,
  { to_fun := λ f, f ∘ (free_algebra.ι _),
  inv_fun := λ f, (free_algebra.lift _ f),
  left_inv := by tidy,
  right_inv := by tidy },
  unit := adj_unit _,
  counit := adj_counit _ }

It still takes a solid 35 seconds to compile this block of code on my machine.

[Adam Topaz]

That naturality' in adj_counit times out if I try to use tidy.

[Eric Wieser]

Note that in theory we can save some lines with hom_equiv := λ X A, (free_algebra.lift _).symm

[Eric Wieser]

But then the also-hidden hom_equiv_unit' and hom_equiv_counit' seem like they might be timing out

[Eric Wieser]

You could go further and set unit.app as (free_algebra.lift _).symm (alg_hom.id R _), but that doesn't seem to help with the proof

[Adam Topaz]

The fact that the auto param in the naturality' for adj_counit times out is suspicious...

[Adam Topaz]

Makes me think the issue is really somewhere else. Note free (in the safe file) also takes a while to compile

[Eric Wieser]

Oh, I totally missed that adj builds on top of the definition in free

[Eric Wieser]

If you manage to work this out, feel free to push to my branch!

[Bhavik Mehta]

It's usually not the best idea to define an adjunction using the actual definition, you're much better off using either mk_of_hom_equiv or mk_of_unit_counit, which let you provide less data. I think this should also reduce the number of auto params being used

[Kevin Buzzard]

I remember you (Bhavik) telling me this several months ago when I was making an adjunction at Xena (possibly to do with abelianisation) (and you were right). Should this be documented somewhere? Maybe a comment in the category theory library?

[Eric Wieser]

@Bhavik Mehta, can you give an example of how to apply docs#category.adjunction.mk_of_hom_equiv there?

[Bhavik Mehta]

Kevin Buzzard said:

I remember you (Bhavik) telling me this several months ago when I was making an adjunction at Xena (possibly to do with abelianisation) (and you were right). Should this be documented somewhere? Maybe a comment in the category theory library?

Yeah, I added this to the docstring of adjunction: https://leanprover-community.github.io/mathlib_docs/category_theory/adjunction/basic.html a little after we talked about it

[Eric Wieser]

None of the links in that docstring work, as the name is category.adjunction.mk_of_hom_equiv

[Kevin Buzzard]

Yeah, I added this to the docstring of adjunction: https://leanprover-community.github.io/mathlib_docs/category_theory/adjunction/basic.html a little after we talked about it

Oh nice!

[Eric Wieser]

I'll have a go at using your suggestion @Bhavik Mehta

[Bhavik Mehta]

My guess would be that you could do either

def adj : free R ⊣ forget (Algebra R) :=
adjunction.mk_of_hom_equiv
{ hom_equiv := λ X A,
  { to_fun := λ f, f ∘ (free_algebra.ι _),
    inv_fun := λ f, free_algebra.lift _ f,
    left_inv := by tidy,
    right_inv := by tidy } },

where there are two auto-params hidden, or

def adj : free R ⊣ forget (Algebra R) :=
adjunction.mk_of_unit_counit
{ unit := { app := λ S, free_algebra.ι _ },
  counit :=
  { app := λ S, free_algebra.lift _ $ id,
    naturality' := by {intros, ext, simp} } }

where again there are auto-params hidden, in either case though I guess it should be faster than the older version - if not you might be able to fill some in manually easily

[Eric Wieser]

The former looks better, given that I already have a hom_equiv instance in Type*, (free_algebra.lift _).symm

[Bhavik Mehta]

Yeah I personally find that version more convenient in practice

[Eric Wieser]

Making that change means I can no longer stick @[simps] on the definition

[Eric Wieser]

Although I don't know if there was any point having it there in the first place

[Bhavik Mehta]

Yup, you can use the semireducible trick instead though, or just hand-make the projections yourself

[Eric Wieser]

Frankly since nothing even uses the projections, and I'm only making this change because the timeout is forcing me to, I think I'll leave it without them

[Eric Wieser]

Updated #4908 to use the new approach, thanks!