On Mon, 19 Feb 2018, Guillaume Melquiond wrote:

> 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.

It does not appear. It does work when I move from one clone of the git
repository to another on the same machine.  I'll see later what happens
when I move to a different machine.  I think that the versions of Coq are
the same (have the same number).  But they are not compiled with the same
version of OCaml.

Why3-club mailing list

Reply via email to