The Coq mailing list

[Jeehoon Kang <jeehoon.kang AT sf.snu.ac.kr>]

Another way to install multiple instances of Coq with opam is using opam aliases:
https://github.com/ocaml/opam/wiki/Advanced_Usage#ability-to-make-a-copy-of-a-given-compiler-under-an-alias

```

opam switch install 4.02.3.coq.8.5.0 --alias-of 4.02.3

opam install coq.8.5.0

```

Then you can switch between multiple versions of Coq with `opam switch 4.02.3.coq.8.5.0` and `opam switch 4.02.3`.

Jeehoon

2016-04-25 17:42 GMT+09:00 Théo Zimmermann <theo.zimmermann AT ens.fr>:

Yes, with Opam you can have several versions of Coq at the same time.

See the advice on this page: http://coq-blog.clarus.me/use-opam-for-coq.html

Guillaume Claret has been the promoter for the use of Opam and he is the author of these two pages. As far as I know there is no official documentation on this topic yet. It would be good, at least, if someone updated the install instructions on Cocorico.

Théo

PS : I recently started looking at the Nix package manager. It is also interesting because it is kept up-to-date (Coq 8.5pl1 was available the day of the release), allows easily switching between multiple versions, does not put the dependencies in the environment and has a cache for compiled binary (thus it is much faster to install Coq with Nix than with Opam). If someone wants to discuss about it, we could start another thread.

Le lun. 25 avr. 2016 à 00:04, Tadeusz Litak <tadeusz.litak AT gmail.com> a écrit :

On 24/04/16 22:16, Beta Ziliani wrote:


> Wouldn't it be nice to have a description how to install Coq with Opam?

I think that once I got opam itself installed and used it to install OCaml (kicking out previously existing OCaml
installations) all I needed for my 8.4.6 installation was

opam pin add coq 8.4.6

In fact, this week I realized that getting Coq via Opam seems preferable to getting it via Macports, which is what I was
doing so far.  And not only because Macports are moving slower: the version available there is still 8.5.0 rather than
8.5pl1.

As you see above, I needed something opposite: I needed to revert to 8.4pl6. I am teaching a course based on SF by
Pierce et al. Not only  did 30%-40% students report problems when I tried some 8.5-specific features (bullets beyond
level three...), but more importantly, the autograder kindly made available by the Penn people (Arthur Azevedo de
Amorim) was not very happy about working with 8.5. After some experiments, I decided that not being an OCaml hacker, I
am not going to rewrite myself the autograder code  to teach it about, e.g., new philosophy of dealing with access paths
from command line level.

[Btw, while I read the relevant  discussion and I understand the reasons, I wish the Coq developer community was just a
_bit_ less cavalier about breaking down compatibility, not just of proof scripts themselves, but with things like this
too. I guess many programs and scripts invoking coqc and coqtop need to be rewritten now. But this is just by the by]

Long story short, I needed to downgrade my Coq installation. And it turned out not so easy with Macports---reverting the
Coq port to 8.4pl6 resulted in compilation problems. If I recall, Macports Ocaml also moved forward since last revision
of Coq 8.4 port. Or something.

In the end, I kicked out everything related to OCaml from Macports and decided to install everything OCaml-ish plus Coq
via Opam. This worked quite well.

And Opam offers full choice, from 8.3 to 8.5.1 at the moment!

I'm curious if I can use Opam switch to keep both 8.4pl6 and 8.5pl1. This would be the best of both words. But the
suggestion of pinning the Coq version that you see on the installation webpage is definitely very sensible.

Best,
t.




>
> Best,
> Beta

--

Jeehoon Kang (Ph.D. student)

Software Foundations Laboratory

Seoul National University