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?
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. -Steve > On Aug 14, 2018, at 12:20 PM, Guillaume Melquiond > <guillaume.melqui...@inria.fr> wrote: > > Le 14/08/2018 à 18:05, Stephen Siegel a écrit : >> Hello Why3 Club, >> I am trying to apply Why3 to the example here: >> http://toccata.lri.fr/gallery/verifythis_2017_pair_insertion_sort.en.html >> I downloaded the zip archive and executed, but got a syntax error: >> siegel$ why3 prove verifythis_2017_pair_insertion_sort.mlw >> File "verifythis_2017_pair_insertion_sort.mlw", line 32, characters 18-20: >> syntax error >> The error refers to the word “in” in the line “label L in” (line 32). >> This is my version of why3: >> siegel$ why3 --version >> Why3 platform, version 0.88.3 >> Does anyone know what is going on? > > You should use Why3 1.0 for most examples from the gallery. > > You can recover examples compatible with Why3 0.88 from the git repository: > > https://gitlab.inria.fr/why3/why3/tree/bugfix/v0.88/examples > > Unfortunately, as far as I know, verifythis_2017_pair_insertion_sort.mlw does > not exist for Why3 0.88. > > Best regards, > > Guillaume > _______________________________________________ > Why3-club mailing list > Why3-club@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
