Installation of Coq on Windows

Installation alternatives

There are two alternatives for installing Coq on Windows:

The simplest is to install the Windows binary directly.

Alternatively, you can run a version of Linux on top of Windows and install Coq inside that environment. Linux can be installed as a virtual machine in Windows or under WSL (Windows Subsystem for Linux). A Linux setup may be preferable if you already use one of those environments.

You should consider whether you will want to use OPAM. The OPAM package manager makes a large number of Coq-related packages available for download. It will automatically download the dependencies of packages you request. In most cases beginners won’t need OPAM or additional packages. OPAM works fine in the Linux setup. While OPAM is available under Windows, where it relies on the Cygwin package to provide Linux commands, the current 2.x version of OPAM is almost unusable on Windows because of a Cygwin bug. (https://github.com/ocaml/opam/issues/3785 is an example of the issues.) If you want to use OPAM then a Linux setup may be easier for you.

WSL provides code that emulates most but not all Linux system calls and features. In contrast, a Linux virtual machine runs the Linux kernel, so it should be closer in behavior to running Linux standalone (i.e. without Windows). Running the virtual machine may require more resources than WSL, such as reserving part of DRAM for the virtual machine and sufficient disk space for a complete Linux installation. Also, while this writer has had a very good experience with WSL, note that Coq is not officially supported on WSL, so you may be more on your own to work around any issues you run into.

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.

The most common interfaces to Coq are CoqIDE or Emacs with ProofGeneral. With a Linux setup, you’ll need to use X-Windows to use these. (For WSL, you will need to install X-Windows separately if you want to use CoqIDE and sometimes for Emacs/Proof General.)

Compiling Coq from source code on Windows is somewhat complex and not recommended for beginners. (OPAM, by the way, generally downloads source code for packages and compiles it as part of the package installation process.) If you want to modify Coq, you will be much happier with a Linux setup.

Installation from binaries (GitHub releases)

A binary installer for Windows is available at https://github.com/coq/coq/releases/latest.

The installer also includes precompiled .vo files for the standard library. Since version 8.8, this installer also includes the possibility to install additional Coq packages. The installers for 8.8.2 and later includes these packages:

aactactics, bignums, compcert, coquelicot, equations, extlib, ltac2, mathcomp, menhir, menhirlib, mtac2, quickchick, vst

If your favorite package is missing or you want a package you maintain to be included, please create an issue.

Chocolatey

Chocolatey, is a Linux-style package manager for Windows. If you are a Chocolatey user, the following command will install Coq by fetching the binaries from the GitHub release page so the end result will be the same as if you download and run the installer manually:

chocolatey install coq -y

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 .