Installation of Coq on Windows
A binary installer for Windows is available at https://github.com/coq/coq/releases/latest Since version 8.8, this installer also includes the possibility to install additional Coq packages (right now, only Bignums is provided).
It is far from an easy task to compile Coq on Windows. Effort is currently under way to make it easier (see #7157).
Some features of Coq are not yet supported under Windows. This includes the native compiler and parallel proof processing in CoqIDE. If you want to take advantage of these features, you are advised to install GNU/Linux in a virtual machine and run CoqIDE from there.
- Install VirtualBox for Windows (open source edition).
- Allocate a virtual hard disk in VirtualBox (at least 4 GB).
- Install Ubuntu inside VirtualBox (there are many tutorials on the internet explaining this).
- Run the virtualized Ubuntu.
- From the virtualized Ubuntu, find the menu "Install Guest Additions" for smooth integration of keyboard and mouse.
- Activate either "Full-screen Mode" or "Seamless Mode" for obtaining a larger display.
- Install Coq following the Installation of Coq on Linux tutorial.
To the extent possible under law, the contributors of the Rocq wiki have waived all copyright and related or neighboring rights to their contributions.
By contributing to the Rocq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.