[Termtools] certification failures

[Frederic Blanqui]

Johannes Waldmann a écrit :
> The timeouts in verification seem to be a Coccinelle problem mainly?
 > There are only a few of them for (Aprove+)Color.

Well, it does not seem so. Currently, Aprove-color has 364 timeouts and 
cime3 only 239.

> Of course there are some problems where only Cime finds a proof,
> and then verification times out.
> 
> The motivation for having short time for verification was
> that this could be an incentive for library developers
> to develop "efficient" proof (methods).

I agree with that. In theory, verification should even take less time 
than proof search!

> The counter-argument was what you just gave and that verification
> cannot easily make use of the multi-core architecture
> (as opposed to proof search).
> 
> Is there a parallel coqc any time soon? (Theoretically,
> could split the *.v into several files and do separate compilation -
> if module dependencies allow this. Well, if this were possible,
> I'm sure the Coq people would already be working on it)

No. But this can be done as follows. Put the proof of the correctness of 
every proof node in a separate coq file. Then use "make -j" to compile 
the whole proof. But to do this, one needs to know the statements 
corresponding to every proof node. This is another reason for including 
this in the proof format...