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?
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.