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

Julien Thierry thierry at adacore.com
Fri Mar 21 11:29:08 CET 2014


On 2014-03-19 13:43, Stefan Berghofer wrote:
> 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.

Thanks a lot, I think you provided me all the information I needed.


Julien Thierry

More information about the Why3-club mailing list