Hello Nicolas, Le 19/09/2016 à 15:39, Niols a écrit : > The compilation goes well, and the transformation is available in the > IDE. But when I try to use it, nothing happens. I tried to use debug > messages, and the transformation seems to be applied on the right task, > but nothing changes in the IDE, except that, when I try to apply other > transformations, they are only scheduled but never applied: the IDE > seems to be blocked in an inconsistent state.
Not really blocked, but nothing happens because the transformation fails. This can be seen by looking at the standard error, where you should see : Failure in transformation eliminate_exists The task already ends with a goal Instead of using the IDE, is is better for debugging transformations to use the "why3 prove" command, e.g. why3 prove -a eliminate_exists -D why3 <your test file> -a applies the given transformation, and -D why3 instructs to print the result in why3 syntax (why3.drv is just a driver like drivers for provers) The reason for your error is here > | _ -> > [create_prop_decl Pgoal pr t] you should put back a "Paxiom" in the task instead. - Claude -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/why3-club
