Zulip Chat Archive

Stream: maths

Topic: presheafed space category


view this post on Zulip Patrick Massot (Jul 08 2019 at 12:08):

@Scott Morrison Is there anything we could do to make that line 64 to consume less than half of mathlib compile time?

view this post on Zulip Johan Commelin (Jul 08 2019 at 12:09):

I guess tidy might be spending some time on the category axioms...

view this post on Zulip Patrick Massot (Jul 08 2019 at 12:10):

Maybe we could help it a bit

view this post on Zulip Patrick Massot (Jul 08 2019 at 12:11):

I'm compiling mathlib a lot, and I keep staring at src/algebraic_geometry/presheafed_space.lean: parsing at line 64

view this post on Zulip Patrick Massot (Jul 08 2019 at 12:11):

and that's on my fast computer

view this post on Zulip Patrick Massot (Jul 08 2019 at 12:12):

What I really don't understand is that I see that multiple times during a single leanpkg build run

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 12:12):

Is there some sort of tidy magic or similar clever tactic going on in that line? Is this a situation where you can look at the proof generated by the magic and just cut and paste it in?

view this post on Zulip Patrick Massot (Jul 08 2019 at 12:12):

It spend some time on that line, then compiles other stuff and comes back to that line

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 12:13):

Are you sure it's just not doing that with one core and doing other things with other cores?

view this post on Zulip Patrick Massot (Jul 08 2019 at 12:13):

Yes, it's probably tidy, so it has a hole command version we could copy-paste

view this post on Zulip Johan Commelin (Jul 08 2019 at 12:13):

You can definitely look at what tidy produces.

view this post on Zulip Patrick Massot (Jul 08 2019 at 12:13):

I don't know how the leanpkg build output interacts with the multiple core thing

view this post on Zulip Patrick Massot (Jul 08 2019 at 12:13):

Lean is using 1500% CPU

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 12:13):

I don't know if tidy has anything to do with it. It's just one of these miraculous proofs which Scott is extremely good at pulling off using his magic

view this post on Zulip Patrick Massot (Jul 08 2019 at 12:14):

tidy is Scott's magic

view this post on Zulip Patrick Massot (Jul 08 2019 at 12:14):

but it's extremely slow

view this post on Zulip Kevin Buzzard (Jul 08 2019 at 12:18):

instance category_of_PresheafedSpaces : category (PresheafedSpace.{v} C) :=
{ hom  := hom,
  id   := id,
  comp := comp }
end

Shouldn't this say by structure_helper? ;-)

view this post on Zulip Scott Morrison (Jul 11 2019 at 05:19):

Sorry about this. I am travelling/on holiday for another 10 days, but will try to get to this then.

view this post on Zulip Scott Morrison (Jul 11 2019 at 05:20):

I'm dubious about using by structure_helper for defining data! (Notice this construction contains no proofs, because they've been tidy'd away.)

view this post on Zulip Keeley Hoek (Jul 11 2019 at 07:07):

Indeed, if we are worried about such definitions being slow, by structure_helper would make that definition strictly slower (though perhaps only by microseconds).

view this post on Zulip Scott Morrison (Jul 28 2019 at 02:52):

@Patrick Massot, sorry, I finally got around to fixing this, it's in #1273 now.

view this post on Zulip Patrick Massot (Jul 28 2019 at 10:56):

Nice! Of course I really hope all this problem will disappear at some point because tactics will either become fast or properly cached.


Last updated: May 10 2021 at 07:15 UTC