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
