search

coq / opam

Archive for all Coq related OPAM packages organized in various repositories
https://coq.inria.fr/opam/www/
GNU Lesser General Public License v2.1
129 stars 166 forks source link

Basic instructions? #36

Closed cpitclaudel closed 8 years ago

cpitclaudel commented 8 years ago

For someone without experience with OPAM, installing coq is not the most intuitive. I've heard a lot about using OPAM to install Coq 8.5 rc1, so I naively ran

opam init
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
opam install coq

but this offered Hott/Coq. So I did opam search coq and got

# Existing packages for system:
coq          --  HoTT/Coq stable branch
coq-shell    --  Simplified OPAM shell for Coq
coqide       --  IDE of the coq formal proof management system
ott          --  Ott is a tool for writing definitions of programming languages and calculi
sibylfs-lem  --  SibylFS fork of Lightweight Executable Mathematics for large-scale semantics
zenon        --  Automated theorem prover for first order classical logic (with equality), based on the tableau method

It would be great to have a quick pointer to the right command. The instructions on https://coq.inria.fr/howto-opam say:

To install Coq:

opam install -j4 -v coq

To install a package:

opam install coq:that-super-package

To add the repository of development packages (use it at your own risks):

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev

To add the repository of development versions of Coq (use it at your own risks):

opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev

TODO: talk about the distribution mechanism.

But opam install -j4 -v coq definitely doesn't do the right thing :/

silene commented 8 years ago

Note that you didn't add the "repository of development versions of Coq", which, as its name implies (or not), does contain Coq 8.5rc1. That said, the documentation could be more explicit with respect to testing beta versions of Coq.

cpitclaudel commented 8 years ago

Sorry, I made a mistake in my original message. This is with core-dev. Having spent more time looking at this, I guess all I needed was a line in the README that said I should run the following.

opam install coq.8.5~rc1

(that being said I don't know how one guesses the right package name; I found it buried in a coq-club discussion)

gares commented 8 years ago

The issue about HoTT having precedence has been solved. I guess we can close the issue.