CODEWITHSUNDEEP
coqopam
Carl Patenaude Poulin
Carl Patenaude Poulin

Reputation: 6570

Configure OPAM switch for installation of Coq packages

Since OPAM 2.0, after installation one is required to create/select a "switch" before installing packages. If all I'm using OPAM for is Coq packages, what should I use as my switch?

Upvotes: 2

Views: 672

Answers (1)

Yves
Yves

Reputation: 4236

here is a sequence of command I applied just yesterday to get coq up and running with opam, on a machine where I was not expecting anything. It happens to be a fedora-32 machine, but I expect a similar script to work on other architectures. Anyway, the only specific command is the one to install opam, and apparently this is already done on your machine.

# execute this command with root privileges, for instance via sudo
dnf install opam

For you, only the following lines should be needed.

# the rest shoud be done without root privilege, as the plain user

opam init # I usually answer no to the questions asked
# replace coq-experiment with the name you like
opam switch create coq-experiment ocaml-base-compiler
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-interval --yes # just an example

The last --yes option is so that you don't have to answer an extra question, but you may want to omit this option to see what will be installed and agree to it.

Then it is often handy to type as the next command

eval $(opam env)

And you should have coqtop, coqc, available as shell command. If you wish to use coqide, you can simply request for its installation.

opam install coqide

and that should be it.

The opam switch command should only be needed if you wish to have several different version of Coq available at the same time on your computer. This is sometimes needed if some package has not been ported to a recent enough version of coq.

Upvotes: 3

Related Questions