What does
Error: in file bug_01.v, could not find META.coq-core.
mean?
How did it happen?
I need to be able to access two artifacts from Coq's CI simultaneously, so I stick one of the artifacts in /github/workspace/builds/coq/coq-failing/
and the other in /github/workspace/builds/coq/coq-passing/
Presumably there's some missing environment variable that needs to be set (PATH
? OCAMLPATH
? COQLIB
? COQCORELIB
? OCAMLFIND_CONF
? Something else?), but I'm not aware of anywhere that documents which variables need to be set to get a working coq environment...
I've made a bug report at https://github.com/coq/coq/issues/17158
Oh, ew, is Declare ML Module "coq-core.plugins.ltac".
no longer something that I can just dump in a file loaded with -nois
to get Ltac support?
Hm, but, no, it still seems to work fine in the bug minimizer test-suite
Looking for the META is probably a findlib error so my money is on OCAMLPATH or OCAMLFIND_CONF not being set correctly.
This is not a findlib error but in tools/coqdep/lib/fl.ml
Last updated: Oct 13 2024 at 01:02 UTC