Zulip Chat Archive

Stream: maths

Topic: speeding up category theory


view this post on Zulip Kevin Buzzard (Dec 07 2019 at 09:49):

Every now and then I attempt to engage with the category theory library and I always manage get a bit further in than the time before. And then I usually run into something which frustrates me (e.g. I get muddled about universes) and moan here for a bit and then go and do something else.

So @Calle Sönne raised the question of proving that the equalizers of (f,g) and (g,f) are isomorphic. If I write down the map like this:

import category_theory.limits.shapes.equalizers

open category_theory
open category_theory.limits

universes v u

variables {C : Type u} [𝒞 : category.{v} C] [has_equalizers.{v} C]
include 𝒞

variables (A B : C) (f g : A  B)

set_option profiler true
def equalizer.symm.hom : equalizer g f  equalizer f g :=
equalizer.lift _ _ (equalizer.ι g f) (by tidy)
-- elaboration of equalizer.symm.hom took 794ms

then things are already slow. I changed tidy to simp and it's still slow. My impression is that in Isabelle you replace by tidy with sledgehammer and then look at the output and use that in your code instead. Is there a way of doing this here?
Isn't there some way of getting tidy to report tidy says...? I know I can put simp logging on but if I could just get something to cut and paste that would be great.

view this post on Zulip Patrick Massot (Dec 07 2019 at 09:50):

https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md#tidy

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 09:52):

boggle why do I have to look at this web page? I even read the Lean source for tidy. Shouldn't this be mentioned in the docstring?

view this post on Zulip Patrick Massot (Dec 07 2019 at 09:52):

Documentation can always be improved, but that one was not so hard to find...

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 09:52):

If I hover over tidy I get tidy ?? tactic.tidy.cfg?

view this post on Zulip Patrick Massot (Dec 07 2019 at 09:53):

But you can PR a better docstring of course.

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 09:55):

Documentation can always be improved, but that one was not so hard to find...

It's not so hard to find if you remember all the places where you're supposed to be looking to find this information. I tried the docstring, I tried the source code for the file hoping for a module docstring, I tried searching Zulip for tidy says, I then asked here.

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 09:58):

I can't write this docstring. "Tidy does something. Try tidy? to see what it did."

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 09:59):

oh wait, I can -- I can just copy from the tactic md file ;-)

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 10:29):

Is it [ci skip] or [skip ci] in the commit message? Both have been used recently. Do both work?

view this post on Zulip Kevin Buzzard (Dec 07 2019 at 10:32):

#1788

view this post on Zulip Patrick Massot (Dec 07 2019 at 11:37):

I think both [ci skip] and [skip ci] work, although the first one is the legit one.


Last updated: May 14 2021 at 18:28 UTC