Re: Building Coq in 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
RE: Building Coq in Cygwin
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' (0x40) is already occupied ... > by 'dllunix.so' (0x40) is already occupied >0 [main] ocamlrun 744 child_info_fork::abort: address space needed > by 'dllunix.so' (0x40) 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
Re: Building Coq in Cygwin
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. $ ./configure 0 [main] ocamlrun 740 child_info_fork::abort: address space needed by 'dllunix.so' (0x40) is already occupied ... by 'dllunix.so' (0x40) is already occupied 0 [main] ocamlrun 744 child_info_fork::abort: address space needed by 'dllunix.so' (0x40) 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 How we solve the reloc issue on 64 bit ? I am a bit ocalm rust -- 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
