The quick guide on https://coq.inria.fr/opam/www/using.html doesn't work

[maksr]

Operating system

Ubuntu 18.04

Description of the problem

The guide on https://coq.inria.fr/opam/www/using.html doesn't work on my Ubuntu 18.04. I installed the opam from Ubuntu distro. The command you give

opam init -n --comp=ocaml-base-compiler.4.02.3 -j 2 # 2 is the number of CPU cores

fails with

Cannot find /home/maksr/opam-coq.8.8.2/compilers/ocaml-base-compiler.4.02.3/ocaml-base-compiler.4.02.3/ocaml-base-compiler.4.02.3.comp: ocaml-base-compiler.4.02.3 is not a valid compiler name.

Searching the web I found that I must give the following command and this one worked for me:

opam init -n --comp 4.02.3

The last of the four commands

opam install coq.8.8.2 && opam pin add coq 8.8.2

failed as well, with

[ERROR] No package matches coq.8.8.2.

Using opam show coq I found the last version in http://coq.inria.fr/opam/released is 8.8.1 (today is October, 27th, 2018).

So I deleted the ~/opam-coq.8.8.2 and repeated the commands with 8.8.1 which seems to be working.

[Zimmi48]

There are two issues:

• The first is that the doc is for OPAM 2.0. This should be made explicit and in fact, there should be instructions for both OPAM 1.2 and OPAM 2.0.
• The second is that Coq 8.8.2 is only available in the OPAM 2.0 repository. There is a PR (coq/opam-coq-archive#495) to add Coq 8.8.2 for OPAM 1.2. @gares @mattam82: What is delaying the merge of this PR?

An additional issue is that the instructions suggests using version 4.02.3 of the compiler which is the minimum version supported. It would be wiser to recommend installing the latest version supported (4.07.0).

[mattam82]

I was basically waiting for @gares to ok it. Given the blocking status, I'll merge it now.

[gares]

Issue 2 is "solved" by the PR your merged, but issue one is still valid. In fact we should just have both lines, one for opam1 and for opam2, as @Zimmi48 suggested. I don't have time for this right now, sorry.

[mattam82]

I fixed the instructions to reflect both opam 2 and opam 1.2.0 but didn't change the ocaml version yet. 4.07.0 had issues with native compilation, no? Shouldn't we recommend 4.07.1 instead?

[Zimmi48]

@vbgl knows but I think it had issue with some extracted code.

[ejgallego]

See https://github.com/coq/coq/pull/8868/commits/d6a5b036ba11850441afe86dedfe8f3591df9cad

[clarus]

@maksr Now the instructions include that opam should be of version 2 (and opam 2 is now largely available). Does that solve your issue?