Le 19/02/2018 à 13:59, Julia Lawall a écrit : > Sorry, I don't understand the sequence of operations. First I start up > why3 ide. Then I click on my goal and then on Coq. This gives me a Coq > line with (not yet edited). In the tools menu, I found "Mark as > obsolete". After clicking on that I get (not yet edited) (obsolete). > After these operations I still have > serial_Policy1_population_left_invariant_11.v s the largest numbered file > in my subdirectory. Clicking on replay seems to do nothing. Clicking on > edit gives a new file serial_Policy1_population_left_invariant_12.v in > which my lemma is not proved.
I wonder if your sequence of operations is correct even on one machine only. After 1) selecting a goal 2) clicking on button "Coq" 3) selecting the line "(not yet edited)" 4) clicking on button "Edit" you should see a CoqIde window appearing (or Emacs/Proof general if your configured for it), where you can complete the proof when the Coq proof is completed (or even it is not yet completed) you can close CoqIde (and save the file), and close Why3Ide (and save session) Then, when restarting Why3ide again, you should see you former Coq proof. If that works on one machine, this should work on the other, if the directory with the .xml file and the .v file is put under git. - Claude PS: I don't think the "mark as obsolete" operation is required, "edit" will notice if your Coq version is different -- 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 https://lists.gforge.inria.fr/mailman/listinfo/why3-club
