Stream: Coq devs & plugin devs

Topic: could not find META.coq-core


view this post on Zulip Jason Gross (Jan 25 2023 at 01:51):

What does

Error: in file bug_01.v, could not find META.coq-core.

mean?

view this post on Zulip Ali Caglayan (Jan 25 2023 at 02:04):

How did it happen?

view this post on Zulip Jason Gross (Jan 25 2023 at 02:11):

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/

view this post on Zulip Jason Gross (Jan 25 2023 at 02:13):

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...

view this post on Zulip Jason Gross (Jan 25 2023 at 02:19):

I've made a bug report at https://github.com/coq/coq/issues/17158

view this post on Zulip Jason Gross (Jan 25 2023 at 02:23):

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?

view this post on Zulip Jason Gross (Jan 25 2023 at 02:24):

Hm, but, no, it still seems to work fine in the bug minimizer test-suite

view this post on Zulip Ali Caglayan (Jan 25 2023 at 09:50):

Looking for the META is probably a findlib error so my money is on OCAMLPATH or OCAMLFIND_CONF not being set correctly.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 25 2023 at 18:57):

This is not a findlib error but in tools/coqdep/lib/fl.ml


Last updated: Sep 25 2023 at 14:01 UTC