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.

Why3-club mailing list

Reply via email to