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
Why does the CI job for
/builds/coq/coq/_build_ci/rewriter (and also in bignums)? Furthermore, why is there
plugin/bignums_syntax.ml in the rewriter directory, and why does
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
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))
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