[Termtools] Upcoming competition - discussion during Nancy Workshop

[Frederic Blanqui]

On Mon, 14 May 2007, Claude Marché wrote:

>    Johannes> To make this intention more clear, the following is suggested
>    Johannes> (by all participants): "checkme" should in fact be "generate":
>    Johannes> it reads a proof and produces an input file for some established proof
>    Johannes> checker, possibly referring to some established
>    Johannes> libraries.
>
> NO. the "runme" script should generate that. It can be any format,
> such as the XML format expected from the Color project.
>
>    Johannes> This input file shall be made visible on the competition web site.
> YES

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

>    Johannes> The organizer (not the "checkme") then calls  the proof checker on that
>    Johannes> file.
>
> NO. The "checkme" is called automatically with the generated file as
> argument. It can do several steps of verification, such as
>  1) generate a Coq script from the XML file
>  2) run coqc on the generated file
>  3) checks coqc return status, and return 0 if everything went OK (as
>     said in the rules document)
>
> The important points are:
> 1) the process in the checkme file must be explained in a short text (as
>   said in the rules document) so that the organizers may be
>   more or less convinced that the certification procedure is safe.
> 2) it should also be explain how the format of the file generated by
>   "runme" is related to the input problem, so that organizers can be
>   convinced that the checking procedure is run on the right problem
>
>    Johannes> (For this year, we expect that all participants use Coq
>    Johannes> and CoLoR.
>
> Wrong. Cime/A3PAT will use Coq but not Color.
>
>    Johannes> Technical detail: this would rely on  Coq and Color installed by Claude,
>    Johannes> and agreement on Coq command line arguments, if any - it should be possible
>    Johannes> to specifiy everything within the Coq input.)
>
> About Coq: as I did for Java, I can manage to install a standard Coq
> version, such as the current one 8.1

ok for coq 8.1

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

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