How to install Coq, with Software Foundations

CoqIDE is a legacy IDE for Coq. It is still maintained, yet it lacks many features provided by general-purpose editors. It is fine to use CoqIDE to work through Software Foundations volumes, but if you plan to work further using Coq, you should really consider another IDE, e.g. VSCode/VSCodium.

The VsCoq extension adds support for interactive Coq proof to the VSCode and VSCodium editors.

VsCoq-1 ("VsCoq Legacy" extension) is stable, but won't evolve. It works perfectly fine for Software Foundation.
VsCoq-2 ("VsCoq" extension, version >= 2.0.0) is a reimplementation of the plugin using a more modern protocol. It also works fine for Software Foundations, however there are still a few missing features compared with VsCoq-1, e.g. shortcuts for toggling display of notations and coercions.

The Docker Engine makes it simpler to use containers, which package applications and configurations to ease deployment of software. VSCode can cooperate with Docker to smoothen the integration of Coq into VSCode.

Proof General is an Emacs-based IDE. It tends to be preferred by users who are already comfortable with Emacs. An alternative is to us VsCoq after setting up Emacs-style binding in VScode (e.g. tuttieee.emacs-mcx extension).

Coqtail enables interactive Coq proof development in Vim. It may be of interest to experienced Vim users. An alternative is to use VsCoq, after setting up the Vim extension for VSCode (vscodevim extension).

Warning: the installation via opam takes a good 15-20 minutes, because of the need to compile the OCaml and Coq tools as well as their libraries.

To install Coq via the Coq Platform, run:

      sudo snap install coq-prover

To install Coq via the Coq Platform, follow the instructions from this page.

To install Coq from system packages, run:

    sudo apt-get install coq

    sudo apt-get install coqide

If you have never used opam before, run:

    sudo apt-get install opam
    opam init

If you have used opam before, run:

    opam update

Optionally, you may want to create a separate switch for Coq (e.g. called coq):

    opam switch create coq ocaml-base-compiler.4.14.1

Next, install the relevant opam packages

      opam update

      opam install coq

    opam install coq coqide

    opam install coq vscoq-language-server

Install VSCode or VSCodium if you don't already have one of them.

They are essentially equivalent. VSCodium is an 100% open-source fork of VSCode. To install it, run:

    sudo snap install --classic codium

An alias 'code' should be automatically created for 'codium'. If not, you can run:

    echo "alias code='codium'" >> ~/.bashrc

Alternatively, to install VSCode, run:

    sudo snap install --classic code

Install VSCode:

    sudo snap install --classic code

To install the VsCoq Legay extension (and not VsCoq 2), run:

    code --install-extension coq-community.vscoq1

To install the VsCoq 2 extension (and not the Legay extension), run:

    code --install-extension maximedenes.vscoq

To test the installation of VsCoq, open a test file:

    code Test.v &

Then type in that file the following line, including the dot character:

    Check 3.

Then press the shortcut Alt+Downarrow Control+Option+downarrow.

You should get the feedback 3:nat in the output window at the bottom of your screen.

Then repeatedly press the shortcut Alt+Downarrow Control+Option+downarrow.

You should get feedback on a side panel.

To test the installation of CoqIDE, open a test file:

    coqide Test.v &

Then type in that file the following line, including the dot character:

    Check 3.

Then press the down-arrow button in the toolbar.

You should get the feedback 3:nat in the output window.

To install Proof General

ProofGeneral is an emacs package available on the MELPA repository.

Follow the Installation instructions for ProofGeneral.

To use and configure Proof General

Read the list of key bindings.

Keybindings can be customized by adding a hook to the proof-mode.

For example, the following material can be copied into your ~/.emacs file. (Alternative: ~/.emacs.d/custom.el.)

