Takafumi Saikawa (Feb 05 2021 at 07:21): Takafumi Saikawa (Feb 05 2021 at 07:21):I experienced an issue at installing math-comp 1.12.0 to my coq-8.13 environment.
More precisely, the tools and settings are:
make install fails with errors like:$ make install
/usr/local/coq-8.13-github/bin/coq_makefile -f Make -o Makefile.coq
make -f Makefile.coq --no-print-directory install
algebra.coq-nativeNmathcomp_algebra_all_algebra.cmi does not exist
algebra.coq-nativeNmathcomp_algebra_finalg.cmi does not exist
algebra.coq-nativeNmathcomp_algebra_countalg.cmi does not exist
algebra.coq-nativeNmathcomp_algebra_fraction.cmi does not exist
algebra.coq-nativeNmathcomp_algebra_intdiv.cmi does not exist
algebra.coq-nativeNmathcomp_algebra_interval.cmi does not exist
I found an issue at the definition of vo_to_obj in <coq root>/tools/CoqMakefile.in which looks like:
vo_to_obj = $(addsuffix .o,\
$(filter-out Warning: Error:,\
$(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1))))
This function turns a .vo path to that of the corresponding native-coq object file.
The path returned by coqtop with -print-mod-uid contains single backslashes, which are unfortunately trimmed at somewhere in the later stages and is not available when the path is used at make install.
As an ad hoc solution, adding a call to cygpath in CoqMakefile.in works:
vo_to_obj = $(addsuffix .o,\
$(filter-out Warning: Error:,\
$(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1) | cygpath -f -)))
But this is clearly too ad hoc. Does anyone have a better idea to cope with this issue? Or am I mistaken at compiling Coq under Cygwin?
Christian Doczkal (Feb 05 2021 at 08:02):I haven't tried myself to compile Coq using Cygwin under Windows, but IIUC this is part of what the Coq-Platform does. So unless you are planning to tinker with the sources of Coq itself, you may be better off using the scripts provided at https://github.com/coq/platform/tree/v8.13
I don't know about the specific error, maybe @Enrico Tassi or @Michael Soegtrop know more.
Enrico Tassi (Feb 05 2021 at 08:20):Yes please use the platform scripts. Also, the windows installer for Coq 8.13 includes mathcomp 1.12 precompild for you.
Enrico Tassi (Feb 05 2021 at 08:22):https://github.com/coq/coq/releases/download/V8.13.0/coq-8.13.0-installer-windows-x86_64.exe
Enrico Tassi (Feb 05 2021 at 08:26):Would you mind opening a bug about coq makefile and native objects installation on cygwin? FTR the platform does not enable yet native compute, so we did not spot the problem.
Michael Soegtrop (Feb 05 2021 at 08:54):So unless you are planning to tinker with the sources of Coq itself, you may be better off using the scripts provided at
I would say even if you do want to develop Coq, the platform scripts are an efficient way to setup a work environment on Windows. The platform scripts set up a new cygwin tailored for opam support. It has a few hacks (like a non standard main/ocaml opam database) but since it is good enough to compile Coq platform - all opam based - it should be good enough for most development work. And the whole thing is well tested - e.g. for the latest cygwin bugs (there have been a few lately).
Takafumi Saikawa (Feb 05 2021 at 11:55):Thank you for advices. I try the platform script.
@Enrico Tassi Is there a test suite for the native compiler? I am willing to check if things work well on cygwin and report it.
Enrico Tassi (Feb 05 2021 at 12:13):there are a few tests in the test suite, but in general just compiling Coq and MC as you did is a test. What failed is the install target of the Makefile.
IMO if you can run Eval native_compute in primes 4. without an error, then things are fine.
Théo Zimmermann (Feb 05 2021 at 14:13):Michael Soegtrop said:
So unless you are planning to tinker with the sources of Coq itself, you may be better off using the scripts provided at
I would say even if you do want to develop Coq, the platform scripts are an efficient way to setup a work environment on Windows. The platform scripts set up a new cygwin tailored for opam support. It has a few hacks (like a non standard main/ocaml opam database) but since it is good enough to compile Coq platform - all opam based - it should be good enough for most development work. And the whole thing is well tested - e.g. for the latest cygwin bugs (there have been a few lately).
I agree with this but I will note that for dev purposes another option is to rely on WSL.
Michael Soegtrop (Feb 05 2021 at 14:52):Yes, if you have WSL already installed it is likely the best option (you might also want to use the Coq platform scripts there to get latest opam patches).
I had some mixed experience with WSL. The newer versions rely on Hyper-V and this is rather heavy. One side effect of installing Hyper-V I experienced is that blue screen core dumps don't work any more - I got only corrupted core dumps one cannot open in a debugger. Uninstalling Hyper-V fixed that. And then you can't use any other virtualization system together with Hyper-V. Since Hyper-V runs above of Windows it is hard to use it in a similar way as VirtualBox, VMware or Simics. Also I have some (not very solid) evidence that Hyper-V constantly sucks a non negligible amount of power - even if you don't use WSL, so I wouldn't install it on a laptop without doing some before/after power measurements. Cygwin is way more light weight.
Last updated: Oct 13 2024 at 01:02 UTC