Expand explanation on opam

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#5207 From: @Lionel-Rieg Reported version: 8.6

[coqbot]

Comment author: @Lionel-Rieg

In addition to the current explanations, I think the following information should be added to the page describing Coq installation via opam:

• Make sure that the location where Coq packages are installed is indeed in the path looked by Coq. It is currently not the case and it makes any installed package unusable unless one manually add the [Add Rec Loadpath] to the correct location of user contribs. This defeats the whole purpose of the Coq Package Index.

• How to avoid typing export OPAMROOT=~/opam-coq.8.5.2 eval opam config env inside each new terminal windows. What I have in my .bashrc for instance (although I do not remember where it comes from) is . ~/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true

• How to get the development version of Coq, with opam directly checking out the git repository. This is clearly not for beginners but would still be useful for more advanced users and I could not find any information about it (although I know it is possible).

• How to have multiple versions of Coq simultaneously through opam (both the root and switch methods).

[Zimmi48]

Most of these issues have been addressed. The only thing that remains to document is how to get the development version of Coq, which is just barely documented in the README of the opam archive but nowhere on the website: https://github.com/coq/opam-coq-archive#opam-archive-for-coq