Versioning of .why3.conf and sanity check
When developing Frama-C, we end up constantly changing between different opam switches with potentially different versions of why3, and in the process the .why3.conf
is not always updated, resulting in weird errors (the last one had some Alt-Ergo drivers dying with "File generation error" messages, without an obvious cause; even though I had run why config --detect --full-config
just before trying it).
We expect simlilar issues to happen to our users during the next Frama-C release, since we are switching from why3 1.2 to 1.3, so we will explicitly include instructions for them to erase their .why3.conf file.
In the interest of future-proofing and ease of use, we believe that, if the .why3.conf
file had some information concerning the version of why3 which generated it, for instance in the [main]
section, then it would be easy to perform a simple check when starting why3 to see if the version used to create the file is the same, and emit a warning or error otherwise.
Do you think such feature would be desirable? Do you see any drawbacks?