Stream: Coq users

Topic: Using CoqIDE on Windows.


view this post on Zulip Ariel (Feb 06 2024 at 22:22):

Hello.

When using CoqIDE on Windows I'm tryinig to use the "make" commands without any arguments in order to compile all the files (I can tell thats the reason why the program isn't running because the files don't have their respective .vo files). But when I do it, I get an error.

make_screenshot.png

Does anyone know how to solve this? Any other methods for compilation or even a suggestion for an easier platform on windows than CoqIDE would be great. I tried already to compile it from CoqIDE It self instead of the cmd, but it doesn't seem to work whenever the file is dependent on other files which haven't been compiled yet (Theoretically it could be possible to compile everything manually this way but it's just way too much work).

view this post on Zulip Huỳnh Trần Khanh (Feb 07 2024 at 07:45):

looks like you need cygwin

view this post on Zulip Huỳnh Trần Khanh (Feb 07 2024 at 07:48):

and no even if you switch to vscoq coq-lsp proof general coqtail whatever you'll still encounter the same problem. you need cygwin

view this post on Zulip Julio Di Egidio (Feb 07 2024 at 12:46):

Yes, there is no make on Windows, so you'd need WSL or Cygwin, though both come with their own cost.

Otherwise indeed coqc and the other command-line tools work: yes, you'd have to compile the individual files and in the right order (on the command line or via CoqIDE, etc.), but you can also write your own script (some .bat file) that compiles things in the right order.

Just compiling the individual files is fine for some study (which is progressive anyway) or small projects. It is painful/unsustainable for large projects, and does not cover compiling external libraries or extensions that need more than just coqc to build.

view this post on Zulip Michael Soegtrop (Feb 07 2024 at 13:41):

@Ariel : the issue is not make, but that most make files require a posix shell, and this is hard to get on Windows. Originally I did ship make with Coq Platform, but it used CMD as shell and people complained that it would hide their "properly working" cygwin supplied make.

The options you have are:

Note that from the various methods to get make and a bash on Windows, cygwin has proven to be the most reliable one.

view this post on Zulip Huỳnh Trần Khanh (Feb 07 2024 at 16:55):

hot take: make based workflow should be yeeted asap to make way for a proper build system... wait we have dune right? how usable is it now?

view this post on Zulip Julio Di Egidio (Feb 07 2024 at 17:02):

Not ready for Windows, not until opam 2.2 if I read the following correctly:
https://dune.build/install
https://opam.ocaml.org/doc/Install.html#Windows

view this post on Zulip Julio Di Egidio (Feb 07 2024 at 17:29):

P.S. +2 for that feature, eventually up to dynamic compilation "first-class".

view this post on Zulip Michael Soegtrop (Feb 07 2024 at 17:38):

The fact that "opam for Windows" has been promised "in the next release" since a while is one of the reasons I didn't put too much effort into Windows using the current work arounds.

@Huỳnh Trần Khanh : dune is included in the Coq Platform Windows binary installer - I didn't test it much, though, since I am not yet using dune. Feedback is welcome.

view this post on Zulip Ariel (Feb 07 2024 at 18:32):

I tried installing cygwin and it didn't anything.
@Michael Soegtrop I tried your link I'm still getting the same error.
the project is too much to compile manually file by file, even if i finished it and it somehow worked I'm expected to deal with more projects like that in the future and it would be way too much to do that to all of them.
I have have no first clue about how to write a batch file.

view this post on Zulip Michael Soegtrop (Feb 07 2024 at 19:06):

@Ariel: if you work with larger Coq projects, you should install Coq Platform via the scripts from sources. You get opam, make, ... this way. See the docs. Note that the script will install cygwin for you with everything needed. A default cygwin lacks some things we need.

view this post on Zulip Ariel (Feb 07 2024 at 19:21):

@Michael Soegtrop I installed Coq Platform as you suggested. I am getting a different error now when I try to run make

make_error.png

view this post on Zulip Paolo Giarrusso (Feb 07 2024 at 20:34):

That make seems to be using the windows shell instead of bash. I seem to remember to use cygwin you need a terminal with a different configuration.

view this post on Zulip Paolo Giarrusso (Feb 07 2024 at 20:36):

sorry this is vague, but I'm hoping the cygwin docs or somebody else can fill in the blanks

view this post on Zulip Paolo Giarrusso (Feb 07 2024 at 20:40):

Docs hint at a cygwin terminal icon

view this post on Zulip Paolo Giarrusso (Feb 07 2024 at 20:43):

That is: try to find and double-click such an icon, go to the right folder and run make from there. The shell is bash so it'll be a bit different, but the cd command is similar

view this post on Zulip Paolo Giarrusso (Feb 07 2024 at 20:47):

While Michael patched coq_makefile to avoid this step, that doesn't extend to all existing makefiles for coq projects. (Software foundations seems to be using a hand-written wrapper)

view this post on Zulip Julio Di Egidio (Feb 08 2024 at 09:44):

make does not exist on Windows, and installing a POSIX shell is easy (even Git for Windows ships with one), still won't give you make.

view this post on Zulip Julio Di Egidio (Feb 08 2024 at 09:49):

@Ariel

I have have no first clue about how to write a batch file.

I'll put together an example, this seems of general interest: hopefully by close of play today.

view this post on Zulip Michael Soegtrop (Feb 08 2024 at 09:51):

@Ariel : the Coq Platform Windows scripts installed a cygwin in some folder (it asked you where). In that folder you find a cygwin.bat file. You need to start a shell via this one. It is a fully fledged Coq dev environment. Note that cygwin's file system root is where it is installed, but you can do a cd 'C:\xyz'.

view this post on Zulip Michael Soegtrop (Feb 08 2024 at 09:58):

@Julio Di Egidio : as mentioned above you can find a working stand alone Windows make here : https://github.com/coq/platform/releases/download/2023.03.0/AddOn_gnumake_win64.zip. It can work with CMD, or if you have it, a posix shell. And yes, one can install a posix shell on Windows - the most common way is cygwin and things like "Git for Windows" are essentially a cygwin clone (via MSys2) with a more straight forward but less flexible installer. The reason I prefer cygwin over MSys2 derivates like "Git for Windows" is that it reliably can handle complicated build scripts based on automake. Most opam packages compile out of the box with cygwin. It is not really what I want, but it gets the job done until we have something better (native opam and dune).

view this post on Zulip Julio Di Egidio (Feb 08 2024 at 10:04):

Besides that you know it doesn't fully close the circle (let's hope post opam 2.2 we can do better), but even disregarding that, what you describe cannot get the job done with a user who does not even know what a .bat file is: which is the majority of Windows users... IOW, we are not replying to the same question.

