Le 14/08/2018 à 18:36, Stephen Siegel a écrit :
Thanks, Guillaume, I figured it was something like that. Is this due to a change of syntax in the language, and are these changes documented somewhere?
These changes are summarily documented in the appendix of the user manual: http://why3.lri.fr/doc/changes.html
My student Ziqing has tried to use 1.0 but got this: File “why3_solution_challenge_1.mlw”, line 13, characters 2-13: Library file not found: int Maybe he has not configured things properly; I will ask him try to figure it out.
Yes, it is presumably a configuration issue, since "int" is part of the standard library. Make sure to run "why3 config --detect" when you upgrade from 0.88 to 1.0.
Best regards, Guillaume _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
