coq binaries from CI are basically unusable without docker

[JasonGross]

I'd like to reuse CI artifacts when debugging failures. It used to be the case that I could just download the artifacts and unpack them, and coqc would run. Since the findlib PR, though, the binaries generate anomalies:

$ ./_install_ci/bin/coqtop
Error:
Anomaly
"Uncaught exception Failure("Config file not found - neither /root/.opamcache/4.14.0+flambda/lib/findlib.conf nor the directory /root/.opamcache/4.14.0+flambda/lib/findlib.conf.d")."
Please report at http://coq.inria.fr/bugs/.

Setting the OCAMLFIND environment variable does not change this. There should be a way to run these binaries without needing docker.

cc @gares @ejgallego

[ejgallego]

The right variable for this is OCAMLFIND_CONF . I'm unsure we can do better, as Coq now requires a working findlib to work.

[JasonGross]

Can the error message at least mention OCAMLFIND_CONF and suggest a way of determining what it should be set to (e.g., which ocamlfind or ocamlfind -where or whatever)?

[ejgallego]

Sure, tho I guess the most principled solution would be to document that Coq now requires a working ocamlfind setup and point out to findlib's own documentation.

[gares]

why don't you use the docker image?

[andrew-appel]

I agree with @JasonGross that the error message should be changed.
That is: I consider it a bug, not a feature, that a basic install of Coq now requires an external environment variable telling it where to find ocamlfind. But if you consider it a feature, that is, perfectly normal behavior that an environment variable must be set, then the error message should not say "Please report", it should say, "Coq cannot work without an environment variable OCAMLFIND_CONF set, you might try something like 'export OCAMLFIND_CONF=/etc/ocamlfind.conf' "

[ejgallego]

Indeed this is far from optimal, error handling here can be better but ocamlfind raises a generic Failure exception so we'd need submit a patch to ocamlfind.

As for plugins, since OCaml 4.08 we have little choice than to locate plugins ocamlfind, due to the way OCaml plugins work since that release.

I wish something like ocamlfind would be a standard part of OCaml but so far attempts to do so have failed.

[silene]

the error message should not say "Please report", it should say, "Coq cannot work without an environment variable OCAMLFIND_CONF set

You might be missing an important point. As explained by @ejgallego, the error message does not originate from Coq but from Findlib. We do not control its wording. Coq is just adding the sentence "Please report ...". I suggest we stop systematically telling people to "Please report at http://coq.inria.fr/bugs/" every time something unexpected happens. Because of this message, people think that every issue they encounter is a bug in Coq.

And by the way, Coq works just fine even when OCAMLFIND_CONF is not set, as long as you did not remove the Findlib files from their expected location. In other words, this bug report is the same as randomly deleting files and then complaining that a tool no longer works. So, closing.