Install Coq

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 Coq 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".

To install Coq + Emacs + Proof General on Windows, you have two ways:

(Recommended) Install Coq and Emacs first, and then follow the quick installation instructions to install Proof General in Emacs.
(Old way)
- Install Coq.
- Download Proof General (the zip package) at https://github.com/ProofGeneral/PG. Unzip the package in your installation directory. As an example, I put it at "C:\PG". It seems unnecessary to do any installation or run "make".
- Install Emacs.
- Add the following line to the .emacs file (change the directory to your own installation directory for proof general):
  
  (load-file "c:\\PG\\generic\\proof-site.el")

Install Emacs on Windows:

(1) Download Emacs for windows from https://www.gnu.org/software/emacs/download.html#windows or https://sourceforge.net/projects/emacsbinw64/.
(2) Run emacs after installation, and do some random change of options in the "Options" menu (you can always change it back) and then press "Save options". This will generate ".emacs" in your HOME directory. For me on Windows 10, as an example, the generated .emacs file is found at C:\users\userID\AppData\Roaming .