performance of large structures

Stream: lean4

[Jakob von Raumer]

Having a structure with lots of fields seems to have bad performance. Has anyone tried to tackle that issue? (/cc @Tobias Grosser @Léon Frenot )

[Tobias Grosser]

In which particular context? Do you have a lean only test case? Is there a lean pr?

[Tobias Grosser]

It would be useful to understand what the reason for this performance issue is.

[Jakob von Raumer]

HugeStructure.lean

[Tobias Grosser]

Are you saying just declaring the struct is slow?

[Tobias Grosser]

Is time to declare a struct non linear. I would find that surprising.

[Jakob von Raumer]

I haven't spent any thought on it. I wouldn't find it surprising if it was quadratic, since generally fields in structs can depend on the type of earlier fields

[Henrik Böving]

Almost all of the time is spent in [Meta.injective] [2.639434] Foo.mk ▶ according to the profiler

[Tobias Grosser]

What does this mean?

[Henrik Böving]

That lean spends almost all the time computing the injectivity theorems for the type

[Jakob von Raumer]

Ah yes.

[Henrik Böving]

Of course you could also try to merge these up into a big BitVec and just not care^^

[Jakob von Raumer]

Would prefer that over splitting up the structure :grinning_face_with_smiling_eyes:

[Tobias Grosser]

Interesting. I would check with growing examples if the asymptomatics are quadratic. If they are, there may be a faster algorithm.

[Jakob von Raumer]

Henrik Böving said:

That lean spends almost all the time computing the injectivity theorems for the type

So Foo.noConfusion itself also seems to have linear length, doesn't it?

[Tobias Grosser]

@jakob, do you already have an obvious mapping to bitvec mind.

[Jakob von Raumer]

Tobias Grosser said:

@jakob, do you already have an obvious mapping to bitvec mind.

-> other channel :grinning_face_with_smiling_eyes:

[Sebastian Ullrich]

We might want to consider generating the injectivity theorem lazily if e.g. you don't foresee needing it for your purposes, worth opening an issue

[Jakob von Raumer]

Do you think the generation is inherently quadratic?

[Sebastian Ullrich]

I'd have to take a closer look. I do see an option genInjectivity as well

[Jakob von Raumer]

That option makes it actually acceptably fast for our purposes

[Jakob von Raumer]

(But it still struggles with the above file...)

[Kyle Miller]

Can you quantify "bad performance" and "struggles"? From Henrik's comment it sounds like we're talking on the order of 5-10 seconds for a structure with over 5000 fields?

[Kyle Miller]

Ah, well I just gave it half a minute and it didn't finish elaboration, so get saying that Lean struggles with this one.

[Henrik Böving]

Kyle Miller said:

Can you quantify "bad performance" and "struggles"? From Henrik's comment it sounds like we're talking on the order of 5-10 seconds for a structure with over 5000 fields?

I cut out almost all the fields for the measurement :D