Installing the software for INF551

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.

Alternative: A virtual machine
If you have issues with the above, you may use a virtual machine (it will not be so well integrated to your Windows environment and it might be a bit slow, but it should work).
Download the course Debian live CD
Install VirtualBox
Launch VirtualBox, create a new 32bit debian installation, start it and choose to boot from the downloaded disk image. Choose live mode and check that everything works fine (the required programs, chromium, etc.). You can now install it on the virtual box using the link on the (virtual) desktop. Emacs and ProofGeneral are available on the Programming tab.

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 - Setting up the OCaml working environment

First, in a shell:
opam init
eval `opam config env`
opam install tuareg merlin

As of 17th September 2017, you should then get version 2.0.10 of tuareg and 3.0.2 of merlin.

Then
opam config var share
Save the path that is returned by this command; 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/..."

Then, we set up your emacs programming environment, editing 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, replacing THE PATH THAT YOU SAVED by the path saved above:

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; 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 "THE PATH THAT YOU SAVED")
(add-to-list 'load-path (concat opam-share "/emacs/site-lisp"))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Merlin stuff

;; Load merlin-mode
(require 'merlin)
;; Start merlin on ocaml files
(add-hook 'tuareg-mode-hook 'merlin-mode t)
(add-hook 'caml-mode-hook 'merlin-mode t)
;; Use opam switch to lookup ocamlmerlin binary
(setq merlin-command 'opam)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Tuareg

(load "tuareg-site-file")
(setq tuareg-indent-align-with-first-arg nil)
(add-to-list 'auto-mode-alist '("\\.mlt\\'" . tuareg-mode))
Finally, let's set-up auto-complete. In emacs, hit alt-x, which invites you to type an emacs command. Type package-install, and then the name of the package to install is auto-complete. Hit return, and emacs should download the package. Then add this to your config file:
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Auto-complete

(require 'auto-complete)
(define-key ac-mode-map (kbd "<backtab>") 'auto-complete)

Part 3 - Coq

Method 1 - if you have opam (Linux, OSX, Windows)

In a shell:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq
As of 17th October 2017, you should get version 8.7.0 of coq.

If the installation does not work, switch to method 2.

If it does, follow the instructions below to set-up the Emacs + Proof General environment.
If that set up does not work, switch to method 2.

Method 2

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

You should be able to start the CoqIDE program, a GUI for Coq.

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

Setting up the Emacs + Proof General environment

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, but if you do not have opam for Windows, you can still install opam from https://www.gnu.org/software/emacs/download.html

For Windows, 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 lattest version of Proof General, the zip file being from github.)

For any OS, once you have both emacs/Aquamacs and Proof General, you must add the following line to your emacs initialisation file:

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Proof General

(load-file "MY_PATH/generic/proof-site.el")
    
where MY_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.