(add-hook
 'proof-mode-hook
 (lambda ()
   ;; Navigation bindings
   (define-key proof-mode-map [(f5)] 'proof-goto-point)
   (define-key proof-mode-map [(f6)] 'proof-undo-last-successful-command)
   (define-key proof-mode-map [(f7)] 'proof-assert-next-command-interactive)

   ;; Query bindings: ask for a name, by default takes the one under the cursor,
   ;; and apply from any of the three Coq buffers

   ;; Query About
   (define-key proof-mode-map [(f8)] 'coq-About)
   (define-key proof-response-mode-map [(f8)] 'coq-About)
   (define-key proof-goals-mode-map [(f8)] 'coq-About)
   ;; Query Search
   (define-key proof-mode-map [(f9)] 'coq-Search)
   (define-key proof-response-mode-map [(f9)] 'coq-Search)
   (define-key proof-goals-mode-map [(f9)] 'coq-Search)
   ;; Query Print
   (define-key proof-mode-map [(f10)] 'coq-Print)
   (define-key proof-response-mode-map [(f10)] 'coq-Print)
   (define-key proof-goals-mode-map [(f10)] 'coq-Print)
   ;; Query SearchPattern -- don't forget the parenthesis, e.g. "(_ = _ + _)"
   (define-key proof-mode-map [(f11)] 'coq-SearchIsos)
   (define-key proof-response-mode-map [(shift f11)] 'coq-SearchIsos)
   (define-key proof-goals-mode-map [(shift f11)] 'coq-SearchIsos)
   )
 )

Other useful configuration lines to include in your ~/.emacs.

;; Femove splash screen
(setq proof-splash-enable nil)

;; Auto compile modules when scripting a "Require M" and M.v has been
;; modified. Uncomment the line below only if you know what you are doing.
;; (setq coq-compile-before-require t)

To obtain the Software Foundation files, download the first volume of Software Foundation.

Let us assume the archive to be located in ~/sf/lf.tgz

Deflate the archive:

    cd ~/sf
    tar -xf lf.tgz
    cd lf

Then open Preface.v and follow instructions from there.

To compile the Coq files in the SF Volume, run:

      make

To open the first two chapters interactively:

        code Preface.v Basics.v &

Repeatedly type the shortcut Alt+Downarrow Control+Option+downarrow.

You should see the lines that are processed being colored.

To open the first two chapters interactively:

      coqide -async-proofs off -async-proofs-command-error-resilience off Preface.v Basics.v &

The options disable "asynchronous" and "error resilience" modes, improving the experience for students.

Repeatedly press the down-arrow button in the toolbar.

You should see the lines that are processed being colored.

To open the first two chapters interactively:

        emacs Preface.v Basics.v &

Assuming ProofGeneral is properly installed and SF files are compiled, Emacs should automatically enable ProofGeneral and read the _CoqProject file for configuration of Coq options.

To install Docker if you do not yet have it, follow these instructions.

If you already have Docker, make sure your existing installation is up to date.

Then make sure Docker is running :

    docker info

Install VSCode's Remote Containers Extension by typing:

    code --install-extension ms-vscode-remote.remote-containers

Open VSCode is the folder associated with the volume, by typing:

    cd ~/sf/lf
    code . &

The SF tar achive, besides the .v file for each chapter, contains a .devcontainer subdirectory with instructions for VSCode about where to find an appropriate Docker image, as well as a _CoqProject file, whose presence triggers the VsCoq extension.

VSCode should ask you whether you want to run the project in the associated Docker container. (If it does not ask you, you can open the command palette by pressing F1 and run the command Dev Containers: Reopen in Container.)

Play a file interactively: open the file Basics.v from the list on the left (or using ctrl+p). Then repeatedly type the shortcut Alt+Downarrow Control+Option+downarrow. You should see the cursor move through the file and the region above the cursor get highlighted.

To view the list of VsCoq keyboard shortcuts:

Open the extensions panel (Menu "View / Extensions", or shortcut Alt+Shift+x)
Select your "VsCoq" extension in the list
Click on the tab "Feature Contributions" on the line below the image.
The "keyboard shortcuts" are listed in the second section on the page.

[Optional] To use function keys F5, F6, F7, and F8 for VsCoq navigation:

Download the customization file keybindings1.json keybindings.json
If the file ~/.config/Code/User/keybindings.json ~/.config/Code/User/keybindings.json does not exist, save the downloaded file at this path.
Otherwise, merge the contents of the downloaded file into the existing file.
(The path may need to be adapted on Macos.)

The important new shortcuts are:

F5: reach current position
F6: backward
F7: forward
F8: reach end of file.
shift+alt+a: toggle display of notation

Accessing function keys without the "Fn" modifier key

On Apple and recent HP laptops, to access the function keys without holding the "Fn" modifier key, one needs to enable a system-wide or BIOS-level setting.

HP: unlocking "Fn" key: access the BIOS by typing F10 at the boot, navigate to system configuration, change the "Action keys mode" settings.
Apple: unlocking "Fn" key: system settings, keyboard menu, keyboard shortcuts button, function key menu, enable "Use F1, F2 as standard function keys".
Dell: unlocking "Fn" key: press "Fn" together with the "Escape" key to toggle between direct access to normal function keys or to multimedia keys. There might also be a BIOS settings or Windows setting.

Open up the download page for Coq binaries.

Click on the link entitled, e.g. Windows (64 bit) installer for Coq 8.17.1, and run the executable.

As explained on this page, you need to run a special command to set the environment variables if you want to call coqc from other tools or command line.

You might also consider the option of installing Coq inside a Linux virtual machine, hosted on your Windows system. Click the button "by installing inside a Linux virtual machine" for details.

Numerous makefiles and plugins for Coq are developped primarily on Linux-based systems. Hence, working on Coq projects is generally smoother in a Linux environment than in a Windows environment.

A practical solution is therefore to install Linux just as if it was a Windows application, then install Coq inside that Linux. The VirtualBox system offers a smooth integration of Linux apps into the Windows desktop, as well as the possibility to access the Windows file system from Linux.

For example, this page provides a relevant tutorial. Make sure to install the "guest additions".

Once your Linux virtual machine is set up, click on the buttons above for instructions on how to install Coq on Linux. If you are not a Linux expert, prefer the installation using a Docker image.

JSCoq is an interactive, web-based environment for the Coq Theorem prover.

It may be convenient to get a first glance at Coq. Yet, this interface is relatively slow and does not allow saving changes.

We therefore strongly advised students to install Coq on their system.

If you want to use JsCoq, first check out the quick-start tutorial.

Then, open this website to navigate through the volumes of Software Foundation using JSCoq.

Direct links