Coq on Windows using WSL

Using Coq
1

I am not a Windows user myself, but will be teaching a course on Coq this fall.

Someone suggested to use WSL to install Coq, as follows below.

I couldn’t find this method documented. E.g. here:

Should it be added?

On Windows 10 64bit

General:
Search for instructions for setting up WSL for GUI programs.
Then follow instructions for your Linux distribution to install Coq.

Comments:
enable Windows Subsystem for Linux (WSL)
download the Linux distribution of your choice from the Windows Store
opening the program gives you now a Linux terminal
initialize and create user
install opam and coq and coqide from terminal in Linux
need to disable sandboxing: opam init --disable-sandboxing
install X server (e.g. Xming) on Windows
set display in Linux terminal (will open a new window with the application)
DISPLAY=:0 coqide

1 Like
2

Thanks @spitters for opening this thread!
I vote for adding such installations instructions for Opam+Coq under Windows+WSL in the Coq wiki.

FYI last year in Toulouse we successfully experimented a similar setup for students’ own machine under Windows+WSL, using OCaml+Merlin+Coq+ProofGeneral under Windows+WSL, communicating with some native Emacs, and I briefly reported on that in this comment of issue coq/coq#8729.

After this @MSoegtrop told me he was interested to test that setup as well, I don’t know if he has additional feedback on this topic.

As this setup didn’t used “graphical WSL Emacs” but “native Windows Emacs”, it needed not a Windows implementation of Xorg, but indeed as you mention, a similar setup of Coq/WSL could just as well work with CoqIDE powered by a Windows port of Xorg, e.g. VcXsrv (which seems to be more up-to-date than Xming).

So I propose that we add two additional sections in the wiki page:

  • Installation of Opam+CoqIDE under Windows+WSL+VcXsrv
  • Installation of Opam+Coq+ProofGeneral under Windows+WSL

What do you think?

3

That sounds good to me.
Could you do that, as I’m not a Windows user myself.

4

I am a bit split on this. On the one hand it is a good idea to add WSL instructions, especially for power users doing Coq development work on Coq. On the other hand it might be quite a bit of work to support an additional platform - and this would be an additional platform. And I think if this is not well maintained, it might be worse than not having it because it might lead people into needless frustration.

For teaching courses I would use the Windows installer. From the feedback I got from people teaching at the HoTT summer school this year I would say that the Windows Installer is the most seamless way to install Coq. It takes 2 minutes and works always. On the other hand I have heard that even on Linux several participants had severe issues to get Coq installed and I don’t see why having the additional complexity of having WSL in between should make this any easier.

I personally started to work on replacing the Windows build system with using dune and opam, so that it is more attractive for power users and makes it easier e.g. to build customized installers for courses (e.g. for the HoTT summer school I had to create a special installer including HoTT). For Linux I think we should work on snap packets to make installation in courses easier.

5

@MSoegtrop I agree with your remarks, to sum up:

(a) adding WSL instructions in the official wiki might lead to additional maintenance work (so if one decides to add such instructions there, some volunteer, ideally a regular user of Windows − which is not my case − should be in charge of testing/maintaining that script/instructions)

(b) for students willing to use Coq on Windows, the easiness of the installation is very important (which is indeed much easier with the Coq Windows Installer, than with WSL!)

Still, there are two use cases that not intended to be addressed by the Coq Windows Installer IINM:

(1) Provide a full OPAM installation to ease the installation of additional coq-released packages on-the-fly;
(2) Make it possible to install Merlin to use Emacs with Tuareg+ProofGeneral under Windows.

To this aim, there is the Cygwin-based solution https://fdopen.github.io/opam-repository-mingw/installation/ that allows one to install a full OPAM setup for Windows: we had tested it two years ago but the installation procedure, albeit simpler, seemed a bit tricky because it was less robust than WSL (several students had problems with the syntax of their Windows username… others just told us that they weren’t able to install it)

(3) Also, even if the installation instructions of a teaching unit says “Please use Cygwin”, we realized there are sometimes students that already have WSL installed on their laptop and really prefer to use it rather than Cygwin, thinking that “WSL should be easier and more convenient” :slight_smile:

So last year, our choice of the WSL approach (which is definitely lighter than installing Coq under Linux in a VM) was motivated by these three points (1)(2)(3).

But WSL itself is not a requirement for us: if one can address (1) and (2) in a simple and robust way, we’ll be interested as well!
E.g., we didn’t test the installation of Chocolatey, mentioned in the wiki: can this address (1) and (2)?

