Installing Coq for SSFT

Part 1 - OS-specific preparation

Windows

First, install Opam for Windows.
The graphical installer should work well, taking the 32-bit or 64-bit version according to your machine.
The installation should prompt you for the Cygwin packages that you want installed. Make sure you select the emacs-w32 package and the emacs package (you may have to select the "Full" list of packages to see them).
After the installation (which may take some time), you will access our working environment by launching Cygwin: This gives you a shell, similar to that found on UNIX systems.

OSX

First install Aquamacs and homebrew.
Then in a shell:
brew install opam
brew install proof-general --with-emacs=/usr/local/bin/emacs (This should be the executable of Emacs. You can confirm by executing 'which emacs' in a terminal window.)

Recent Debian or Ubuntu

In a shell, as a super-user:
apt-get install m4 opam emacs proofgeneral

Part 2 - Installing Coq if you have opam (Linux, OSX, Windows)

If anything in the following installation does not work, switch to Part 3.

In a shell:
opam init && eval `opam config env`
opam repo add coq-released https://coq.inria.fr/opam/released
opam update && opam upgrade && opam install coq coq-mathcomp-ssreflect

The next step is to get an IDE for Coq working. Two of them exist:

CoqIDE - the easiest to install

In a shell:
opam install coqide
You should then be able to start the CoqIDE program, a GUI for Coq, by running:
coqide &

Emacs + Proof General - the most professional

Make sure you have emacs/Aquamacs installed, as well as Proof General:
For Linux and OSX, instructions can be found at the beginning of this page to do this via your OS package manager, or homebrew for OSX.
For Windows, emacs should be installed if you succeeded to install opam for Windows as described above; add Proof General by downloading and decompressing https://github.com/ProofGeneral/PG/archive/master.zip. (You can also do this in Linux and OSX, it will actually give you the latest version of Proof General, the zip file being from github.)

To set up your emacs Coq environment, edit emacs's config file. This file is usually called .emacs in your home directory (or the directory where you installed Cygwin), or in a subdirectory called .emacs.d (with various possibly names such as init.el). For Aquamacs, the file is probably called Preferences.el, to be found in an appropriate directory.

This file might be empty or might not exist, in which case you can just create it. I suggest you then add the following code to that file:

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Load Melpa package managers

(require 'package)
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/"))
(package-initialize) ;; You might already have this line

;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; CUA (this is to have the standard keystrokes for cut/copy/paste)
(custom-set-variables '(cua-mode t nil (cua-base)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Cursor (this is to have a cursor instead of a block)
(add-to-list 'default-frame-alist '(cursor-type . bar))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Opam
;; Add opam emacs directory to the load-path
(setq opam-share "OPAM_PATH")
(add-to-list 'load-path (concat opam-share "/emacs/site-lisp"))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Proof General
(load-file "PG_PATH/generic/proof-site.el")

where

OPAM_PATH is the path that is given as the output of the shell command
opam config var share
It should probably start with "/home/..."
Warning: for Windows+Cygwin users, this path will be preceded by the cygwin directory; you should ignore the Cygwin directory, and only keep the part looking like "/home/..."
PG_PATH is the home path of Proof General (just check that generic/proof-site.el exists). For instance, for a version of Proof General installed via one of Ubuntu's package managers, this path is
/usr/share/emacs/site-lisp/proofgeneral
For the version of Proof General that is obtained via the zip file above, it is the PG-master subdirectory of wherever you unzipped the archive.

Part 2 - Installing Coq if you do not have opam

Download and install the version of Coq that is appropriate for your system

You should be able to start the CoqIDE program, an IDE for Coq.

You can also still try setting up the Emacs + Proof General IDE, as described below, a Coq development environment that is usually preferred.

Install emacs from https://www.gnu.org/software/emacs/download.html.
Then add Proof General by downloading and decompressing https://github.com/ProofGeneral/PG/archive/master.zip.
Then edit emacs's config file, usually called .emacs. This file might be empty or might not exist, in which case you can just create it. I suggest you then add the following code to that file:

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Load Melpa package managers

(require 'package)
(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/"))
(package-initialize) ;; You might already have this line

;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; CUA (this is to have the standard keystrokes for cut/copy/paste)
(custom-set-variables '(cua-mode t nil (cua-base)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Cursor (this is to have a cursor instead of a block)
(add-to-list 'default-frame-alist '(cursor-type . bar))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Proof General
(load-file "PG_PATH/generic/proof-site.el")

where PG_PATH is the home path of Proof General (just check that generic/proof-site.el exists). For instance, for a version of Proof General installed via one of Ubuntu's package managers, this path is
/usr/share/emacs/site-lisp/proofgeneral
For the version of Proof General that is obtained via the zip file above, it is the PG-master subdirectory of wherever you unzipped the archive.