The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 25/01/2016 13:49, Frédéric Blanqui wrote:
> Hi!
> 
> To give you finer statistics (COQC=./time_coqc make && ./stat_time in
> CoLoR):
> 
> files: 265, time: 2037s, mean: 7.69s
> max: 124.71s (./Coccinelle/term_orderings/rpo.v)
> files>10s: 49 (18%), time: 1327s (65%)
> 
> There are 265 files. The average time is 7.69s/file. 49 files (18%) take
> more than 10s each and 65% of the total time.
> 
> The record is Coccinelle/term_orderings/rpo.v (not actually part of
> CoLoR but included in it for some reasons [the coq-color opam package
> does not include it though]) with 124.71s! (It has 312136 characters and
> 8259 lines.)
> 
> The 10 first files are:
> 
> ./Coccinelle/term_orderings/rpo.v     124,71
> ./Term/Lambda/LAlpha.v        111,53
> ./Term/Lambda/LCompClos.v     92,29
> ./Term/Lambda/LSubs.v         77,31
> ./Util/FGraph/FGraph.v        68,79
> ./Term/Lambda/LCompRewrite.v  58,2
> ./Term/Lambda/LComp.v         46,56
> ./Util/FGraph/TransClos.v     45,47
> ./Term/Lambda/LAlphaAlt.v     44,52
> ./Term/SimpleType/TermsConv.v         29,64
> 
> 
> With Coq 8.4pl6, the results are:
> 
> mean: 6.90s
> max: 79.49s (./Coccinelle/term_orderings/rpo.v)
> files>10s: 44 (16%), time: 980s (53%)
> 
> ./Coccinelle/term_orderings/rpo.v     79,49
> ./Term/Lambda/LAlpha.v        62,11
> ./Term/Lambda/LSubs.v         58,5
> ./Term/Lambda/LCompClos.v     57,33
> ./Term/SimpleType/TermsBeta.v         45,75
> ./Util/FGraph/TransClos.v     37,3
> ./Term/Lambda/LAlphaAlt.v     36,96
> ./Term/Lambda/LCompRewrite.v  34,74
> ./Util/FGraph/FGraph.v        29,83
> ./Term/Lambda/LComp.v         29,19
> 
> 
> So, on some files, the compilation time is multiplied by 2 almost... :-(

Look at the bright side of it ;-). Since the overall time is only 60
seconds larger, it also means that we are also doing incredibly better
on many files. For instance, according to your numbers, TermsBeta is
compiled at least 50% faster (if not more).

That said, it would be interesting to know what makes rpo.v, LAlpha.v,
and so on, so much slower to compile.

Best regards,

Guillaume