What’s the simplest way to install this library and achieve the state where I can simply “Require Import MathClasses” and use it? On Windows.
Thank you in advance!
2 Likes
Some libraries, like MathComp, are included (https://github.com/coq/coq/wiki/Installation-of-Coq-on-Windows#installation-from-binaries-github-releases), but MathClasses isn’t.
Maybe could install that library from source via make install, after installing either Cygwin or Msys2, but I’m not sure of the exact procedure, and it doesn’t sound so easy.
That webpage lists some alternative install methods;
I’d probably use either WSL + opam or a Linux virtual machine.
Last, they discourage opam, but from the issue they link, it seems like it might work, but not be easy to use.
I hope somebody else has better solutions?
1 Like
The Coq Platform project will provide an easy way to install a fixed set of standard Coq packages on any system. This will extend and stabilize the work that has already been done with @MSoegtrop to support installing some Coq packages in the Windows installer (mentioned by @Blaisorblade above), but will also support macOS and Linux. However, as this will be a fixed set, there will always be packages that will fall out of its scope. In this case, other solutions, like using opam within WSL, Cygwin or Msys2 will be necessary. The goal is (only) to make the newcomer experience as easy as possible.
So to answer the question generically, I’m not a regular Windows user myself but from what I gathered, it would seem that using opam under WSL is one of the most reliable solutions (documented here). Depending on what interface to Coq you want to use, this might be more or less difficult to set up. CoqIDE is usually the preferred interface on Windows because it is shipped in the binary installer, but from the documentation here, it would seem that VsCode is the most straightforward to install (no need for an X server) and to connect to WSL (no need for wsl-alias thanks to the Remote - WSL extension).
Disclaimer: I haven’t tested this setup myself yet.
1 Like
If it is just about this library, I can quickly add it and provide an installer.
If this is a general question it is not easy to answer. I am still working on a solution. that is a script to setup a cygwin which easily allows to build libraries for MinGW Coq via opam. The main issue here is that one needs a heavily patched opam repo for this, but the goal is that the Coq opam repo can be used unchanged. That is patches shall only be required for prerequisites.
1 Like