Re: [Why3-club] why3 on multiple machines

2018-02-20 Thread Julia Lawall
J'ai fait des transferts dans les deux sens entre les deux machines, et ca
marche comme il faut.

Merci,
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club


Re: [Why3-club] why3 on multiple machines

2018-02-19 Thread Julia Lawall


On Mon, 19 Feb 2018, Claude Marché 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.
>
> 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.

This is all fine.

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

I'll see what happens with this later.

thanks,
julia

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


Re: [Why3-club] why3 on multiple machines

2018-02-19 Thread Claude Marché


Le 19/02/2018 à 14:20, Julia Lawall a écrit :
> 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.

Strange. I don't think the version of OCaml is a problem.

You should look at the terminal to see of error messages appear there.

- Claude

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


Re: [Why3-club] why3 on multiple machines

2018-02-19 Thread Claude Marché


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


Re: [Why3-club] why3 on multiple machines

2018-02-19 Thread Julia Lawall


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


Re: [Why3-club] why3 on multiple machines

2018-02-19 Thread Guillaume Melquiond

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


Re: [Why3-club] why3 on multiple machines

2018-02-19 Thread Julia Lawall


On Mon, 19 Feb 2018, Guillaume Melquiond wrote:

> Le 19/02/2018 à 11:43, Julia Lawall a écrit :
> > I have two laptops, one at home, one at work.  I tried saving the state
> > (foo subdirectory, for a foo.mlw file) with git on my home machine, and
> > pulling onto my work machine.  Part of my state is a coq proof.  But when
> > I start up why3 at work and select coq, it asks me to make a new proof,
> > rather than using the one I already completed.  How can I get it to use an
> > existing coq proof?
>
> The way you did should be fine. The foo subdirectory contains both a
> session file (why3session.xml) and your Coq proof, and the session file
> tells Why3 that you already have a Coq proof. It also contains a shape
> file (why3shapes.gz), which helps Why3 to reassociate the Coq proof to
> the proper goal, in case you have modified the .mlw file.
>
> Note that, if the version of Coq is different on both computers, you
> need to mark the old proof as obsolete and replay it first, to force
> Why3 to update the proof attempt to the new version of Coq. Otherwise
> Why3 might just assume that you want to create a new proof for a
> different version of Coq rather than reuse the old one.

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.

thanks,
julia___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club


Re: [Why3-club] why3 on multiple machines

2018-02-19 Thread Guillaume Melquiond

Le 19/02/2018 à 11:43, Julia Lawall a écrit :

I have two laptops, one at home, one at work.  I tried saving the state
(foo subdirectory, for a foo.mlw file) with git on my home machine, and
pulling onto my work machine.  Part of my state is a coq proof.  But when
I start up why3 at work and select coq, it asks me to make a new proof,
rather than using the one I already completed.  How can I get it to use an
existing coq proof?


The way you did should be fine. The foo subdirectory contains both a 
session file (why3session.xml) and your Coq proof, and the session file 
tells Why3 that you already have a Coq proof. It also contains a shape 
file (why3shapes.gz), which helps Why3 to reassociate the Coq proof to 
the proper goal, in case you have modified the .mlw file.


Note that, if the version of Coq is different on both computers, you 
need to mark the old proof as obsolete and replay it first, to force 
Why3 to update the proof attempt to the new version of Coq. Otherwise 
Why3 might just assume that you want to create a new proof for a 
different version of Coq rather than reuse the old one.


Best regards,

Guillaume
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club


[Why3-club] why3 on multiple machines

2018-02-19 Thread Julia Lawall
I have two laptops, one at home, one at work.  I tried saving the state
(foo subdirectory, for a foo.mlw file) with git on my home machine, and
pulling onto my work machine.  Part of my state is a coq proof.  But when
I start up why3 at work and select coq, it asks me to make a new proof,
rather than using the one I already completed.  How can I get it to use an
existing coq proof?

thanks,
julia
___
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club