X-Recipient: archive-cygwin AT delorie DOT com
DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 967273AA942F
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cygwin.com;
	s=default; t=1620303726;
	bh=OgTefF6B/iYsiuuiznQu4XAfadVM1kgDYPbhE+iv9r4=;
	h=To:Subject:Date:References:In-Reply-To:List-Id:List-Unsubscribe:
	 List-Archive:List-Post:List-Help:List-Subscribe:From:Reply-To:
	 From;
	b=wmKSQELwMclgFD0sZuZ0aEQOYZgEdnLFM0M5Ik/0WLj0SNfQ/2qwoLwc9+gXL+NnR
	 VWdWel8WD4ZUrq0GlAAdcu1/8P2rfCGb8MZ9tP6WFXmKh72uB/bGmRm0WKtfpN/m7h
	 dsGrVVImt7xZWmG5ItfEnTgsI8ZNZgxACah9/0Wo=
X-Original-To: cygwin AT cygwin DOT com
Delivered-To: cygwin AT cygwin DOT com
DMARC-Filter: OpenDMARC Filter v1.3.2 sourceware.org 476BB388E836
To: "cygwin AT cygwin DOT com" <cygwin AT cygwin DOT com>
Subject: RE: Building Coq in Cygwin
Thread-Topic: Building Coq in Cygwin
Thread-Index: AQHXQlX6ZxJY5nrIUUahdRzBzQTlH6rWUlVQ
Date: Thu, 6 May 2021 12:22:25 +0000
Message-ID: <af76b61e3ad9472ca51e7706bf8e579e@metastack.com>
References: <1b58b800-bfa3-b203-6a5f-2d53c5685d33 AT cs DOT umass DOT edu>
 <99e025c8-e4c8-60ba-3995-dbae9c0dc967 AT gmail DOT com>
In-Reply-To: <99e025c8-e4c8-60ba-3995-dbae9c0dc967@gmail.com>
Accept-Language: en-GB, en-US
Content-Language: en-US
X-MS-Has-Attach: 
X-MS-TNEF-Correlator: 
x-originating-ip: [172.16.0.125]
MIME-Version: 1.0
X-Scanned-By: MIMEDefang 2.65 on 62.31.23.242
X-Smtpcorp-Track: 1_-d104baU1nJm.k29rXr1NZyEs2
Feedback-ID: 614951m:614951apMmpqs:614951sCPXoAq0dE
X-Report-Abuse: Please forward a copy of this message, including all headers,
 to <abuse-report AT smtp2go DOT com>
X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00, DKIMWL_WL_MED,
 DKIM_SIGNED, DKIM_VALID, DKIM_VALID_EF, HEADER_FROM_DIFFERENT_DOMAINS,
 SPF_HELO_PASS, SPF_PASS, TXREP autolearn=no autolearn_force=no version=3.4.2
X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on
 server2.sourceware.org
X-BeenThere: cygwin AT cygwin DOT com
X-Mailman-Version: 2.1.29
List-Id: General Cygwin discussions and problem reports <cygwin.cygwin.com>
List-Archive: <https://cygwin.com/pipermail/cygwin/>
List-Post: <mailto:cygwin AT cygwin DOT com>
List-Help: <mailto:cygwin-request AT cygwin DOT com?subject=help>
List-Subscribe: <https://cygwin.com/mailman/listinfo/cygwin>,
 <mailto:cygwin-request AT cygwin DOT com?subject=subscribe>
From: David Allsopp via Cygwin <cygwin AT cygwin DOT com>
Reply-To: David Allsopp <David DOT Allsopp AT cl DOT cam DOT ac DOT uk>
Content-Type: text/plain; charset="utf-8"
Sender: "Cygwin" <cygwin-bounces AT cygwin DOT com>
Content-Transfer-Encoding: 8bit
X-MIME-Autoconverted: from base64 to 8bit by delorie.com id 146CM88i023969

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

-- 
Problem reports:      https://cygwin.com/problems.html
FAQ:                  https://cygwin.com/faq/
Documentation:        https://cygwin.com/docs.html
Unsubscribe info:     https://cygwin.com/ml/#unsubscribe-simple