Stream: Coq devs & plugin devs

Topic: spurious metacoq failure?


view this post on Zulip 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

view this post on Zulip Karl Palmskog (Jul 01 2020 at 12:12):

this looks very much like the infamous OCaml bug (fixed in OCaml 4.06.0) that plagued Gauillaume Claret's CompCert builds

view this post on Zulip Karl Palmskog (Jul 01 2020 at 12:13):

we fixed this by only doing parallel compilation if the OCaml version is >= 4.06.0

view this post on Zulip Karl Palmskog (Jul 01 2020 at 12:13):

https://github.com/AbsInt/CompCert/issues/327


Last updated: Oct 21 2021 at 20:02 UTC