From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mailsrv.cs.umass.edu (mailsrv.cs.umass.edu [128.119.240.136]) by sourceware.org (Postfix) with ESMTPS id E9BD63AA982C for ; Thu, 6 May 2021 14:00:27 +0000 (GMT) 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@cs.umass.edu Received: from [192.168.50.218] (c-24-62-201-179.hsd1.ma.comcast.net [24.62.201.179]) by mailsrv.cs.umass.edu (Postfix) with ESMTPSA id 73AC5401CE27; Thu, 6 May 2021 10:00:25 -0400 (EDT) Reply-To: moss@cs.umass.edu Subject: Re: Building Coq in Cygwin To: David Allsopp , "cygwin@cygwin.com" References: <1b58b800-bfa3-b203-6a5f-2d53c5685d33@cs.umass.edu> <99e025c8-e4c8-60ba-3995-dbae9c0dc967@gmail.com> From: Eliot Moss 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: Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: 7bit 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@cygwin.com X-Mailman-Version: 2.1.29 Precedence: list List-Id: General Cygwin discussions and problem reports List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 06 May 2021 14:00:38 -0000 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