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.
julia
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
