Installing packages for Coq using OPAM

Question

I am trying to install a coq-contrib package OPAM. I am still new to OPAM and Coq. I was using OPAM 1.2.2 and was getting this:

$ opam install coq-graph-basics
Your request can't be satisfied:
- No package matches coq-graph-basics

No solution found, exiting

even though I could see it when running

opam search coq-

After reading this issue https://github.com/ocaml/opam/issues/2526, I tried upgrading to OPAM 2.0.0.

This is what I got this time when trying to install the package:

$ opam install coq-graph-basics
The following dependencies couldn't be met:
- coq-graph-basics → coq < 8.6~
not available because the package is pinned to version 8.7.2

No solution found, exiting

I am not sure what I am doing wrong here. Does anyone know what these messages mean? What am I missing?

Thanks

Focalize

You probably need opam repo add coq-released https://coq.inria.fr/opam/released (I don't remember if it's necessary but opam update won't hurt). – Viscose

I think that upgrading to opam 2.0.0 is premature. – Morten

What this means is that opam knows a package coq-graph-basics, but it is not compatible with recent versions of Coq (>= 8.6), and your version is recent (8.7.2). One solution could be to downgrade Coq, but here you rather need a newer version of the package that is compatible with recent versions of Coq. See @AntonTrunov's comment to tell opam about a repository with more recent versions of Coq packages. – Havelock

how do you install a specific version of coq using opam for the current switch? – Kamseen

Answer 1

Your error means that opam knows a package coq-graph-basics, but it is not compatible with recent versions of Coq (>= 8.6), and your version is recent (8.7.2).

One solution could be to downgrade Coq. Here, this is not proposed, because your Coq package is "pinned" to version 8.7.2, which means you told opam not to change its version. If you unpin it, with opam unpin coq, you would be proposed to downgrade Coq. But this is not the way to go here.

In your case, you rather need a newer version of the package that is compatible with recent versions of Coq. As @AntonTrunov points out in his comment, you can tell opam to look at other repositories than the default one.

The commands:

opam repo add coq-released https://coq.inria.fr/opam/released
opam update

add a repository with recent versions of most Coq packages, and in particular a recent version of coq-graph-basics.

EDIT: Coq packages are distributed using three repositories (one of them being "coq-released"). The repositories are presented here.

Havelock

Hum, this is the right procedure in general, but in this case there does not seem to exist a 8.7.2 compatible version of coq-graph-basics. – Havelock

how do you install a specific version of coq using opam for the current switch? – Kamseen

@CharlieParker As usual with opam, you can do opam install coq.8.15.2 if you want to install coq at version 8.15.2, or even opam pin add coq 8.15.2 if you want it to stay at this precise version unless you unpin it. – Havelock