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
