CODEWITHSUNDEEP
coqopam
Charlie Parker
Charlie Parker

Reputation: 5199

How does one switch to a specific version of Coq -- especially when managing Coq versions with Opam?

I am currently using the standard one I installed the standard way (probably through the website). But I want to use tcoq. I believe I have installed it correctly because I have a bin file and all the usual Coq stuff seems to be there:

pinno:~/gamepad/tcoq $ ls bin
coq-tex     coqc        coqchk.byte coqdep_boot coqmktop    coqtop.byte coqworkmgr  gallina
coq_makefile    coqchk      coqdep      coqdoc      coqtop      coqwc       fake_ide    ocamllibdep

I tried doing an alias:

alias tcoq="/Users/pinno/gamepad/tcoq/bin/coqc"

to it in my vimrc which does run the right command but then I get further errors like:

pinno:~/gamepad $ tcoq examples/foo1.v > examples/foo1.dump
Error: cannot guess a path for Coq libraries; please use -coqlib option

which makes me think I didn't properly create the command to switch to this version of coq fully. How do I do such a thing?

Edit using Opam to manage Coq versions

I am specially interested in how to do this when managing Coq with opam. Commands I usually run for this:

# - install opam
# brew install opam # for mac
conda install -c conda-forge opam
opam init
# if doing local env? https://stackoverflow.com/questions/72522412/what-does-eval-opam-env-do-does-it-activate-a-opam-environment
# eval $(opam env)

# - install coq: see https://stackoverflow.com/questions/71117837/how-does-one-install-a-new-version-of-coq-when-it-cannot-find-the-repositories-i
# local install
#opam switch create . 4.12.1
#eval $(opam env)
#opam repo add coq-released https://coq.inria.fr/opam/released
#opam install coq

# If you want a single global (wrt conda) coq installation (for say your laptop):
opam switch create 4.12.1
opam switch 4.12.1
# eval $(opam env)  # why don't I need this in the global, what makes this global?
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq

Upvotes: 1

Views: 891

Answers (2)

Charlie Parker
Charlie Parker

Reputation: 5199

I was suggest to do this: opam pin add coq <version> for a specific coq version. Though not sure exactly what that does or compare with coq install coq <version>. Pin keeps it in that version regardless of future opam commands.

Upvotes: -1

Charlie Parker
Charlie Parker

Reputation: 5199

Not a very interesting answer, but I just followed the instructions again and it seems to work. Go to https://github.com/ml4tp/gamepad and do the read me file. The command that sets up PATH is:

IMPORTANT: set your terminal to point to the built version of tcoq (by setting right PATH) source build_config.sh

which contains:

COQBUILD=$PWD/tcoq/build

export PATH=$COQBUILD/bin:$PATH
export COQ_MK=$COQBUILD/bin/coq_makefile
export COQBIN=$COQBUILD/bin/

Upvotes: 0

Related Questions