It seems that Coq fails to build on Windows via opam because
[ERROR] The compilation of zarith failed at "D:\\cygwin\\bin\\make.exe".
-> installed dune.3.0.3
#=== ERROR while compiling zarith.1.12 ========================================#
# context 2.0.10 | win32/x86_64 | ocaml-variants.4.11.1+mingw64c | git+https://github.com/fdopen/opam-repository-mingw.git#opam2
# path D:/a/fiat-crypto/fiat-crypto/_opam/.opam-switch/build/zarith.1.12
# command D:\cygwin\bin\make.exe
# exit-code 2
# env-file D:/.opam/log/zarith-1600-548b09.env
# output-file D:/.opam/log/zarith-1600-548b09.out
### output ###
# (echo "let"; grep "version" META | head -1) > zarith_version.ml
# ocamldep -native zarith_version.ml z.ml q.ml big_int_Z.ml z.mli q.mli big_int_Z.mli > depend
# ocamlc -I +compiler-libs -bin-annot -c zarith_version.ml
# ocamlc -I +compiler-libs -bin-annot -c z.mli
# ocamlc -I +compiler-libs -bin-annot -c z.ml
# ocamlc -I +compiler-libs -bin-annot -c q.mli
# ocamlc -I +compiler-libs -bin-annot -c q.ml
# ocamlc -I +compiler-libs -bin-annot -c big_int_Z.mli
# ocamlc -I +compiler-libs -bin-annot -c big_int_Z.ml
# ocamlmklib -failsafe -o zarith zarith_version.cmo z.cmo q.cmo big_int_Z.cmo -lgmp
# ocamlc -ccopt "-ID:/a/fiat-crypto/fiat-crypto/_opam/lib/ocaml -DHAS_GMP " -c caml_z.c
# ocamlmklib -failsafe -o zarith caml_z.o -lgmp
# ocamlc -I +compiler-libs -bin-annot -c zarith_top.ml
# ocamlc -o zarith_top.cma -a zarith_top.cmo
# ocamlopt -I +compiler-libs -c zarith_version.ml
# ocamlopt -I +compiler-libs -c z.ml
# ocamlopt -I +compiler-libs -c q.ml
# ocamlopt -I +compiler-libs -c big_int_Z.ml
# ocamlmklib -failsafe -o zarith zarith_version.cmx z.cmx q.cmx big_int_Z.cmx -lgmp
# ocamlopt -shared -o zarith.cmxs -I . zarith.cmxa -linkall
# ** Fatal error: Cannot run cygpath -m "libuser32" "libuser32.lib" "libuser32.dll.a" "libuser32.a" "D:/a/fiat-crypto/fiat-crypto/_opam/lib/ocaml\libuser32" "D:/a/fiat-crypto/fiat-crypto/_opam/lib/ocaml\libuser32.lib" "D:/a/fiat-crypto/fiat-crypto/_opam/lib/ocaml\libuser32.dll.a" "D:/a/fiat-crypto/fiat-crypto/_opam/lib/ocaml\libuser32.a" ".\libuser32" ".\libuser32.lib" ".\libuser32.dll.a" ".\libuser32.a" "D:/a/fiat-crypto/fiat-crypto/_opam/lib/ocaml\flexdll\libuser32" "D:/a/fiat-crypto/fiat-crypto/_opam/lib/ocaml\flexdll\libuser32.lib" "D:/a/fiat-crypto/fiat-crypto/_opam/lib/ocaml\flexdll\libuser32.dll.a" "D:/a/fiat-crypto/fiat-crypto/_opam/lib/ocaml\flexdll\libuser32.a" "/usr/lib/gcc/x86_64-w64-mingw32/11/libuser32" "/usr/lib/gcc/x86_64-w64-mingw32/11/libuser32.lib" "/usr/lib/gcc/x86_64-w64-mingw32/11/libuser32.dll.a" "/usr/lib/gcc/x86_64-w64-mingw32/11/libuser32.a" "/usr/x86_64-w64-mingw32/lib/x86_64-w64-mingw32/11/libuser32" "/usr/x86_64-w64-mingw32/lib/x86_64-w64-mingw32/11/libuser32.lib" "/usr/x86_64-w64-mingw32/lib/x86_64-w64-mingw32/11/libuser32.dll.a" "/usr/x86_64-w64-mingw32/lib/x86_64-w64-mingw32/11/libuser32.a" "/usr/x86_64-w64-mingw32/lib/libuser32" "/usr/x86_64-w64-mingw32/lib/libuser32.lib" "/usr/x86_64-w64-mingw32/lib/libuser32.dll.a" "/usr/x86_64-w64-mingw32/lib/libuser32.a" "/usr/x86_64-w64-mingw32/sys-root/mingw/lib/x86_64-w64-mingw32/11/libuser32" "/usr/x86_64-w64-mingw32/sys-root/mingw/lib/x86_64-w64-mingw32/11/libuser32.lib" "/usr/x86_64-w64-mingw32/sys-root/mingw/lib/x86_64-w64-mingw32/11/libuser32.dll.a" "/usr/x86_64-w64-mingw32/sys-root/mingw/lib/x86_64-w64-mingw32/11/libuser32.a" "/usr/x86_64-w64-mingw32/sys-root/mingw/lib/libuser32" "/usr/x86_64-w64-mingw32/sys-root/mingw/lib/libuser32.lib" "/usr/x86_64-w64-mingw32/sys-root/mingw/lib/libuser32.dll.a" "/usr/x86_64-w64-mingw32/sys-root/mingw/lib/libuser32.a"
# File "caml_startup", line 1:
# Error: Error during linking (exit code 2)
# make: *** [project.mak:80: zarith.cmxs] Error 2
https://github.com/mit-plv/fiat-crypto/runs/5761380206?check_suite_focus=true
Any ideas for fixing this?
This looks like an error due to the command line being way too long. Possibly fixed by https://github.com/ocaml/flexdll/pull/68
You might need what Coq Platform does here:
https://github.com/coq/platform/blob/a3337168563a1835a022caa616c477f89ec23280/windows/configure_profile.sh#L31
https://github.com/coq/platform/blob/a3337168563a1835a022caa616c477f89ec23280/windows/configure_profile.sh#L35
Depending on what your PATH is, keeping it + OLDPATH (which is set by cygwin) might blow the environment beyond the limits on Windows and then strange things happen. It definitely works with Coq Platform.
Btw.: is there a good reason why you don't use the Coq Platform scripts to setup cygwin? You can install just Coq with Coq Platform and install all the rest manually with opam if you want.
Thanks, I will try reducing PATH if this error keeps happening.
Btw.: is there a good reason why you don't use the Coq Platform scripts to setup cygwin? You can install just Coq with Coq Platform and install all the rest manually with opam if you want.
If you have a suggestion for simplifying https://github.com/mit-plv/fiat-crypto/blob/master/.github/workflows/coq-windows.yml with the Coq Platform, I'd be happy to use it, but for https://github.com/mit-plv/fiat-crypto/blob/master/.github/workflows/coq-opam-package.yml I'm actually using exactly the same script on Windows, Mac, and Linux, and just relying on the ocaml/setup-ocaml@v2 action to set up opam for me on the relevant platform.
iirc ocaml-setup and the platform scripts are very similar wrt setting up ocaml.
Last updated: Oct 13 2024 at 01:02 UTC