Stream: general

Topic: Timeout issues with auto_params

Eric Wieser (Nov 04 2020 at 22:52):

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 (Nov 04 2020 at 23:09):

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 },


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

Adam Topaz (Nov 04 2020 at 23:11):

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

Eric Wieser (Nov 04 2020 at 23:11):

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

Eric Wieser (Nov 04 2020 at 23:12):

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

Eric Wieser (Nov 04 2020 at 23:13):

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 (Nov 04 2020 at 23:14):

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

Adam Topaz (Nov 04 2020 at 23:17):

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

Eric Wieser (Nov 04 2020 at 23:20):

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

Eric Wieser (Nov 04 2020 at 23:20):

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

Bhavik Mehta (Nov 05 2020 at 11:17):

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 (Nov 05 2020 at 11:33):

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 (Nov 05 2020 at 12:15):

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

Bhavik Mehta (Nov 05 2020 at 12:16):

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 (Nov 05 2020 at 12:17):

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

Kevin Buzzard (Nov 05 2020 at 12:22):

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 (Nov 05 2020 at 12:29):

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

Bhavik Mehta (Nov 05 2020 at 12:32):

My guess would be that you could do either

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 } },


where there are two auto-params hidden, or

def adj : free R ⊣ forget (Algebra R) :=
{ 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 (Nov 05 2020 at 12:32):

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

Bhavik Mehta (Nov 05 2020 at 12:34):

Yeah I personally find that version more convenient in practice

Eric Wieser (Nov 05 2020 at 12:44):

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

Eric Wieser (Nov 05 2020 at 12:45):

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

Bhavik Mehta (Nov 05 2020 at 12:45):

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

Eric Wieser (Nov 05 2020 at 12:45):

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 (Nov 05 2020 at 12:49):

Updated #4908 to use the new approach, thanks!

Last updated: May 11 2021 at 21:10 UTC