search

coq / coq.github.io

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

Privilege installing Coq via opam #153

Closed carlpaten closed 3 years ago

carlpaten commented 4 years ago

Installing Coq via opam gives access to community packages, which I imagine would be a common ask. I was surprised when I needed to reinstall Coq because the version I installed using apt wasn't recognized by opam as fulfilling the dependency on coq.

I'm not wed to the specific wording here.

Zimmi48 commented 4 years ago

I was surprised when I needed to reinstall Coq because the version I installed using apt wasn't recognized by opam as fulfilling the dependency on coq.

Yeah, that's too bad that dependencies that are installed system-wide are not recognized...

I'm OK to strengthen the wording in favor of opam but not this much. For instance, you could write "this is the recommended method... if you want to install third-party Coq libraries...".

On Windows, the trade-off between the added complexity of compiling with opam in a Linux-like environment vs the reduced flexibility of the Windows installer (which already includes a number of third-party libraries by default) is less clear.

More generally, for newcomers who are not used to the console, opam can be a huge barrier of entry. This is also why we are hoping to provide a Coq platform (i.e. an installer of Coq + several common third-party libraries) for several systems (at least Windows and macOS) in the short-term future.

Zimmi48 commented 3 years ago

@lilred: The Coq platform is now a reality. In particular, its interactive scripts allow to easily install Coq with opam on all major systems. I'm updating the website to account for this and to explicitly warn users against installation methods that do not give access to third-party libraries. See #162 (supersedes this PR).