Installation of Coq on Windows

The recommended installation method is through the Coq platform.

Note though that some features of Coq are not yet supported under Windows that should work under a Linux setup. This includes the native compiler and parallel proof processing in CoqIDE. Therefore, some Windows users may prefer installing Coq in a Linux environment on top of Windows (either WSL or a full-blown virtual machine). These methods are also described below.

Coq platform

The Coq platform is a distribution of the Coq proof assistant together with a selection of Coq libraries. It provides a set of scripts to compile and install opam, Coq, external Coq libraries and Coq plugins on macOS, Windows and many Linux distributions in a reliable way with consistent results.

Binary package

Beginners are advised to use the binary installers available from: https://github.com/coq/platform/releases/latest

Installation from sources

Experienced users can rely on the Coq platform interactive scripts to install the Coq platform from sources using opam. This will install a Cygwin environment, create an opam switch with Coq and a standard set of packages, which can then be modified, e.g., by installing additional packages.

See the Windows specific instructions for the Coq platform scripts here: https://github.com/coq/platform/blob/2021.02/README_Windows.md#compiling-from-sources-with-cygwin-as-build-host

Once the Coq platform is set up, you can install additional Coq packages by running opam install coq-packagename.

User interfaces

You will need a user interface to run Coq. The Coq platform bundles CoqIDE, which is a Coq-specific editor. Alternatively, you can install editor-support packages for VsCode, Emacs or Vim. See https://coq.inria.fr/user-interfaces.html for details.

Installation of Coq in a Linux virtual machine

1. Install VirtualBox for Windows (open source edition).
2. Allocate a virtual hard disk in VirtualBox (at least 4 GB).
3. Install Ubuntu inside VirtualBox (there are many tutorials on the internet explaining this).
4. Run the virtualized Ubuntu.
5. From the virtualized Ubuntu, find the menu "Install Guest Additions" for smooth integration of keyboard and mouse.
6. Activate either "Full-screen Mode" or "Seamless Mode" for obtaining a larger display.
7. Install Coq following the Installation of Coq on Linux tutorial.

Installation of Coq in WSL

1. Enable WSL and install a Linux distribution (e.g., Ubuntu or Debian) from the official WSL page.
2. Open a WSL terminal and make sure that you are logged in as a regular Linux user (i.e., not root).
3. Install OPAM's dependencies, e.g. for Ubuntu/Debian:

   sudo apt-get update
   sudo apt-get install aspcud bubblewrap build-essential curl gcc git m4 tar unzip
   

4. Install OPAM 2.0 in WSL, using for instance the official installation script.
5. Configure OPAM using the --disable-sandboxing flag (WSL doesn't support the Linux system call needed to use sandboxing):

   opam init --disable-sandboxing --auto-setup --yes --compiler=ocaml-base-compiler.4.05.0
   eval $(opam env)
   

6. Install Coq following the Installation of Coq on Linux tutorial.

An important word about WSL and files: WSL has its own file system nested inside the Windows filesystem. The metadata on files written by WSL processes differs from that of files written by Windows processes. Windows processes must not write to files in the WSL file system; this will cause tears. On the other hand, WSL processes can safely write files in the Windows file system. WSL is aware of the difference and handles that case correctly. While the Coq binaries and libraries will be stored in the WSL file system, proof files that you create and modify in CoqIDE or emacs should be saved only in the Windows file system. For example, /mnt/c/myproofs corresponds to C:\myproofs.

Update: this limitation doesn't apply to WSL in Windows 10 version 1903. In WSL2 (in version 2004), I/O to the Windows filesystem is very slow, so it's better to put the files in Linux file filesystem. See [wsl2] filesystem performance is much slower than wsl1 in /mnt.

Front-end setup in WSL

Here are four ways to setup a prover front-end such as CoqIDE or Emacs+ProofGeneral or VsCode+VSCoq:

• (A) Run CoqIDE in WSL + an X server for Windows:
  • Install a Windows port of X server, such as VcXsrv.
  • To run CoqIDE, make sure your X server is running (VcXsrv installs an icon on the desktop), then enter DISPLAY=:0 coqide & from WSL bash.
• (B) Install a graphical Emacs in WSL + ProofGeneral + an X server for Windows:
  • Install GNU Emacs (sudo apt-get install emacs25) and ProofGeneral.
  • Install a Windows port of X server such as VcXsrv.
  • Run Emacs from WSL after properly setting the DISPLAY variable (DISPLAY=:0 emacs &).
  • To run Emacs, make sure your X server is running (VcXsrv installs an icon on the desktop), then enter DISPLAY=:0 emacs & from WSL bash.
• (C) Install a (native) graphical Emacs in Windows + ProofGeneral (no X server required):
  • Install emacs, such as Vincent Goulet's Emacs 26 installer and ProofGeneral
  • To handle Windows/WSL path translations, install wsl-alias in WSL.
  • Add this pattern to your Windows PATH: %userprofile%\wsl-alias
  • Open a Windows terminal (e.g., cmd.exe, but not WSL) and type the following commands:

    b wsl-alias add opam opam
    b wsl-alias add ocaml "opam exec -- ocaml"
    b wsl-alias add ocamlc "opam exec -- ocamlc"
    b wsl-alias add ocamlmerlin "opam exec -- ocamlmerlin"
    b wsl-alias add coqtop "opam exec -- coqtop"
    b wsl-alias add coqc "opam exec -- coqc"
    b wsl-alias add coqidetop "opam exec -- coqidetop"
    b wsl-alias list  # to proofread the list
    b                 # with no argument, to enter in WSL mode again
    

  • You should now be in the folder /mnt/c/Users/YOURLOGIN (Windows personal folder).
  • If you already have a working Emacs configuration (an example is available here), put your .emacs file in this folder, then launch Emacs from Windows icon.
• (D) Use (native) graphical Visual Studio Code in Windows (no X server required):
  • Install Visual Studio Code.
  • Under extensions install the VSCoq extension.
  • Under extensions install the Remote - WSL extension.
  • In wsl navigate to your project folder and run code .