Stream: Coq devs & plugin devs

Topic: building Coq on Windows via opam?

view this post on Zulip Jason Gross (Mar 30 2022 at 22:05):

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?

view this post on Zulip Guillaume Melquiond (Mar 31 2022 at 05:45):

This looks like an error due to the command line being way too long. Possibly fixed by https://github.com/ocaml/flexdll/pull/68

view this post on Zulip Michael Soegtrop (Mar 31 2022 at 08:16):

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.

view this post on Zulip Jason Gross (Apr 01 2022 at 00:36):

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.

view this post on Zulip Enrico Tassi (Apr 01 2022 at 06:17):

iirc ocaml-setup and the platform scripts are very similar wrt setting up ocaml.

Last updated: Apr 19 2024 at 10:02 UTC