[Termtools] termination competition interface

[Johannes Waldmann]

Thanks Simon,


I managed to upload some versions of Matchbox
and I did see the results of test runs (for SRS and TRS standard, so far).
I encourage the others to test-upload their provers as well.

It seems that the test inputs are randomly selected from the data base.
that's fine for now, but an extension for user-selected would be nice to 
have.

I noticed that for each prover, there is exactly one category
(if I want SRS and TRS, I need to submit two "tool implementations")?


What is the specification for the "certified" category
(as it is implemented currently)? Something with "runme" and "checkme"?
Or could someone who took part in this category last year
repeat them for us? The FAQ would be "I have a prover
that reads  "foo.?rs" and produces  "foo.rainbow",
how does this fit into the execution environment?"


What about SRS-certified? I'd love to have that.


I would appreciate if we could use versions of
Coq, Color, Rainbow installed on the server.
It should be possible to distinguish "last year"
from "current" (coq-8.2beta4, color and rainbow from CVS)
by different names/directories? I don't think this is even necessary.
According to my tests, current rainbow is backward compatible.


Also, could you please install these constraint solvers
* minisat http://minisat.se/downloads/minisat2-070721.zip
* boolector http://fmv.jku.at/boolector/ (0.5)

I think it's the wrong idea to require termination prover authors
to package such constraint solvers with their provers.
In some cases this may even be legally questionable:
The termination-prover.zip submission will be available
from the competition web site, and this constitutes
a re-distribution of all the binaries that are contained in them.
We are on the safe side if the auxiliary binaries are not there,
and the user of the termination prover is required to
(accept the license and) install the underlying constraint solver on 
their own.


Best regards, and thanks for doing all the work! - 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/60ffa20e/attachment.pgp