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.
Yes I was aware of that limitation, and you’re right that it should be mentioned in the wiki (probably at the end of item (D))… so I propose adding the following sentence, borrowing in part what you suggested:
“”“Note that a current limitation of WSL is that regular Windows processes must not write to WSL files (which are visible though buried in the Windows filesystem). This approach (D) is thus intended to edit Coq project files stored in the Windows filesystem using Windows Emacs, which itself processes proofs in the background by relying on the WSL Coq binaries.”“”
To run things, I just type “bash” in the Windows search box to open a WSL bash window,
Yes, that corresponds to the step “2. Open a WSL terminal”… but indeed that sentence could be slightly extended, mentioning the Windows search box, feel free to edit the wiki page accordingly!
then I can type “bin/coqtop” on the command line in my source tree. That seems simpler than the wsl-alias stuff.
I am not sure to follow your remark because:
Using bin/coqtop in WSL just corresponds to approach (C) and is already documented;
If the question consists in: is wsl-alias really required for approach (D)? then the answer is yes, to be able to translate the Windows filesystem paths to the Coq binary
Finally if you suggest that using coqtop is simpler, I’m unsure it will scale with large proofs
But given your remark, one could maybe want to add a sentence in “approach (C)” like this?
“”“This approach also permits running coqtop directly in WSL (or through a CLI wrapper such as rlwrap).”“”
The main users for “the recommended method” are students attending Coq courses. There is experimental evidence that the amount of effort needed by tutors to help attendees getting Coq installed is extremely low with the Windows Coq Installer. This time is already substantially larger with plain main Linux distros (Ubuntu …) and it is not unheard of that attendees don’t manage to get Coq installed on plain Linux even with substantial help from tutors. I would expect that the time and effort to get Coq installed on WSL on Windows is larger than the time needed to install Coq on plain Linux.
I completely agree that for researchers using Coq ease / speed / reliability of installation is much less important than other factors and I also agree that the Coq Windows installer has issues which are not acceptable for advanced users. But the main goal of such recommendations is to give beginners an easy start with Coq. If someone has spent a few 100 hours with Coq and reaches the limits of the Windows Installer version (s)he likely has seen the other options at colleague’s computers and is willing to spend a few hours to explore such options. But for beginners and course attendants installation should be fast and reliable and not require any system administration knowledge.
Aside: Discourse seems like the wrong tool for copyediting. The regular GitHub review process would be better (and we’re all very familiar with it).
“Note that a current limitation of WSL is that regular Windows processes must not write to WSL files (which are visible though buried in the Windows filesystem). This approach (D) is thus intended to edit Coq project files stored in the Windows filesystem using Windows Emacs, which itself processes proofs in the background by relying on the WSL Coq binaries.”
The restriction is relevant to all 4 options A-D. Putting the editable files in Windows is the safest practice in case you ever edit them with a Windows process. I initially put my files in the WSL area. That didn’t work well. I ended up deleting everything and starting fresh. (For my development environment my source tree is in Windows as are the WSL binaries that it builds. I compile and run the binaries from a WSL bash terminal, but so far without CoqIDE.)
I guess wsl-alias is to start a WSL process from a Windows process, so ignore my earlier comment about bin/coqtop. I think we should remove (C) unless someone figures out how to get it to work well. The menus were an awful mess. No user should have deal with that. Character mode is a throwback to ancient technology.
These are useful only for developers, right? So not needed here
b wsl-alias add ocaml "opam exec -- ocaml"
b wsl-alias add ocamlc "opam exec -- ocamlc"
b wsl-alias add ocamlmerlin "opam exec -- ocamlmerlin"
@MSoegtrop how do I get the gtk file needed to build CoqIDE on Linux/Ubuntu? The following doesn’t work yet:
$ sudo apt-get install liblablgtksourceview3-ocaml-dev
Reading package lists... Done
Building dependency tree
Reading state information... Done
E: Unable to locate package liblablgtksourceview3-ocaml-dev
I still intend to update the beginning of the document.
Also, what about using OPAM for installing packages for Coq? Is that an important consideration for students in classes? Currently it’s pretty much impossible to install 64 bit OPAM 2.0 directly on Windows. And 32 bit OPAM 2.0 may require disabling the sandboxing option.
@Zimmi48 I’m having trouble building coqide with the makefile under WSL/Ubuntu. When I run ./configure, it says “native CoqIde will be built” and “CoqIde : opt” but a full build doesn’t create a bin/coqide. All I get in bin with that prefix are bin/coqidetop and bin/coqidetop.opt.
(I was able to install lablgtk3 with OCaml 4.06, so I think the “opam switch create 4.05.0” is just the minimum version required. Right?)
PS I added several paragraphs at the beginning describing the alternatives plus I edited parts of the current text (rewording, moving, deleting redundant info). Please take a look when you have a chance and let me know if it’s OK.
I moved Choclatey to the end. I was tempted to delete it entirely. It seemed like a bit of spam advertising to put it first on the page: I’ve not heard any Coq folk mention it, the person who added it to the page is unknown (at least to me). Also Choclately appears to be a for-profit operation (see https://chocolatey.org/pricing).
(BTW, Discourse won’t let me add a 4th new comment in a row. That seems pretty lame.)
That’s weird. But it has been a long time since I haven’t built CoqIDE that way. Have you tried building with Dune?
Right.
Great intro!
I’ve moved Chocolatey in the section about binaries, while giving it less of an “alternative install method” status. The place where you had put it was mostly equivalent to removing it from the page. The fact that we don’t know the person who contributed this installation method doesn’t matter. The wiki is free for anyone to edit. Besides, I’d really like to encourage anyone doing a good job at packaging Coq and keeping the package up-to-date. That’s why I have put the Chocolatey badge in the README a while ago (actually four months before it was added to the Windows page on the wiki): Add badges linking to a selection of up-to-date Coq packages. by Zimmi48 · Pull Request #9340 · coq/coq · GitHub. Chocolatey may be for-profit (but does it matter? npm, the most popular package manager is for-profit as well) but the person doing the actual work of packaging Coq is certainly not paid for this.
I have nothing to do with it (let alone use Windows), but it’s definitely not some random spam. Chocolatey is pretty well-known way to install packages. (Case in point: you would get it pre-installed on Travis & CircleCI Windows VMs.)
That’s weird. But it has been a long time since I haven’t built CoqIDE that way. Have you tried building with Dune?
On a freshly cloned git repository, I get the following error on the very first step:
$ dune build
Error: Conflict between the following libraries:
- "coq.stm" in _build/default/stm
- "coq.stm" in /home/jfehrle/.opam/4.06.0/lib/coq/stm
-> required by library "coq.plugins.ltac" in
/home/jfehrle/.opam/4.06.0/lib/coq/plugins/ltac
Earlier, I used OPAM to install Coq 8.9.1.
Any ideas on a workaround?
But not urgent; I somehow managed to build coqide with make without really trying and then ran it in Xwindows for the first time.
@herbelin IIRC I got around the confusing messages ( “native CoqIde will be built” and “CoqIde : opt” but a full build doesn’t create a bin/coqide) by installing the appropriate gtk libraries in opam. Then I ran into the “Conflict between the following libraries” problem which I haven’t tried to resolve. It’s no longer urgent for me, but would be good to fix if possible (instead of having to create a new switch).
In theory, with OCaml being improved for Windows platforms, and opam too, Coq switch to Dune and getting rid of the shellscripts might the truly native Windows port become true, without the need of WSL, Cygwin or MinGW (and various X server fake implementations). GTK3 can be built with MSVC for example, so even CoqIDE should work smoothly. Hopefully that day will come soon.
vscode is not documented here. I would imagine that it could simplify installation. Any experiences?
I’m currently helping a student and we are fighting GTK on Windows ;-(
