[Why3-club] Problem with the hypothesis_selection plugin

Piotr Trojanek piotr.trojanek at gmail.com
Tue Nov 12 13:15:20 CET 2013


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



More information about the Why3-club mailing list