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 Why3email@example.com https://lists.gforge.inria.fr/mailman/listinfo/why3-club