The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

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