3

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?

9
  • 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). Jan 25, 2017 at 17:55
  • 1
    @AntonTrunov: This recommendation seems to be a bit involved. Cannot Coq be installed directly from homebrew?
    – Zimm i48
    Jan 26, 2017 at 10:24
  • 1
    @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. Jan 26, 2017 at 10:27
  • 1
    @AntonTrunov: Right, opam has some advantages, but for beginners I suppose it may result in unnecessary complications.
    – Zimm i48
    Jan 26, 2017 at 10:29
  • @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
    Jan 26, 2017 at 12:41

2 Answers 2

4

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.

1
  • I think the default install location (and the one to add to your path) is C:\Coq\bin. Apr 12, 2022 at 7:47
0

When using Mac, just run

brew install coq

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.