search

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq
https://metacoq.github.io
MIT License
367 stars 79 forks source link

faster PCUICSR #1081

Closed mrhaandi closed 2 months ago

mrhaandi commented 3 months ago

Replaced slow firstorder calls by appropriate constructor, left, right calls. This improves performance from 5m49.68s | 2644580 ko | PCUICSR.vo to 0m49.37s | 1443968 ko | PCUICSR.vo, also improving overall project compilation speed.

TheoWinterhalter commented 3 months ago

I'm amazed that it's only two occurrences that take up that long!

ppedrot commented 3 months ago

FTR I have had firstorder on my radar for a while. It's very inefficient because it strongly normalizes all terms from the context. (It's a bit sad that these instances will disappear for benching purposes, btw.)

TheoWinterhalter commented 3 months ago

Would that be reason enough to keep them though? Could we keep them as a special CI that only runs for benchmarks?

mattam82 commented 2 months ago

It does not seem reasonable to me to not fix it so that the firstorder issue stays in the CI. @ppedrot It should be easy to make a specific test-case for that no?

mattam82 commented 2 months ago

Thanks @mrhaandi !

ppedrot commented 2 months ago

Note that coq/coq#19126 has probably made this PR much less usefull in practice.