Zulip Chat Archive

Stream: general

Topic: Timeout issues with auto_params


view this post on Zulip 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?

view this post on Zulip 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 },
  unit := adj_unit _,
  counit := adj_counit _ }

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

view this post on Zulip Adam Topaz (Nov 04 2020 at 23:11):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Nov 04 2020 at 23:14):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 04 2020 at 23:20):

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

view this post on Zulip Eric Wieser (Nov 04 2020 at 23:20):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Eric Wieser (Nov 05 2020 at 12:29):

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

view this post on Zulip Bhavik Mehta (Nov 05 2020 at 12:32):

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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Nov 05 2020 at 12:34):

Yeah I personally find that version more convenient in practice

view this post on Zulip Eric Wieser (Nov 05 2020 at 12:44):

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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (Nov 05 2020 at 12:45):

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

view this post on Zulip 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

view this post on Zulip 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