Jason Gross (Apr 26 2022 at 11:26): Jason Gross (Apr 26 2022 at 11:26):What's up with Coq 8.14 on Windows failing at https://github.com/mit-plv/fiat-crypto/runs/6135821728?check_suite_focus=true ?
# DUNE _build/default/plugins/firstorder/firstorder_plugin.cmxs
# File "plugins/cc/dune", line 1, characters 0-143:
# 1 | (library
# 2 | (name cc_plugin)
# 3 | (public_name coq-core.plugins.cc)
# 4 | (synopsis "Coq's congruence closure plugin")
# 5 | (libraries coq-core.plugins.ltac))
# (cd _build/default && D:\a\fiat-crypto\fiat-crypto\_opam\bin\ocamlopt.opt.exe -w -40 -rectypes -g -O3 -unbox-closures -shared -linkall -I plugins/cc -o plugins/cc/cc_plugin.cmxs plugins/cc/cc_plugin.cmxa)
# ** Fatal error: Cannot find file "dllcrt2.o"
# File "caml_startup", line 1:
# Error: Error during linking (exit code 2)
# make[1]: *** [Makefile.common:144: _build/default/plugins/cc/cc_plugin.cmxs] Error 1
# make[1]: *** Waiting for unfinished jobs....
# make[1]: Leaving directory '/cygdrive/d/a/fiat-crypto/fiat-crypto/_opam/.opam-switch/build/coq.8.14.1'
# make: *** [Makefile.make:122: submake] Error 2
"CRT" usually stands for "C runtime"; Google suggests it's from Mingw's C runtime...
Michael Soegtrop (Apr 26 2022 at 11:34):Is this Coq Platform script/installer or another install method?
Michael Soegtrop (Apr 26 2022 at 11:35):The Coq Platform installer includes quite a few MinGW shared libraries - I hope I didn't forget any. When you use scripts + cygwin these should be there automatically, but you have to have a proper path which includes the MinGW system root.
Jason Gross (Apr 29 2022 at 10:26):I'm using the opam/ocaml GitHub action and doing opam install coq
Michael Soegtrop (Apr 29 2022 at 11:53):Sorry, I can't say much about the github action. I guess I should put it on my ToDo list to do a Coq Platform github action.
Last updated: Oct 12 2024 at 11:01 UTC