presheafed space category

Stream: maths

[Patrick Massot]

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

[Johan Commelin]

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

[Patrick Massot]

Maybe we could help it a bit

[Patrick Massot]

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

[Patrick Massot]

and that's on my fast computer

[Patrick Massot]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Johan Commelin]

You can definitely look at what tidy produces.

[Patrick Massot]

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

[Patrick Massot]

Lean is using 1500% CPU

[Kevin Buzzard]

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]

tidy is Scott's magic

[Patrick Massot]

but it's extremely slow

[Kevin Buzzard]

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

Shouldn't this say by structure_helper? ;-)

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Patrick Massot]

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