Stream: Coq devs & plugin devs

Topic: fiat-crypto-ocaml failing


view this post on Zulip Gaëtan Gilbert (Jul 09 2020 at 16:57):

eg https://gitlab.com/coq/coq/-/jobs/630766766

File "src/Rewriter/Util/plugins/strategy_tactic.mli", line 1:
Error: /builds/coq/coq/_install_ci/lib/coq//kernel/names.cmi
is not a compiled interface for this version of OCaml.
It seems to be for a newer version of OCaml.

cc @Jason Gross

view this post on Zulip Jason Gross (Jul 09 2020 at 18:28):

Why does the CI job for library:ci-fiat_crypto_ocaml run make in /builds/coq/coq/_build_ci/rewriter (and also in bignums)? Furthermore, why is there plugin/bignums_syntax_plugin.mlpack and plugin/bignums_syntax.ml in the rewriter directory, and why does make run OCAMLLIBDEP and CAMLDEP on them, and how is it possible that it can do this before creating Makefile.coq (and why is Makefile.coq missing in the first place?) Furthermore, there is a build failure on plugin/bignums_syntax.ml. I'm thoroughly confused by all this, but it seems like it's a bug in Coq's CI scripts (which should not ever be rebuilding things in dependencies: / needs:), not in fiat-crypto-ocaml? (This is presumably only caught by fiat-crypto-ocaml because it's the only one which uses a version of OCaml which is incompatible with the one that compiled the library that it depends on? (It's also the only one where needs does not include transitive dependencies, c.f. https://github.com/coq/coq/pull/12431#discussion_r432926226))

view this post on Zulip Gaëtan Gilbert (Jul 09 2020 at 21:11):

Ah, I was wrong about not needing transitive dependencies. We call into Makefile.ci so it will try building the dependencies, normally the recursive make recognises that there's nothing to do but in this case there is something to do.


Last updated: Oct 21 2021 at 21:03 UTC