The Coq mailing list

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

Hello Enrico.

I was just trying to use your new compilation procedure but I get 
errors. But I am not sure how to proceed. It's perhaps better to discuss 
this offline first.

time make -j20 quick:

Error: The value you are asking for (matching_complete) is not available in
this process. If you really need this, pass the "-async-proofs off" 
option to
CoqIDE to disable asynchronous script processing and don't pass "-quick" to
coqc.
make[1]: *** [Conversion/Coccinelle.vio] Erreur 1
make[1]: *** Attente des tâches non terminées....
make[1]: quittant le répertoire « /local/blanqui/src/color-svn-8.5 »
make: *** [quick] Erreur 2

real    3m2.226s
user    20m31.229s
sys    1m50.994s

Note that I do not use CoqIDE. It's batch compilation.

Frédéric.


Le 25/01/2016 11:15, Enrico Tassi a écrit :
> On Mon, Jan 25, 2016 at 11:08:33AM +0100, Frédéric Blanqui wrote:
> > j  |
> > --------------------
> > 1  | 27'00"
> > 3  | 10'47"
> > 20|   6'45"
> >
> > So, you can see that it is really important for me to use -j20...
> Can you try with a -j6 when you have a minute?
>
> Also, given that you mentioned it, do you have timings for
> "make quick -j20" and "make vio2vo J=20" ?
>
> Best,