[Termtools] termination competition interface

[Simon Bailey]

hi johannes,

On Oct 13, 2008, at 10:58 AM, Johannes Waldmann wrote:
> 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.

ok, i'll put it on the wish-list.

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

please elaborate? 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).

[see "Entering the competition" on this page: http://colo5-c703.uibk.ac.at:8080/termcomp/help/tool.seam 
  or this image: http://colo5-c703.uibk.ac.at:8080/termcomp/img/help/edit-tool.png 
  ]

> 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?"

in the certified category, the tool provides a coq input file on  
stdout (as in claude's implemenation) and this output is passed (by  
the competition environment) to coqc as a .v file.

see the methods runCommand() and certifyResult() in this file: http://dev.aspsimon.org/websvn/filedetails.php?repname=termcompLocal&path=%2Ftrunk%2Fsrc%2Forg%2Faspsimon%2Ftermcomp%2Fremote%2FCompetitionJobExecutor.java

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

this involves adding a category with the selection of SRS problems and  
marking it as a certified category --> simple job.

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

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

rainbow and color from cvs could be installed in /usr/local/share/ 
{color,rainbow}-cvs/ and leaving the standard "release" versions in / 
usr/local/share/{color,rainbow}/ – this shouldn't present a problem.  
except for the annoying bug in rainbow's tpdb2xml (i think) which  
writes a file /tmp/pb.xml and does not delete it; this causes absolute  
insanity on multi-user machines.

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

either today or tomorrow.

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


ack.

regards,
sb

--
Simon Bailey
Systems Administrator
Institut fuer Informatik
Universitaet Innsbruck
Technikerstrasse 21a/2
A-6020 Innsbruck
Tel: +43 (0) 512 507 - 6433
Mob: +43 (0) 664 812 5267
Fax: +43 (0) 512 507 - 2887
http://informatik.uibk.ac.at/