view this post on Zulip Michael Soegtrop (Feb 08 2024 at 10:42):

Julio Di Egidio : indeed the majority of Windows users doesn't know what a .bat file is. But I have doubts that this is true for the intersection of the sets of "Coq Users" and "Windows Users". Anyway for the first contact with Coq (and only this) we have the binary installers. If you went through however far this gets you, it is reasonable to expect from users to learn a few basics.

Regarding it doesn't fully close the circle: I still don't quite understand what you mean by this. The Coq Platform Windows shell can install almost all relevant opam packages just with opam install <package>. The packages in Coq Platform extended for which this is not true are coq-hammer and coq-fiat-crypto (prerequisites work). For both packages there are good reason why this is so, which have nothing to do with the build system. For coq-hammer the reason is that it makes massive use of fork, and this simply doesn't work on Windows. For fiat-crypto we get stack overflows in coqc (this is something one might be able to fix - just didn't find anyone up to now to want it on Windows).

If you are aware of any packages which are generally useful and can't be installed in a Coq Platform cygwin shell with opam install, please list them, and I can have a look.

If your argument is more like "anything involving any kind of command line stuff is unsuitable" my argument is that if you want to work with coq, some day you have to learn what the command line is. No however fancy install system will save you from that.

view this post on Zulip Paolo Giarrusso (Feb 08 2024 at 18:21):

I think some mathematicians want to use tools like Coq without understanding this kind of tooling. I can sympathetize, but my sympathy won't magic a fix


Last updated: Jun 13 2024 at 19:02 UTC