[Termtools] certification failures

[Johannes Waldmann]

The timeouts in verification seem to be a Coccinelle problem mainly?
There are only a few of them for (Aprove+)Color.
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).

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)

Until this happens, I think it is perfectly reasonable
to re-run some verifications with larger timeout.
The committee has to define a procedure for that,
and then it needs some implementation work on the server
(select the things to re-run).

J.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 257 bytes
Desc: OpenPGP digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20081112/02a6aa2f/attachment.pgp