[Termtools] termination competition interface

[Johannes Waldmann]

> you can select multiple categories in the category list when you're in
> the tool editor (on a pc use control+click, on a mac command+click).

Ah! that's what I was looking for. Thanks for reminding me.


> 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.)


> /usr/local/share/{color,rainbow}-cvs/ 

Fine. Instead of -cvs, please put -$(date -I) there.


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/20081013/df5edeaa/attachment.pgp