Error: in file bug_01.v, could not find META.coq-core.
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
Presumably there's some missing environment variable that needs to be set (
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
Last updated: Jun 09 2023 at 08:01 UTC