Using CoqIDE on Windows. · Coq users

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).

Huỳnh Trần Khanh (Feb 07 2024 at 07:45):

looks like you need cygwin

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

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.

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:

Extending on what @Julio Di Egidio wrote: for simple cases just write a batch file to call coqc for the files you need. As long as your compile time is less than a few seconds, it is hardly worth the effort to get make on Windows. If you approach a minute, it is worthwhile to have make
This release https://github.com/coq/platform/releases/tag/2023.03.0 contains an asset which is gnu make plus a patch to coq makefile which makes coq makefile generated make files compatible with both, posix and CMD shell. It does not support all make targets created by coq makefile - I hacked it together for a lecture.
Use the Coq Platform scripts to install Coq Platform, then you get a fully fledged development environment (based on cygwin) - this is the same environment in which the Coq installers are built.

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

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?

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

Julio Di Egidio (Feb 07 2024 at 17:29):

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

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.

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.

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.

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

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.

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

Paolo Giarrusso (Feb 07 2024 at 20:40):

Docs hint at a cygwin terminal icon

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

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)

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.

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.

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'.

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).

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.

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.

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: Oct 13 2024 at 01:02 UTC

Stream: Coq users

Topic: Using CoqIDE on Windows.

Ariel (Feb 06 2024 at 22:22):