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.
Why3-club mailing list