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 , "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> 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-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 List-Unsubscribe: , List-Archive: List-Post: List-Help: List-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" 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