Building Coq in Cygwin

Building Coq in Cygwin

[Eliot Moss]

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

Re: Building Coq in Cygwin

[Marco Atzeri]

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.

$ ./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


How we solve the reloc issue on 64 bit ? I am a bit ocalm rust

RE: Building Coq in Cygwin

[David Allsopp]

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

Re: Building Coq in Cygwin

[Eliot Moss]

On 5/6/2021 8:22 AM, David Allsopp via Cygwin wrote:

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

Thank you, David, that worked great!  I was able then to go on and process a
Coq library I was interested in, and it went through with no problems.  I
appreciate the help!

Best wishes - Eliot