Installing Coq

From POPLmark

[edit] Coq and Coqide

Binaries for the latest version Coq (which is 8.1pl2, as of this writing) and the graphical user interface Coqide can be found at [1]. We detail below platform-specific installation instructions that are not mentioned on that page.

WARNING: There exist reported problems for Coqide under Linux and Mac OS X, and the instructions for Coqide should be updated! --Dimitriv 16:40, 27 November 2007 (EST)

[edit] Windows

Simply download the .exe installer and run it, letting it install Coq in the default location.

[edit] x86 Linux

Your Linux distribution may already come with a package for Coq. Otherwise, for RPM based systems, install Coq and Coqide from the provided .rpm files. For all other systems, download the appropriate .tar.gz file. To install Coq into /usr/local, run

 tar -C / -xvzf coq-<something>.tar.gz

where something should be replaced according to the name of the file that you downloaded. (You probably need to run this command as root, e.g., by using sudo.) Make sure that /usr/local/bin is in your path and that /usr/local/lib in your library path; this is usually the case by default.

A note about Gnome: If you're running Gnome, you may need to modify the keybindings for CoqIDE to avoid conflicts with the window manager's key bindings. See this page for some tips on how to do so.

[edit] Mac OS X

Download the appropriate .dmg files for your computer, mount the disk images, and install Coq and Coqide from the .pkg files contained in the disk images.

[edit] Proof General

After installing Coq, one can install Emacs and Proof General as follows. This is only necessary if you prefer to work in Emacs or cannot get Coqide to work. (Functionally, Proof General and Coqide are equivalent.)

[edit] Windows

The instructions here are courtesy of Vasileios Koutavas.

1. Emacs: Install a recent version of GNU Emacs (21.3 or later should work, preferrably 22.1). For example, download [2] and extract it in a suitable directory, e.g., C:\Program Files\emacs. Optionally, run the program C:\Program Files\emacs\emacs-22.1\bin\addpm.exe to create a Start Menu item for Emacs.
2. Proof General:
   1. Download a recent development release of Proof General (e.g. 3.7pre071112) from [3] GNU Emacs communicates with the Coq process in unicode, but the stable release of Proof General can't handle unicode and hangs. Install Proof General in a local directory (e.g., C:\Program Files\ProofGeneral-3.7pre071112).
   2. Make sure that there are no .elc files in C:\Program Files\Proofgeneral-3.7pre071112 and its sub-directories. The development release shouldn't have any, but if it does, then simply delete them. (The .elc files are sometimes precompiled for XEmacs).
   3. Open your .emacs file, and add the following two lines to it:

    
     (defvar coq-prog-name "Start-Coq.bat") 
     (load-file "C:/Program Files/ProofGeneral-3.7pre071112/generic/proof-site.el") 

   4. Create a file Start-Coq.bat that sets the right Coq environment variables and save it in the Emacs exec-path (e.g., C:\Program Files\emacs\emacs-22.1\bin). Below, we give the contents of a sample Start-Coq.bat file.

    
     @echo off
     set COQTOP=C:\PROGRA~1\Coq
     set COQLIB=%COQTOP%\lib
     set COQBIN=%COQTOP%\bin
     set PATH=%PATH%;%COQBIN%
     set HOME=%HOMEPATH%
     %COQBIN%\coqtop.opt.exe -top "%COQTOP%" -emacs-U
   

To check that everything has been installed correctly, open a file named Test.v in Emacs, check that Proof General loads, and type:

 Definition A:Set.

Go to the end of the file and press C-c C-n. The above line should be underlined and the *goals* buffer of Emacs should be updated.

[edit] x86 Linux

We assume that Coq is installed under /usr/local, as was described above.

1. Emacs: Most Linux distributions include a package for a recent version of Emacs. Otherwise consult [4].
2. Proof General:
   1. Download a recent development release of Proof General (e.g. 3.7pre071112) from [5]. GNU Emacs communicates with the Coq process in unicode, but the stable release of Proof General can't handle unicode and hangs.
   2. Install Proof General by running:

       tar -C /usr/local -xzf ProofGeneral-3.7pre071112.tar.gz 

      You probably need to run this command as root,e.g., by using sudo.
   3. Remove all .elc files from the installation (they are sometimes pre-compiled for XEmacs). If you have GNU Make, simply run make clean at the root of the Proof General installation directory.
   4. Add the following line to your .emacs file:

    (load "/usr/local/ProofGeneral/generic/proof-site.el")
   

Assuming that you installed Coq in a location such as /usr/local, there is no need to modify environment variables. To check that everything has been installed correctly, open a file named Test.v in Emacs, check that Proof General loads, and type:

 Definition A:Set.

Go to the end of the file and press C-c C-n. The above line should be underlined and the *goals* buffer of Emacs should be updated.

[edit] Mac OS X

Emacs 22.1 is available as a MacPorts package ([6]). Installing Proof General is the same as under Linux.