By the way I am unsure if as you say, “it might be worse [to have it documented but not maintained] than not having it because it might lead people into needless frustration”, because as suggested in item (3) above, omitting such instructions in the official wiki could maybe add frustration for users that really want to rely on WSL…
Maybe if we are afraid that at some point the instructions are not fully up-to-date, some disclaimer could just be added there to say so and/or redirect power users to the simplest installation method?

I personally started to work on replacing the Windows build system with using dune and opam, so that it is more attractive for power users and makes it easier e.g. to build customized installers for courses (e.g. for the HoTT summer school I had to create a special installer including HoTT).

Great!
out of curiosity, would this kind of customized installer target items (1) and (2) above, or the opam switch is only involved during the preparation of the customized installer, and not kept in the final installation?

6

@erikmd:

I think the best way forward is to describe the WSL process in the Wiki but make it clear that the recommended and maintained method is to use the Windows Installer and that the WSL method is mostly intended for experienced system administrators who know what they are doing.

Yes it does address point (1) and (2). The goal is to have a fully fledged opam based Coq/OCaml developer environment using cygwin as “shell system” and OCaml with MinGW target. But at least for the time being I need a patched opam repo for Windows (there is already a Windows fork which is maintained). Mid term I plan to bring all the extra rules into the main opam repo. This should also address the issues of creating extended custom Windows Installers (e.g. containing additional libraries for courses).

I have a cygwin emacs patched up so that it can understand cygwin and Windows paths, which is a requirement to work with the MinGW OCaml toolchain - otherwise e.g. emcas cannot provide an executable path to ocamldebug, which ocamldebug can understand. I am currently in discussions with the cygwin emacs maintainer on this topic - there are some minor technical and philosophical issues left. I don’t like the usual Windows emacs since it installs yet another Linux abstraction layer. The other alternative would be to provide a cygwin MinGW OCaml cross toolchain, so that ocamlc, ocamldebug, … digest cygwin paths but produce MinGW executables. But this also has its trickeries and working with the MinGW tolchain under cygwin worked quite well so far. I am still experimenting with cygwin vs. MinGW builds of Merlin. As far as I can tell Merlin has little issues with paths since it mostly seems to use relative paths. Tuareg inherits the file system patches from emacs.

In case you have specific needs for your courses, e.g. provide a Coq environment with Emacs, Merlin, Tuareg on Windows, I can likely provide an automated script which sets this up (based on cygwin) which will work within a few iterations between us. Essentially I have all this running (I needed all this for the tricky CoqIDE GTK3 port debugging on Windows). But I am not proficient with Emacs, so I guess there are some issues which need to be fixed.

1 Like
7

:+1: although “experienced system administrators” might be a bit much. Students that already use WSL on their machines are just hackers who like having a Linux-style console in a graphical Windows machine.

The wiki is open to anyone to contribute and does not reflect the opinions or the methods supported by the development team. Therefore, it should be fine to add instructions to use WSL, and explicitly mention that people can improve these installation instructions if they want.

I don’t think it does. Chocolatey is just a Linux-style package manager wrapper that installs Coq using the official installer behind the scene. This is similar to what Homebrew Cask does for the CoqIDE package on macOS.

8

How about: “The WSL approach is mostly intended for those who enjoy debugging and fixing system and build issues from time to time as much as using Coq” ?

9

Still sounds too strong to me. I’d rather say, “the WSL approach is not the officially supported method, and as such, you should be ready to jump through hoops if this is the approach you choose”.

2 Likes
10

That’s a very nice formulation!

11

That’s weird, did you really intend to quote yourself?

12

Dear @MSoegtrop and @Zimmi48, thank you for your feedback!

FYI I’ve just added a new section in the wiki Installation of Coq in WSL + (VcXsrv or wsl-alias) with the following features:

  • The 4 approaches I am aware of are documented (A)-(B)-(C)-(D): the (D) approach corresponds to what I had tested and documented in French in this repo; approach (C) corresponds to the approach that @jfehrle had tested IINM, and approaches (A) and (B) rely on another dependency (X server).
  • Even if I only tested approach (D), I have put (A)-(B) in the beginning of the list as they should be simpler to setup.
  • The potential pitfalls (or simply the differences w.r.t. a regular Linux installation) are put in bold.
  • I included a disclaimer with the prose suggested by Théo.

Feel free to comment / proofread / edit.

1 Like
13

@MSoegtrop

In case you have specific needs for your courses, e.g. provide a Coq environment with Emacs, Merlin, Tuareg on Windows, I can likely provide an automated script which sets this up (based on cygwin) which will work within a few iterations between us. Essentially I have all this running (I needed all this for the tricky CoqIDE GTK3 port debugging on Windows). But I am not proficient with Emacs, so I guess there are some issues which need to be fixed.

