[Why3-club] Generation of realizations broken

Stefan Berghofer berghofe at in.tum.de
Fri Nov 22 16:48:47 CET 2013


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



More information about the Why3-club mailing list