We recommend two ways to interact with Coq:
- (Friendly for beginners) Use CoqIDE, which is included in the standard Coq installation process.
- (Recommended, if you work on large Coq projects) Use Coq + Emacs + Proof General.
Install Coq (and CoqIDE) on Windows:
- (1) Download the Coq platform from https://coq.inria.fr/download , and install it. As an example, my installation directory is "C:\Coq".
- (2) Add the installation directory (in my case "C:\Coq\bin") to the system environment "Path".
Install Coq + Emacs + Proof General on Windows:
Install Emacs on Windows:
References (in particular, if you are a non-Windows user, please read):