[Termtools] Concerning certified competition.
Claude Marché
Claude.Marche at lri.fr
Mon May 14 17:30:12 CEST 2007
>>>>> "Koprowski," == Koprowski, A <A.Koprowski at tue.nl> writes:
Koprowski,> The idea discussed during the meeting at Nancy was as follows:
Koprowski,> (1) "runme": runs the termination prover which produces a proof in some
Koprowski,> format (like XML format of CoLoR)
Koprowski,> (2) "checkme": reads that proof and translates it to a
Koprowski,> Coq/Isabelle/PVS/... script
May be I did not understand something: is there anything special in
that part (2) other than just translate XML syntax into Coq syntax? In
a previous mail, I was asking whether this part would take a
significant amount of time: I guess it would not. I am right?
Koprowski,> (3) organizers run Coq/Isabelle/PVS/... on the generated script to
Koprowski,> verify it.
>>> [Johannes]
>>> The organizer (not the "checkme") then calls the proof checker on
Koprowski,> that file.
>> [Claude]
>> I do not understand: I will not run anything by hand!
Koprowski,> The idea of (3) being done by organizers was to makes this verification
Koprowski,> explicit (and not part of a script provided by participants, which may
Koprowski,> do whatever it desires, including something silly). Of course it should
Koprowski,> be part of the script maintaining the competition and not done "by
Koprowski,> hand".
So in practice, this part should be the last line of your provided
checkme script: How the organizers could know what to do otherwise?
Koprowski,> I think ideally both the intermediate result (XML/...) and the final
Koprowski,> certificate (Coq/... script) should be available via the results page.
Koprowski,> But the latter must necessarily be accessible for credibility of the
Koprowski,> verification process.
In the rules, the checkme script is just supposed to return 0 if check
went OK, but nothing is said about its output. If there is interest, I
can manage to record its output and make it available, just like the
output of runme is, by clicking on the CPU time. Then, if you want to
see the Coq certificate, you could just write a copy to the standard
output. This can be done in a few lines of shell script.
>> [Claude]
>> Compiled before the competition: of course.
>> But what does "installing" mean? Do you need Color installed in a
Koprowski,> specific place? Why not in the same directory as the runme, > checkme,
Koprowski,> etc.
Koprowski,> I think it's ok to provide CoLoR in a bundle, together with a
Koprowski,> termination prover. It could even be precompiled, but then there are two
Koprowski,> problems:
Koprowski,> - the binaries of CoLoR are around 40MB,
Koprowski,> - we would have to make sure that it's compiled with precisely the same
Koprowski,> version of Coq as used during the competition, as otherwise the binaries
Koprowski,> may be incompatible.
No problem: just submit the sources and tell me how to compile
them. Ideally, I'd like just to run "make" if possible.
Koprowski,> The preliminary round to check that everything is fine (as for other
Koprowski,> categories) would be most welcome!
Koprowski,> Greetings,
Koprowski,> Adam
Koprowski,> --
Koprowski,> ========================================================================
Koprowski,> Adam Koprowski, (A.Koprowski at tue.nl, http://www.win.tue.nl/~akoprows)
Koprowski,> Department of Mathematics and Computer Science
Koprowski,> Eindhoven University of Technology (TU/e)
Koprowski,> The difference between impossible and possible lies in determination
Koprowski,> Tommy Lasorda
Koprowski,> ========================================================================
Koprowski,> <html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:st1="urn:schemas-microsoft-com:office:smarttags" xmlns="http://www.w3.org/TR/REC-html40">
Koprowski,> <head>
Koprowski,> <meta http-equiv=Content-Type content="text/html; charset=us-ascii">
Koprowski,> <meta name=Generator content="Microsoft Word 11 (filtered medium)">
Koprowski,> <o:SmartTagType namespaceuri="urn:schemas-microsoft-com:office:smarttags"
Koprowski,> name="City"/>
Koprowski,> <o:SmartTagType namespaceuri="urn:schemas-microsoft-com:office:smarttags"
Koprowski,> name="PlaceType"/>
Koprowski,> <o:SmartTagType namespaceuri="urn:schemas-microsoft-com:office:smarttags"
Koprowski,> name="PlaceName"/>
Koprowski,> <o:SmartTagType namespaceuri="urn:schemas-microsoft-com:office:smarttags"
Koprowski,> name="place"/>
Koprowski,> <!--[if !mso]>
Koprowski,> <style>
Koprowski,> st1\:*{behavior:url(#default#ieooui) }
Koprowski,> </style>
Koprowski,> <![endif]-->
Koprowski,> <style>
Koprowski,> <!--
Koprowski,> /* Style Definitions */
Koprowski,> p.MsoNormal, li.MsoNormal, div.MsoNormal
Koprowski,> {margin:0cm;
Koprowski,> margin-bottom:.0001pt;
Koprowski,> font-size:12.0pt;
Koprowski,> font-family:"Times New Roman";}
Koprowski,> a:link, span.MsoHyperlink
Koprowski,> {color:blue;
Koprowski,> text-decoration:underline;}
Koprowski,> a:visited, span.MsoHyperlinkFollowed
Koprowski,> {color:purple;
Koprowski,> text-decoration:underline;}
Koprowski,> p.MsoPlainText, li.MsoPlainText, div.MsoPlainText
Koprowski,> {mso-margin-top-alt:auto;
Koprowski,> margin-right:0cm;
Koprowski,> mso-margin-bottom-alt:auto;
Koprowski,> margin-left:0cm;
Koprowski,> font-size:12.0pt;
Koprowski,> font-family:"Times New Roman";}
Koprowski,> span.EmailStyle17
Koprowski,> {mso-style-type:personal-compose;
Koprowski,> font-family:Arial;
Koprowski,> color:windowtext;}
Koprowski,> @page Section1
Koprowski,> {size:595.3pt 841.9pt;
Koprowski,> margin:72.0pt 90.0pt 72.0pt 90.0pt;}
Koprowski,> div.Section1
Koprowski,> {page:Section1;}
-->
Koprowski,> </style>
Koprowski,> </head>
Koprowski,> <body lang=EN-US link=blue vlink=purple>
Koprowski,> <div class=Section1>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>>> [Johannes]<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>>> To make
Koprowski,> this intention more clear, the following is suggested<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>>> (by all
Koprowski,> participants): "checkme" should in fact be "generate":<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>>> it reads
Koprowski,> a proof and produces an input file for some established proof<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>>> checker,
Koprowski,> possibly referring to some established<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>>>
Koprowski,> libraries.<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>> [Claude]<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'>> NO. the
Koprowski,> "runme" script should generate that. It can be any format, such as
Koprowski,> the XML format expected from the Color project.<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'><o:p> </o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'>The idea discussed during
Koprowski,> the meeting at <st1:City w:st="on"><st1:place w:st="on">Nancy</st1:place></st1:City>
Koprowski,> was as follows:<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'>(1) “runme”:
Koprowski,> runs the termination prover which produces a proof in some format (like XML
Koprowski,> format of CoLoR)<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'>(2) “checkme”:
Koprowski,> reads that proof and translates it to a Coq/Isabelle/PVS/… script<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'>(3) organizers run
Koprowski,> Coq/Isabelle/PVS/… on the generated script to verify it.<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'><o:p> </o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>>> [Johannes]
Koprowski,> <o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>>> The
Koprowski,> organizer (not the "checkme") then calls the proof checker on that file.<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>> [Claude]<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'>> I do not understand: I
Koprowski,> will not run anything by hand!<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'> The idea of (3) being
Koprowski,> done by organizers was to makes this verification explicit (and not part of a
Koprowski,> script provided by participants, which may do whatever it desires, including
Koprowski,> something silly). Of course it should be part of the script maintaining the
Koprowski,> competition and not done “by hand”.<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'><o:p> </o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'> I think ideally both
Koprowski,> the intermediate result (XML/…) and the final certificate (Coq/…
Koprowski,> script) should be available via the results page. But the latter must necessarily
Koprowski,> be accessible for credibility of the verification process.</span></font><font
Koprowski,> size=2 face=Arial><span style='font-size:10.0pt;font-family:Arial'><o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
Koprowski,> font-family:Arial'><o:p> </o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>> [Claude]<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal style='text-autospace:none'><font size=2 face="Courier New"><span
Koprowski,> lang=EN-ZW style='font-size:10.0pt;font-family:"Courier New"'>> Compiled
Koprowski,> before the competition: of course.<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'>> But what does
Koprowski,> "installing" mean? Do you need Color installed in a specific place?
Koprowski,> Why not in the same directory as the runme, > checkme, etc.<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'> I think it’s ok
Koprowski,> to provide CoLoR in a bundle, together with a termination prover. It could even
Koprowski,> be precompiled, but then there are two problems:<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'>- the binaries of CoLoR are
Koprowski,> around 40MB,<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'>- we would have to make sure
Koprowski,> that it’s compiled with precisely the same version of Coq as used during
Koprowski,> the competition, as otherwise the binaries may be incompatible. <o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'> The preliminary round
Koprowski,> to check that everything is fine (as for other categories) would be most
Koprowski,> welcome!<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'><o:p> </o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'> Greetings,<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face="Courier New"><span lang=EN-ZW
Koprowski,> style='font-size:10.0pt;font-family:"Courier New"'> Adam<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoNormal><font size=2 face=Arial><span style='font-size:10.0pt;
Koprowski,> font-family:Arial'><o:p> </o:p></span></font></p>
Koprowski,> <p class=MsoPlainText style='margin:0cm;margin-bottom:.0001pt'><font size=2
Koprowski,> color=black face="Courier New"><span lang=PL style='font-size:10.0pt;
Koprowski,> font-family:"Courier New";color:black'>--<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoPlainText style='margin:0cm;margin-bottom:.0001pt'><font size=2
Koprowski,> color=black face="Courier New"><span lang=PL style='font-size:10.0pt;
Koprowski,> font-family:"Courier New";color:black'>========================================================================<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoPlainText style='margin:0cm;margin-bottom:.0001pt'><font size=2
Koprowski,> color=black face="Courier New"><span lang=PL style='font-size:10.0pt;
Koprowski,> font-family:"Courier New";color:black'> Adam Koprowski, (<a
Koprowski,> href="mailto:A.Koprowski at tue.nl">A.Koprowski at tue.nl</a>, <a
Koprowski,> href="http://www.win.tue.nl/~akoprows">http://www.win.tue.nl/~akoprows</a>)<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoPlainText style='margin:0cm;margin-bottom:.0001pt'><font size=2
Koprowski,> color=black face="Courier New"><span lang=PL style='font-size:10.0pt;
Koprowski,> font-family:"Courier New";color:black'> </span></font><font size=2
Koprowski,> color=black face="Courier New"><span style='font-size:10.0pt;font-family:"Courier New";
Koprowski,> color:black'>Department of Mathematics and Computer Science<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoPlainText style='margin:0cm;margin-bottom:.0001pt'><font size=2
Koprowski,> color=black face="Courier New"><span style='font-size:10.0pt;font-family:"Courier New";
Koprowski,> color:black'> <st1:place w:st="on"><st1:PlaceName w:st="on"><u1:place u2:st="on"><u1:PlaceName u2:st="on">Eindhoven</st1:PlaceName></u1:PlaceName>
Koprowski,> <st1:PlaceType w:st="on"><u1:PlaceType u2:st="on">University</st1:PlaceType></st1:place></u1:PlaceType></u1:place>
Koprowski,> of Technology (TU/e)<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoPlainText style='margin:0cm;margin-bottom:.0001pt'><font size=2
Koprowski,> color=black face="Courier New"><span style='font-size:10.0pt;font-family:"Courier New";
Koprowski,> color:black'> The difference between impossible and possible lies in
Koprowski,> determination<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoPlainText style='margin:0cm;margin-bottom:.0001pt'><font size=2
Koprowski,> color=black face="Courier New"><span style='font-size:10.0pt;font-family:"Courier New";
Koprowski,> color:black'> </span></font><font size=2
Koprowski,> color=black face="Courier New"><span lang=PL style='font-size:10.0pt;
Koprowski,> font-family:"Courier New";color:black'>Tommy Lasorda <o:p></o:p></span></font></p>
Koprowski,> <p class=MsoPlainText style='margin:0cm;margin-bottom:.0001pt'><font size=2
Koprowski,> color=black face="Courier New"><span lang=PL style='font-size:10.0pt;
Koprowski,> font-family:"Courier New";color:black'>========================================================================<o:p></o:p></span></font></p>
Koprowski,> <p class=MsoPlainText style='margin:0cm;margin-bottom:.0001pt'><font size=3
Koprowski,> face="Times New Roman"><span style='font-size:12.0pt'> </span><o:p></o:p></font></p>
Koprowski,> </div>
Koprowski,> </body>
Koprowski,> </html>
Koprowski,> _______________________________________________
Koprowski,> Termtools mailing list
Koprowski,> Termtools at lists.lri.fr
Koprowski,> 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 |
More information about the Termtools
mailing list