The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

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... :-(

Best regards,

Frédéric.

PS. Places where Coq is slow are marked with (*SLOW*) in the code.

Le 25/01/2016 13:00, Guillaume Melquiond a écrit :

On 25/01/2016 11:37, Frédéric Blanqui wrote:

Hi Guillaume.

With /usr/bin/time make -j20, I get:

2017.92user 108.62system 8:14.59elapsed 429%CPU (0avgtext+0avgdata
1850172maxresident)k
0inputs+607752outputs (0major+12904377minor)pagefaults 0swaps

I don't know how to interpret all this. Does this answer your questions?

Yes and no. At the very least, it tells us that memory is not an issue,
since you never had any major pagefault. But it does not tell us why the
whole compilation process got much slower while Coq itself did not. The
number of outputs seems quite large, but without a comparison point, it
is hard to tell.

6:
real    9m33.979s
user    28m0.672s
sys    1m17.952s

20:
real    8m12.333s
user    32m43.505s
sys    1m43.168s

Notice how the system is somehow getting swamped. You seem to have gone
past the point where increasing the number of concurrent processes
actually makes the system slower, since the "user" and "system" times
are getting much higher than needed. But I have no idea what part of the
operating system is causing a bottleneck.

Best regards,

Guillaume