[Termtools] termination competition interface

[Frederic Blanqui]

Johannes Waldmann a écrit :

>> i don't think that using a beta version of a certification tool is a
>> good idea. beta implies bugs and bugs are not good... ;)
> 
> If color/rainbow were buggy, it would be detected by coq,
> unless coq has a bug. we'd have to trust the coq development process.
> From reading the mailing lists it seems 8.2beta4
> is a release candidate for 8.2 proper.
> 
> The motivation is that 8.2 is needed for the new rainbow/color
> that have new features (1. handles SRS, including "reverse" transform;
> 2. SCC decomposition). SRS-certified would depend on (1) (?).
> 
> What do the others think?  Using these new features might seem unfair
> to those who didn't follow the latest developments closely,
> and have no time to make use of them for their November submissions.
> 
> Formally, the question is: do we count verification by coq-8.2beta4
> as a successful verification?
> 
> We don't have to discuss what versions of color/rainbow are "allowed"
> since the current specs do not constrain the way
> the *.v file is produced. (This is independent from the discussion
> of what versions will be provided on the server.)

I fully agree with Johannes. What version of Coq/CoLoR/Rainbow can be 
used by a tool should not be restrained.