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.
Why3-club mailing list