X-Recipient:	archive-cygwin AT delorie DOT com
X-Original-To:	cygwin AT cygwin DOT com
Delivered-To:	cygwin AT cygwin DOT com
DMARC-Filter:	OpenDMARC Filter v1.3.2 sourceware.org E9BD63AA982C
Authentication-Results:	sourceware.org;
	dmarc=none (p=none dis=none) header.from=cs.umass.edu
Authentication-Results:	sourceware.org;
	spf=pass smtp.mailfrom=moss AT cs DOT umass DOT edu
Subject:	Re: Building Coq in Cygwin
To:	David Allsopp <David DOT Allsopp AT cl DOT cam DOT ac DOT uk>,
	"cygwin AT cygwin DOT com" <cygwin AT cygwin DOT com>
References:	<1b58b800-bfa3-b203-6a5f-2d53c5685d33 AT cs DOT umass DOT edu>
	<99e025c8-e4c8-60ba-3995-dbae9c0dc967 AT gmail DOT com>
	<af76b61e3ad9472ca51e7706bf8e579e AT metastack DOT com>
From:	Eliot Moss <moss AT cs DOT umass DOT edu>
Message-ID:	<9a0f5141-e1c9-efa7-0e59-3107d44390f4@cs.umass.edu>
Date:	Thu, 6 May 2021 10:00:26 -0400
User-Agent:	Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:68.0) Gecko/20100101
	Thunderbird/68.12.1
MIME-Version:	1.0
In-Reply-To:	<af76b61e3ad9472ca51e7706bf8e579e@metastack.com>
X-Spam-Status:	No, score=-2.4 required=5.0 tests=BAYES_00, KAM_DMARC_STATUS,
	NICE_REPLY_A, RCVD_IN_DNSWL_LOW, SPF_HELO_NONE, SPF_PASS,
	TXREP autolearn=ham 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-Unsubscribe:	<https://cygwin.com/mailman/options/cygwin>,
	<mailto:cygwin-request AT cygwin DOT com?subject=unsubscribe>
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>
Reply-To:	moss AT cs DOT umass DOT edu
Errors-To:	cygwin-bounces AT cygwin DOT com
Sender:	"Cygwin" <cygwin-bounces AT cygwin DOT com>

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

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