The Coq mailing list

[Michael Soegtrop <MSoegtrop AT yahoo.de>]

Hi Benoit,

> In my case I am stuck at version 8.8.x, and the reason being my
> researched depended a lot on specific version of VST & subsequently
> Compcert.

Did you modify VST tactics and would have to maintain these 
modifications or is just so that your proofs break after an update? When 
I update also some of my VST proofs break, but rarely in a bad way. 
Usually what happens is that the entailer of a newer version can prove 
things automatically the previous one couldn't. Since the Coq platform 
creates a new opam switch it is easy to use the old and the new version 
in parallel. So I bring up two CoqIDEs, load the failing fail in both 
versions, navigate to the point where things deviate - usually I just 
have to delete a few lines. For the last few updates of VST the process 
didn't take longer than until lunch for my complete VST code base. For 
an update from 2.0 to 2.7 it might take a bit longer but I think this 
time is more than made up for my new features of Coq, especially in the 
area of reliable automation.

Best regards,

Michael