RE: Building Coq in Cygwin

[David Allsopp <David.Allsopp@cl.cam.ac.uk>]

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 init
  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)
  coqtop
  Quit.

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

HTH,


David