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>
Content-Language: en-US
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
Precedence: list
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
Content-Transfer-Encoding: 7bit
Content-Type: text/plain; charset="us-ascii"; Format="flowed"
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