search

coq / coq.github.io

Source files of the coq.inria.fr website
https://coq.inria.fr/
Other
15 stars 37 forks source link

Update instructions to install via OPAM #96

Closed Lysxia closed 5 years ago

Lysxia commented 5 years ago

Fixes #95

On a side note, would it be a good idea to update the old ocaml version at the top too (4.02.3)?

Zimmi48 commented 5 years ago

On a side note, would it be a good idea to update the old ocaml version at the top too (4.02.3)?

Absolutely!

gares commented 5 years ago

The choice of using a ROOT rather than a SWITCH is that, at least in opam 1.2, multiple roots can be used simultaneously, while the same is not supported using multiple switches.

Also, the version of ocaml we currently support is 4.02.3, bumped to 4.05 in the next release.

Zimmi48 commented 5 years ago

But what's the point on recommending people to use the lowest supported version of OCaml?

gares commented 5 years ago

Well, I'd like to recommend something we test. I don't think we do test 8.9 + 4.0.7. If we do, I'm fine suggesting it. IMO 4.02 works for 1 year old versions of Coq, not sure about 4.07. I think we should formalize this requirement, and have CI set up accordingly. Eg the opam archive tests 4.02 and 4.06 IIRC (dunno why not 4.05). But it does not test 4.07, so I've no clue if there are problems there.

Lysxia commented 5 years ago

Thanks @gares for the answers. So there are indeed good reasons for things to be as they are here.

Zimmi48 commented 5 years ago

The choice of root vs switch for running multiple versions of Coq at once may make sense (although for people who have such a use case, using Nix might actually be a better solution). On the other hand, it seems like the instructions should still be updated to talk about opam 2 and should only mention roots (or switches) in an advanced section. Most users do not actually need to install several versions of Coq in parallel. A possible solution would be to keep the instructions on this website to a minimum and link to a wiki page for more advanced setups.

See also #101.

Zimmi48 commented 5 years ago

See also:

export OPAMROOT=~/opam-coq.8.9.0

Why do we have this with "Instructions target an OPAM newcomer"?

in coq/coq#9969.

Lysxia commented 5 years ago

Thanks for the comments :) I may give this another shot over the weekend, if someone else doesn't get to it before!