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: *** [Makefile.common:144: _build/default/plugins/cc/cc_plugin.cmxs] Error 1 # make: *** Waiting for unfinished jobs.... # make: 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...
Is this Coq Platform script/installer or another install method?
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.
I'm using the opam/ocaml GitHub action and doing
opam install coq
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: Feb 05 2023 at 21:03 UTC