[Why3-club] Generation of realizations broken

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Fri Nov 22 18:25:51 CET 2013


Dear Stefan,

Thanks for the heads-up. Andrei and I just fixed it in
commit 5e51326c70a2b5cd4af2ba4e2d5744c63c716a27

You would have to apply a similar patch to your Isabelle printer, most
likely.

Best regards,
--
Jean-Christophe



On 22/11/2013 16:48, Stefan Berghofer wrote:
> Dear Why3-Club,
> 
> it seems that generation of realizations is currently broken in the
> development version
> of Why3. It still worked in revision
> c76541ab4eba53dfd7bce74617e5ef22796c300f.
> If you try out something like
> 
>   WHY3CONFIG="" bin/why3.opt --realize -L theories -D
> drivers/coq-realize.drv -T list.Append -o foo
> 
> in the base directory with this revision, you'll get a file foo/Append.v
> containing a
> number of proof obligations. Note that I've chosen foo as an output
> directory to avoid
> overwriting existing realizations.
> If you try the same with revision
> a8ab6cc184e18467fc04b3ec4a05c793eb88c519 directly after
> the merge with branch 'no_t_vars', you'll get a file with no proof
> obligations at all, just
> with a list of "Require" commands.
> This problem also affects the printer for Isabelle that I'm currently
> developing.
> 
> Can you confirm this, or is it just me?
> 
> Greetings,
> Stefan
> 
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club



More information about the Why3-club mailing list