How to install Coq

2
votes

I have been installing Coq using the download links from the https://coq.inria.fr/ for both Windows and Mac. However, when I try coqc or coqtop on terminal or command prompt I get error messages saying that the command is not found. Although with that being said, I can still run Coq almost perfectly fine on the Coq IDE but when I compile buffer, in particularly the exercises from Software Foundations, i get the following message.

Running: coqc -I '/Users/zhangsheng/Desktop/G/repos/Coqy/cis500' '/Users/zhangsheng/Desktop/G/repos/Coqy/cis500/Basics.v' 2>&1

From what I understand, 2>&1 seems to be some form of misdirection and I feel that is the reason why coqc and coqtop don't seem to work on my terminal/command prompt.

Could someone kindly suggest the 'best' way to install Coq on either Mac or Windows or both such that I don't get the problems I mentioned above?

1
coqcoqide
For Mac you can use opam to install coq (opam is a source-based package manager for OCaml ecosystem). To install opam one can use homebrew, which is a package manager for macOS (homebrew uses both binary and source-based packages). – Anton Trunov
@AntonTrunov: This recommendation seems to be a bit involved. Cannot Coq be installed directly from homebrew? – Zimm i48
@Zimmi48 Oh, yes, you are right :) It's just when experimenting with Coq's versions and different packages, it's easier (for me) to use opam. – Anton Trunov
@AntonTrunov: Right, opam has some advantages, but for beginners I suppose it may result in unnecessary complications. – Zimm i48
@AntonTrunov Thanks for your recommendation. Does using opam give me OCaml so that I can then do my installation by cloning the Coq repo? Would be good if I can get more explicit instructions on the installation process. – Zhangsheng

1 Answers

3
votes

Although I am not a Windows or OSX user, I imagine that you're having this problem because the Coq installer does not update the system's PATH variable. This variable is a list of directories used by the terminal to look up the programs corresponding to commands you type. If you don't want to install Coq via a different method, you should probably find where the coqc and coqtop binaries are installed, and add these directories to your PATH. Here are a few references on how to do this: OSX, Windows.