The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

On 10/14/2013 09:55 AM, Thomas Braibant wrote:

Indeed, various Coq versions should coexist each with its own set of packages, and switching from one version to another should not involve recompiling Coq. My own way of doing this used to be symlinks (install various versions of coq in coqs, and do "rm coq; ln -s coqs/whateverversion coq"). Sure you do not have to recompile coqs to do that, and I bet you do something similar. 

I just keep around various source distributions and run "make install" for the one I want to switch to.  The only issues I've run into are from libraries installed to standard system-level locations, which can confuse Coq versions that aren't the ones they were compiled with.  I never intentionally use system-level library installation, anyway, so I'm mostly satisfied with this simple approach!

Hi Adam, 

Yes, this works. But the downside is that you copy files to the system-level part, and as you said, you cannot deal with system-level library installation. 

Using symlinks, you can have each coqs/version be an --local installation. Then, you have a symlink from coq to coqs/version, and the right things in your path (the COQBIN).  When installing a library, you can perform a "symlink level installation": that is, the package will be put in the right coqs/version/user-contrib. That being said, if you are fine with your workflow, I am sure we will try not to break it [1]. 

Cheers, 

Thomas

[1] http://xkcd.com/1172/