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.
When you launch why3ide on the new machine, the old Coq proof should already appear in the proof tree. If it does not, it means that Why3 is confused by the way you moved the session file and the Coq proof from one computer to the other. Just exit why3ide and verify that the files are properly located.
If the old Coq proof does appear and if the same version of Coq is used on both computers, you don't have anything special to do; just edit it.
If the old Coq proof appears but the version of Coq is different, then you first have to mark this old proof as obsolete and replay it. Why3 should then notice that you have no suitable version of Coq to replay the old version and it should suggest to use instead your actual version of Coq. Then you can edit it.
Let me stress the original point again: If the Coq proof attempt does not appear in the tree when you launch why3ide, it means that you did not properly move the files from one computer to the other.
Best regards, Guillaume _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
