This method is intended for beginners. For advanced users it is recommended to compile Coq from sources via opam (see next section).
In case you want to use the fast path:
- Download the installer from https://github.com/coq/platform/releases (click on "Assets" at the end of a release section)
- Run the installer and follow the instructions
A note to lecturers: it is easy to create a customized Windows installer from an opam switch - see Customized Installers
This method is intended for advanced users who need additional flexibility and/or an advanced working environment. For beginners it is recommended to use the Windows installer (see previous section).
- Get the coq platform scripts via either of these methods
git clone --branch 2021.02 https://github.com/coq/platform.git- download and extract
https://github.com/coq/platform/archive/2021.02.zip
- Open a command window, navigate to the download folder and execute
coq_platform_make_windows.bat - This will ask for the Cygwin installation path and setup a fresh Cygwin as build host (the created Coq is MinGW and runs without Cygwin).
- After the Cygwin setup, the script will automatically execute the common setup shell script
coq_platform_make.sh. - The script will ask a few questions if no parameters are given and then run fully unattended.
- The build time is between 1..5 hours, depending on CPU speed and RAM size.
- The script has various options for configuring paths and proxies; see
example_coq_platform_make.batfor an example command line. - The resulting Coq installation is opam based and best used from the Cygwin prompt (started via
C:\<your_coq_platform_Cygwin_path>\Cygwin.bat) - The script creates a new opam switch named
_coq-platform_.2021.02.1- this means the script does not touch your existing opam setup unless you already have a switch of this name. - Use the following commands at the Cygwin prompt to activate this switch after opening a new shell:
opam switch _coq-platform_.2021.02.1eval $(opam env)- The second step can be automated by rerunning
opam init
- The main opam repository for Coq developments is already added to the created opam switch, so it should be easy to install additional coq packages.
- For OCaml packages a specially patched opam repo for Windows is added which offers a rich but reduced set of packages (not everything builds on Windows)
- CoqIDE can be started from the shell prompt with
coqide. - The full installation might require up to 5 GB of disk space.
- It is possible to install several versions of the Coq platform in one Cygwin, as long as the pre-requisites are met. This is best achieved
by running the additional
coq_platform_make.shdirectly from the coq platfiorm created Cygwin.
This method is not officially tested but reported by users to work. Essentially you follow the instructions for Linux at README_Linux
There are no reports of virus scanners reporting any executable generated by the coq platform as virus but they sometimes lead to errors in the build process.
If a virus scanner does its work it has files and/or directories open which on Windows results in Permission denied errors in case a build system tries to rename a remove a folder or file. This is not a bug of the scanners but a design issue of Windows, namely that open files and folders are referenced by path names rather than inode numbers. An example error message is:
<><> Fetching repository information ><><><><><><><><><><><><><><><><><><><><><>
[ERROR] Could not update repository "default": "C:\\bin\\Cygwin_coqplatform_8_12_0\\bin\\mv.exe
C:/bin/Cygwin_coqplatform_8_12_0/home/Michael/.opam/repo/default.new
C:/bin/Cygwin_coqplatform_8_12_0/home/Michael/.opam/repo/default" exited with code 1 "/usr/bin/mv: cannot move
'C:/bin/Cygwin_coqplatform_8_12_0/home/Michael/.opam/repo/default.new' to
'C:/bin/Cygwin_coqplatform_8_12_0/home/Michael/.opam/repo/default': Permission denied"
[ERROR] Initial download of repository failed
In case this happens, it might help to simply retry and if this does not help to pause the virus scanner during the build or to exclude the Cygwin destination folder from scans. This might also help another issue with virus scanners: they can take considerable amounts of CPU time and RAM during a highly parallel build. A virus scanner from GData took about 3..4 cores (6..8 threads) of a Xeon CPU and almost 2.0 GB RAM during Coq platform build tests. And GData seems to be on the better side - much worse resource usage slowing down a build by a factor of ten is not unheard of.
A GData virus scanner with standard settings took about 3..4 cores (6..8 threads) of a Xeon CPU and almost 2.0 GB RAM during Coq platform build tests. For GData virus scanners it helps to disable BEAST (Behavior Monitoring) and Deep Ray in the real time protection - the resource usage is reasonable then.
In case you have advice or experience reports for other virus scanner products, please share via an issue or PR.
Especially for lecturers it might be useful to create customized installers with additional packages or a reduced package set. The scripts used to create the released Installer essentially create an installer from the current opam switch. So one can easily add or remove packages and then run the installer script. A few notes on this:
- The installer distinguishes between user selectable packages and packages which are automatically selected if needed. Dependencies between user selectable packages are also taken care of - this is done because otherwise the package list becomes much too long. The selection is done with a positive and a negative regexp filter. If the results don't match, the script aborts. In this case just adjust one or the other filter.
- This method is only tested with the full platform package set. It is likely to work with many other packages, but we cannot guarantee this, since this is not testable. Please file a ticket in case a configuration does not work.
- Creating an installer only works with Cygwin as build host, not with WSL.
- You should always test the resulting installer.
In order to create an installer, open a Cygwin shell, navigate to the platform folder and run the script windows/create_installer_windows.sh