Re: [Why3-club] why3 on multiple machines
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
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
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
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
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
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
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
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
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