Thanks a lot for proposing! :+1:

Indeed I’d be interested to discuss this… so let’s say I’ll come back to you when I’ll be in the course of preparing our upcoming Coq laboratory sessions :slight_smile:

14

Hi Erik,

Some thoughts:

I did © only to work on the PG code. I don’t use emacs otherwise. Indeed, I didn’t know there was GUI version of emacs until later (I hadn’t used emacs for ages). I noticed that at times the display was not updated properly, e.g. sometime the menus would go crazy.

I recently rebuilt my development environment on a new laptop with Windows/WSL/Ubuntu. I didn’t run into any big issues. I don’t recall whether I did sudo apt-install opam or something more like what you suggested. I definitely didn’t use choclatey, which I think gives you the Windows executable rather than Linux. If you’re going to do WSL, seems like you ought to use the Linux version. I probably just built Coq directly rather then doing an installation.

$ apt list |grep opam
opam/bionic 1.2.2-6 amd64
opam-docs/bionic 1.2.2-6 all

For WSL, and in particular (D), I learned that regular Windows processes must not write to WSL files, which are visible though buried in the Windows filesystem. The issue is that files have metadata that’s specific to Windows or Linux. WSL process->Windows file will work correctly but Windows process->WSL file will have problems. So for my development environment, my working directories are in /mnt/c/proj. My editor is a Windows process. It’s not clear from your description where the files emacs edits are stored.

To run things, I just type “bash” in the Windows search box to open a WSL bash window, then I can type “bin/coqtop” on the command line in my source tree. That seems simpler than the wsl-alias stuff.

The 5 section headers are a little confusing. Seems to me that 1) first choose between Windows and WSL/Linux then 2) For WSL/Linux choose between virtualized Linux and WSL. Then 3) For each of (Choclatey, virtualized Linux and WSL), decide whether to install source or binaries.

How about adding advice on which one to use at the top of the page? I would recommend using WSL as the simplest option, second choice virtualized Linux (requires more resources, perhaps more complex??), third choice Choclatey. “Installation from binaries” is Windows-specific, doesn’t cover the other two. “Installation from sources” is also Windows-only.

By the way, the next release of Windows is supposed to make WSL a full-fledged virtual machine. So the virtualized Linux info may not be needed long term.

Jim

15

Currently, I’m using Coq on Arch Linux on WSL at work. Everything has worked fine for me, except that there are some minor performance issues with WSL 1, but nothing outrageous. I expect that WSL 2 will solve them.

By far, I have found using Coq on WSL to be the most reliable way to run Coq on Windows, besides perhaps running a full-fledge Linux VM, which could be heavy weight. I have no problem using features such as native code compilation in WSL either, so IMO the Coq team should consider making WSL the recommended method, especially when WSL 2 is officially released.

I would like to recommend Arch Linux for this purpose, but it’s not officially supported by WSL so…

16

@jfehrle I think you are confused about what Chocolatey is. It is definitely not related to Linux, except it imports the Linux style of installing package. As is said in the wiki page, Chocolatey is just a way of installing Coq for Windows through the official binary installers.

@erikmd Thanks for adding this section. I would also add that installing using Nix is possible once you are in WSL: https://github.com/coq/coq/wiki/Nix.

@xuanruiqi If I’m not mistaken, activating WSL supposes to first enable a so-called “developer-mode”. I don’t think it is fair to expect that all Coq users are “developers”, especially the ones using Windows. Making this the primary supported method would not be a good sign to send, e.g., to the mathematical community.

17

If I’m not mistaken, activating WSL supposes to first enable a so-called “developer-mode”. I don’t think it is fair to expect that all Coq users are “developers”, especially the ones using Windows. Making this the primary supported method would not be a good sign to send, e.g., to the mathematical community.

AFAIK, as of the Fall 2017 update, enabling WSL does not require Developer Mode anymore (official documentation). At least I didn’t have to enable it until I wanted to install an unofficial distribution.

18

Thanks for the info! The WSL method still requires a more complex series of steps than the installer, but it seems like it could make sense to start to promote it as a reasonable alternative, especially for users who want the full power of Coq on Linux. Anyway, this addition to the wiki page is a good first step.

19

Not at all, that’s exactly what I thought when I read it.
I would revise the page to list the alternatives in the first paragraph along with when we recommend using them. I’d be happy to add such a paragraph if we agree on a recommendation. I didn’t feel I should do so without some agreement on the recommendations. I would also change the section titles for clarity and mention that Windows processes writing to Linux files is an issue.

20

For sure, feel free to go ahead and edit the page, or to post a proposition here if you want a review first.