OCaml says this is not Cygwin

[RalfJung]

According to Sys.os_type of the ocaml installed by this, the environment is "Win32" and not "Cygwin". That affects e.g. Coq compiled via opam as it fails to detect that it runs in a Cygwin environment, see https://coq.inria.fr/bugs/show_bug.cgi?id=5782.

I am actually confused myself here, because the website and the repository and the opam switch all contain "mingw" in their name, but the website also says that it sets up cygwin and the environment I get is definitely a Cygwin environment. What is going on here?

[fdopen]

Build system and target system differ. The build system of many packages (including basic packages such as ocamlfind, ocamlbuild, camlp5) require common posix tools: bash, gnu make, m4, ... They are usually not available as native windows programs (or with too many features missing). Therefore cygwin is necessary at build time. The compiled programs however are native windows program, they don't depend on cygwin. Additionally opam imposes conventions how and where programs are installed. And this conventions mirror the conventions known from Unix, not Windows.

If your program can't deal with this conventions, you can install just the dependencies with opam (opam install --deps-only coq) and then compile your program manually and install it outside the opam directories.

[RalfJung]

If your program can't deal with this conventions, you can install just the dependencies with opam (opam install --deps-only coq) and then compile your program manually and install it outside the opam directories.

That doesn't really help though; what I want to achieve is tell people to use opam to install (the build dependencies for) our project, and that project depends on Coq. The final artifact is not a binary but some proofs being checked, so in the end it doesn't matter whether some binaries used in the process depend on Cygwin or not.

The compiled programs however are native windows program, they don't depend on cygwin.

Wow, so this is some form of cross-compilation. Impressive. I didn't know that was possible. I suppose there's no way to switch things around such that everything is Cygwin-based? (That may involve using an entirely different "opam on Windows" solution; the reason I am here is because this is the only option I found to use opam on Windows.)

[fdopen]

There is a cygwin version of opam/ocaml. You can install both through cygwin's setup-*.exe: https://cygwin.com/ However, the cygwin version of OCaml is in rather bad shape. It's slower and until recently it often couldn't be use because of the license restrictions implied by cygwin. But it might work good enough for your use case.

Anyway, coq 8.7.0 is now officially released and can be installed through this repo. For whatever reason it was necessary to specify the libdir path manually on Windows: https://github.com/fdopen/opam-repository-mingw/commit/ae60216cf16fe59e4b8138e67169e093496fbd30#diff-524e3aff1c58bee5240dfd0a0c3b0a97 I hope it works as intended ...

[RalfJung]

For whatever reason it was necessary to specify the libdir path manually on Windows: ae60216#diff-524e3aff1c58bee5240dfd0a0c3b0a97 I hope it works as intended ...

Thanks! I submitted a similar fix upstream but not in time for 8.7.0: https://github.com/coq/opam-coq-archive/pull/203