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

Stefan Berghofer berghofe at in.tum.de
Wed Mar 19 13:43:05 CET 2014


On 03/18/2014 06:06 PM, Julien Thierry wrote:
> 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?

Dear Julien,

like the Coq printer, the Isabelle printer does not contain any specific code for inventing file names.
A printer has no influence on the name of the output file and does not even know it, because it is generated
by the infrastructure calling the printer. In order to handle changes in VCs, Why3 implements a heuristics
for finding out whether or not a newly generated VC is similar to a VC that has already been proved. If
Why3 finds out that a new VC is similar to an old VC, then the name of the generated file (and hence also
the .thy file) is reused, otherwise a file with a new name is generated. The details of this heuristics
are described in

   http://hal.inria.fr/hal-00875395
   http://www.lri.fr/~filliatr/pub/saarbrucken-5-march-2013.pdf

I am sure the authors of this paper can give you additional information if necessary.

Greetings,
Stefan



More information about the Why3-club mailing list