
This file might be empty or might not exist, in which case you can just create it. emacs.d (with various possibly names such as init.el).įor Aquamacs, the file is probably called Preferences.el, to be found in an appropriate directory. emacs in your home directory (or the directory where you installed Cygwin), or in a subdirectory called. To set up your emacs Coq environment, edit emacs's config file. (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.) Make sure you have emacs/Aquamacs installed, as well as Proof General:įor 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.įor Windows, emacs should be installed if you succeeded to install opam for Windows as described above add Proof General by downloading and decompressing You should then be able to start the CoqIDE program, a GUI for Coq, by running:Ĭoqide & Emacs + Proof General - the most professional The next step is to get an IDE for Coq working. Opam update & opam upgrade & opam install coq coq-mathcomp-ssreflect In a shell: opam init & eval `opam config env` If anything in the following installation does not work, switch to Part 3. You can confirm by executing 'which emacs' in a terminal window.)Īpt-get install m4 opam emacs proofgeneral Part 2 - Installing Coq if you have opam (Linux, OSX, Windows) This gives you a shell, similar to that found on UNIX systems.īrew install proof-general -with-emacs=/usr/local/bin/emacs (This should be the executable of Emacs. You will access our working environment by launching Cygwin: 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).Īfter the installation (which may take some time), The installation should prompt you for the Cygwin packages that you want installed.

The graphical installer should work well, taking the 32-bit or 64-bit version according to your machine. Installing Coq for SSFT Part 1 - OS-specific preparation Windows
