1

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
Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
  • cross posted: https://www.quora.com/unanswered/How-does-one-switch-which-to-a-specific-version-of-Coq – Charlie Parker Jan 28 '19 at 01:35
  • It looks like you ran `./configure` without `-local` but never did `make install`? – Jason Gross Jan 29 '19 at 01:16
  • 1
    @JasonGross I don't remember exactly how I did this. Perhaps I should just start again from scratch? (note, I also want to be able to switch back to my usual Coq potentially, because I don't want weird issue with ProofGeneral once I go back to develop Coq code as normal...or what do you think? Using TCoq for both should be fine?) – Charlie Parker Jan 29 '19 at 01:27
  • related: https://stackoverflow.com/questions/71117837/how-does-one-install-a-new-version-of-coq-when-it-cannot-find-the-repositories-i for m1 mac machine – Charlie Parker Jun 08 '22 at 18:29
  • I was suggest to do this: `opam pin add coq ` for a specific coq version. Though not sure exactly what that does or compare with `coq install coq `. – Charlie Parker Jun 08 '22 at 19:59

2 Answers2

0

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/
Charlie Parker
  • 5,884
  • 57
  • 198
  • 323
  • I was suggest to do this: `opam pin add coq ` for a specific coq version. Though not sure exactly what that does or compare with `coq install coq `. – Charlie Parker Jun 08 '22 at 19:59
-1

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.

Charlie Parker
  • 5,884
  • 57
  • 198
  • 323