Gaëtan Gilbert (Jul 01 2020 at 12:01): Gaëtan Gilbert (Jul 01 2020 at 12:01):https://gitlab.com/coq/coq/-/jobs/619174897
CAMLOPT -c -for-pack Metacoq_template_plugin gen-src/ast_denoter.ml
findlib: [WARNING] Interface numeral.cmi occurs in several directories: /builds/coq/coq/_install_ci/lib/coq/plugins/syntax, gen-src
File "gen-src/ast_denoter.ml", line 1:
Error: Corrupted compiled interface
gen-src/ast_quoter.cmi
Command exited with non-zero status 2
gen-src/ast_denoter.cmx (real: 0.06, user: 0.01, sys: 0.01, mem: 20204 ko)
Makefile.plugin:667: recipe for target 'gen-src/ast_denoter.cmx' failed
this looks very much like the infamous OCaml bug (fixed in OCaml 4.06.0) that plagued Gauillaume Claret's CompCert builds
Karl Palmskog (Jul 01 2020 at 12:13):we fixed this by only doing parallel compilation if the OCaml version is >= 4.06.0
Karl Palmskog (Jul 01 2020 at 12:13):https://github.com/AbsInt/CompCert/issues/327
Last updated: May 28 2023 at 13:30 UTC