[Why3-club] Generating Coq with Why3 into separate files

Julien Thierry thierry at adacore.com
Tue Mar 18 18:06:37 CET 2014


 

Dear Stefan,

Thank you for the answers.

On 2014-03-13 14:43, Stefan
Berghofer wrote:
> Would writing a Coq plugin using a similar approach be an
option for you
> as well? While this
> plugin was relatively straightforward
to write for Isabelle, it may be
> more complicated for
> Coq, since the Coq
driver contains some extra quirks such as proofs that
> all Why3 types are
>
inhabited.

I fear that might be a bit too complex since I don't have much
experience with Coq.

> I doubt that the Why3 infrastructure for writing
drivers for external
> provers currently supports
> the generation of more
than one file for a particular task. The outputs
> of the fprintf commands
in
> the printers all end up in the same file, and also the Why3 session
>
description file why3session.xml
> only seems to be able to keep track of
one file for each goal and prover.
> To circumvent this problem,
> I
provided an additional wrapper script that is called by Why3 with the
> name
of a generated *.xml
> file as an argument, and then calls Isabelle with the
corresponding *.thy
> file. If the *.thy file
> does not yet exist, the
wrapper script generates a stub *.thy file
> containing the names of the
proof
> obligations extracted from the *.xml file. Unfortunately, there are
still
> some issues with this
> approach. Why3 is only aware of the
existence of the *.xml files but not
> of the *.thy files. As
> a
consequence, Why3 issues an error message when the *.xml files are not
>
present, even though they
> could be generated and the only important files
for replaying the proof
> are the *.thy files. This
> is why the *.xml files
for the examples involving Isabelle are currently
> part of the Why3
repository
> as well, see e.g.

About this method, I understood that your
files' names are related to the VCs' name.
I was wondering: How is handled
the case of renaming a VC?
Is a new editable .thy file created forgetting
about the previous file possibly containing a proof?
Or do you have a way to
more or less "sync" the old files with the new VCs when code is
regenerated?

Regards,

-- 
Julien Thierry

 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20140318/b9deb0b2/attachment.html>


More information about the Why3-club mailing list