## Stream: maths

### Topic: presheafed space category

#### 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?

#### Johan Commelin (Jul 08 2019 at 12:09):

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

#### Patrick Massot (Jul 08 2019 at 12:10):

Maybe we could help it a bit

#### 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

#### Patrick Massot (Jul 08 2019 at 12:11):

and that's on my fast computer

#### 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

#### 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?

#### 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

#### 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?

#### Patrick Massot (Jul 08 2019 at 12:13):

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

#### Johan Commelin (Jul 08 2019 at 12:13):

You can definitely look at what tidy produces.

#### Patrick Massot (Jul 08 2019 at 12:13):

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

#### Patrick Massot (Jul 08 2019 at 12:13):

Lean is using 1500% CPU

#### 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

#### Patrick Massot (Jul 08 2019 at 12:14):

tidy is Scott's magic

#### Patrick Massot (Jul 08 2019 at 12:14):

but it's extremely slow

#### 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? ;-)

#### 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.

#### 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.)

#### 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).

#### Scott Morrison (Jul 28 2019 at 02:52):

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

#### 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