[Termtools] versions of coq used in competition

[Johannes Waldmann]

Dear all,


the Aprove team alerts us to the following problem:

only the most recent version of coccinelle
features matrix interpretations.

but this version does not compile with coq-8.2beta4,
instead it needs a more recent coq version
(a checkout from the development tree).


We had the goal that all the experiments that take place during
competition must be independently verifiable.

the reasons being that (1) otherwise it's not science,
and (2) the users of termination tools
want to be able to install all the necessary software
via downloads from  the competition website,
and stable external archival repositories.

The question is whether using some svn trunk version of coq
is acceptable.


One might argue that this goal of using only stable tools
is already broken by allowing rainbow/color from CVS and coq-8.2beta4,
at the request of matchbox. This is delicate since matchbox
is chairing the competition.


So I'm inclined to agree with  using a coq version
that can compile current versions of both coccinelle and color
(I am checking with coq-8.2-11512 now).

I would oppose the use of different coq versions for verifying outputs
of different provers. (To verify a certificate is the task of the
execution platform, and is not at the discretion of the competitor.)

In any case it should be made very clear on the competition results
web site what versions of tools/libraries had been used.


Best regards, Johannes.




-------------- 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/20081027/a09bc43b/attachment.pgp