metacoq icon indicating copy to clipboard operation
metacoq copied to clipboard

Published 20 hours ago • verified publisher icon MetaCoq

faster PCUICSR

Open mrhaandi opened this issue 9 months ago • 3 comments

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.

mrhaandi avatar May 08 '24 13:05 mrhaandi

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

TheoWinterhalter avatar May 09 '24 01:05 TheoWinterhalter

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

ppedrot avatar May 09 '24 09:05 ppedrot

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

TheoWinterhalter avatar May 09 '24 12:05 TheoWinterhalter

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 avatar Jun 12 '24 12:06 mattam82

Thanks @mrhaandi !

mattam82 avatar Jun 12 '24 12:06 mattam82

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

ppedrot avatar Jun 13 '24 08:06 ppedrot