Coq-HoTT
Coq-HoTT copied to clipboard
HoTT
Reduce universes for performance
It seems likely that a lot of the slowness of V.v is due to its insane number of universe parameters (e.g. V.function has over 2000). We should experiment with adding more universe annotations to reduce this number and see how it affects performance.
No, I don't think we do. Last I checked, V.v was still using around thousands, if not tens of thousands, of universe variables in a single definition.
Just as a remark, I'm experimenting with more agressive minimization to try to lower these numbers, I'll keep you updated. In my experience one thing that can be tried otherwise is to see if you have basic definitions creating many universes for the same l.u.b. and explicitly share them.
I've went back on this. The problem is caused by using Let's in sections. Each Let introduces universes that are rigid so when they unifiy with each other you get two universes plus an equality between them instead of a single universe without additional constraints. Most of the 20000's come from this. This is really a design issue with sections, which would be resolved by "lambda-lifting" section constants immediately and just providing an appropriate shortcut to their instantiated versions while working with them in the section. This would avoid having to do any work at section closing time as well. I'm planning to write a CEP about this, and hopefully have it done by Coq 8.7/9. In the meantime, I suggest avoiding Let's here and using definitions instead.
I only see five Lets in V.v, and replacing them with Definition doesn't seem to appreciably change the number of universes or the speed of compiling that file.
@spitters nope, I've had no time to look into it. We should discuss this with @SkySkimmer and @ppedrot, maybe they have different ideas on how to tame this problem.
Maybe @ppedrot 's pseudo-monomorphic universe instantiation would work for this? Not sure to what extent V uses univ polymorphism.
I don't think it'd affect let-bindings in a section, but it may help otherwise. I still have the branch somewhere if you want to try to play with it.
There is a quite outdated version there. The option name is Universe Polymorphism Monomorphism Emulation (yes, I know) and once activated, every time a constant is given without a specified universe instance, there will be a unique one generated for the whole proof that will be reused next time the constant appears.
I am going to rebase the branch anyways.
for the whole proof
A version scoped to the section is what I was thinking of