[Termtools] Upcoming competition - discussion during Nancy Workshop

[Claude Marché]

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

    Johannes> This input file shall be made visible on the competition web site.
    >> YES

    Frederic> i think that this is the final coq proof that should be published, not the 
    Frederic> intermediate xml proof. otherwise, we won't be able to compare the acutal 
    Frederic> proofs generated by say cime and tpa-rainbow-color. hence, the interest of the 
    Frederic> proposition: checkme generates a coq proof and the organizers run coqc on it.

So: if you want to see the generated Coq script instead of the
intermediate XML format, please include the XML to Coq translator into the
runme script. Would it take much CPU time? I guess not. I guess Coq
compilation is the bottleneck.

Please recall that the rules must be independant of the checking
method. Other participants might want to use Isabelle, PVS... So
every participants choose the proof language they want.

    Johannes> The organizer (not the "checkme") then calls  the proof checker on that
    Johannes> file.

I do not understand: I will not run anything by hand!

    >> On the other hand, I don't want to take care of other unstable
    >> versions of Coq or Coq libraries. In particular, participants willing
    >> to use Coq as proof checking tool should provide all needed librairies.

    Frederic> we need the color library to be installed somewhere and compiled before the 
    Frederic> beginning of the competition. why not installing color yourself? this is no 
    Frederic> more difficult than coq.

Compiled before the competition: of course.
But what does "installing" mean? Do you need Color installed in a
specific place? Why not in the same directory as the runme, checkme,
etc. 

Please also take into account that everything needed to run your tools
will be made available on the Web site. For that purpose, I prefer
that the precise needed version of the Color library should be given. 


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