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
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))
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 13 2024 at 01:02 UTC