Building Coq in Cygwin
Thu May 6 12:22:25 GMT 2021
Marco Atzeri wrote:
> On 06.05.2021 02:56, Eliot Moss wrote:
> > Folks - Before I try to Coq mailing lists, I am wondering if anyone
> > here has had success building Coq under Cygwin. I've tried the dune
> > and the make approaches, and both fail, in different ways, but
> > seemingly because some components can't deal with the uniquenesses of
> > Cygwin - though they seem to try to provide for it.
> > Regards - Eliot
> another of those software that thinks Automake/cmake are non needed ...
> usually they are a mess to port to un-forecasted platforms.
This has nothing to do with the build systems of these packages and
everything to do with the fact the ocaml on Cygwin64 has been broken for a while...
> $ ./configure
> 0 [main] ocamlrun 740 child_info_fork::abort: address space needed
> by 'dllunix.so' (0x400000) is already occupied ...
> by 'dllunix.so' (0x400000) is already occupied
> 0 [main] ocamlrun 744 child_info_fork::abort: address space needed
> by 'dllunix.so' (0x400000) is already occupied I can not automatically
> find the name of your architecture.
> Give me a name, please [win32 for Win95, Win98 or WinNT]:
> ^^ frontline technology I see
:) Amusingly, the git history shows it has been preserved through updates 13 and 8 years ago,
but the line was originally written in 1999. Mature and (formally) proven is possibly the
description the Coq team might prefer!
> How we solve the reloc issue on 64 bit ? I am a bit ocalm rust
I fixed the underlying problem in OCaml 4.12, but I haven't had time to propose
adopting the Cygwin packages yet - I'm hoping to over the next few months.
The short-term workaround is either to use Cygwin32 or to install the opam, libgmp-devel and
flexdll 0.39 packages and run:
opam switch -y create coq ocaml-base-compiler.4.12.0
# This takes a looong time, especially the "make install" step
opam install -y coq
eval $(opam env)
(NB flexdll 0.39 must be selected manually or using the new flexdll=0.39-1 syntax on the command line,
as I've left it marked test until ocaml 4.12 is packaged)
More information about the Cygwin