[Why3-club] Problem with the hypothesis_selection plugin

Piotr Trojanek piotr.trojanek at gmail.com
Tue Nov 12 13:22:33 CET 2013


I have forgot to attach the patch :(

PS With hypothesis_selection enabled my goals are indeed proved.

-- Piotr

On Tue, Nov 12, 2013 at 12:15:20PM +0000, Piotr Trojanek wrote:
> Hi, fortunately I did not gave up. The "solution" is to add description
> when registering the transformation (see the attached patch).
> 
> Now, my question is whether the lack of description when registering
> hypothesis_selection is intentional or is it a bug?
> 
> --
> Regards,
> Piotr Trojanek
> 
> On Tue, Nov 12, 2013 at 10:58:01AM +0000, Piotr Trojanek wrote:
> > Dear Why3-club,
> > 
> > I believe that the "hypothesis_selection" should help in proving my
> > goals, but I am unable to apply this transformation.
> > 
> > I have checked that:
> > - the configure script outputs "Hypothesis selection    : yes"
> > - the plugin file is compiled, installed and detected properly
> > - the plugin is executed, because I see a debug print message that
> >   I have put just before the "Trans.register_transform" call
> > 
> > However, the "hypothesis_selection" is missing from the output of
> > 'why3 --list-transforms' and is not available in the why3ide.
> > 
> > Any advice?
> > 
> > --
> > Piotr Trojanek

-- 
Piotr Trojanek
-------------- next part --------------
A non-text attachment was scrubbed...
Name: hypothesis_selection_desc.patch
Type: text/x-diff
Size: 505 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131112/83a4ad80/attachment.patch>


More information about the Why3-club mailing list