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
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>
Sender:	"Cygwin" <cygwin-bounces AT cygwin DOT com>
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

- Raw text -