[Termtools] certified - strange proofs

[Claude Marché]

I think you are correct: Coq is given an empty file and considers it
OK. It means the runme/checkme scripts are wrong.

I must say that I spent quite a lot of time in adapting these scripts,
to make them OK. For example, in checkme I needed first to make a copy
of the given file, because it was not ending with .v. The modified
scripts are of course visible on the web by clicking on the tool name
and following the link "tool executable". The fact that ttt2 and tpa
are sharing the same back-end Rainbow/Color, and that this backend
changed significantly between the preliminary and the final version
was much trouble. But I do not think this error comes from my
modifications.

I grep'ed for the faulty answer "not a proofMAYBE" in the generated
proofs for ttt2, and found 36 such examples. 

If we follow the rules, ttt2 should be disqualified.

- Claude


>>>>> "Frederic" == Frederic Blanqui <blanqui at loria.fr> writes:

    Frederic> On Wed, 6 Jun 2007, Koprowski, A. wrote:
    >> The really bad outcome of the whole thing is that TTT2 gets points for 
    >> systems for which it essentially fails. Of course this should be avoided and 
    >> even more so in the certified competition!

    Frederic> this means that proofs have to be checked and points have to be computed by 
    Frederic> hand...
    Frederic> _______________________________________________
    Frederic> Termtools mailing list
    Frederic> Termtools at lists.lri.fr
    Frederic> http://lists.lri.fr/mailman/listinfo/termtools

-- 
Claude Marché                          | tel: +33 1 72 92 59 69           
INRIA Futurs - ProVal                  | mobile: +33 6 33 14 57 93 
Parc Orsay Université - ZAC des Vignes | fax: +33 1 74 85 42 29   
3, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |