[Termtools] versions of coq used in competition

[Julien Forest]

Dear all, 


On Mon, 27 Oct 2008 19:58:44 +0100
Johannes Waldmann <waldmann at imn.htwk-leipzig.de> wrote:

> 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).
> 
Not exactly, 
the only distributed version of coccinelle which can feature matrix
interpretation is the one corresponding to the coq trunk branch. 
On the other hand, this is not a problem to distribute a coccinelle tar
file for coq-8.2beta4 during the week (in fact I only need time to copy
a file and recheck my benches) 

> 
> 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.
> 
In my opinion, the competition should run under a relatively stable
version of Coq. 
Being a coq developer, I must mention that the official coq-8.1 version
is now too old to be fully usable by us and probably by Color. The next
release to appear will be the coq-8.2 which should be very close to
it's actual beta4 version so that for me we should run under the beta4
version of coq-8.2. 

> 
> 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).
> 
As mentioned before, we do not need such a breaking rule.

Best regards, 
Julien Forest