The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

Maybe this is due to the universe algorithm. Have you tried my patch
(included in trunk but not in 8.5 currently) ?

-- 
JH

Le 25/01/2016 14:00, Guillaume Melquiond a écrit :
> 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

Attachment: signature.asc
Description: OpenPGP digital signature