Jason Gross (Jun 03 2021 at 16:20): Jason Gross (Jun 03 2021 at 16:20):Can anyone explain why building metacoq (using Coq's CI target) would fail with
patching file gen-src/cRelationClasses.mli
Hunk #1 succeeded at 98 (offset -6 lines).
make[4]: Leaving directory '/github/workspace/builds/coq/coq/_build_ci/metacoq/template-coq'
coq_makefile -f _TemplateCoqProject -o Makefile.template
`which gsed || which sed` -i -e s/coqdeps/coqdeps.template/g Makefile.template
make -f Makefile.template optfiles
make[4]: Entering directory '/github/workspace/builds/coq/coq/_build_ci/metacoq/template-coq'
COQDEP VFILES
COQPP src/g_template_coq.mlg
CAMLDEP src/plugin_core.mli
CAMLDEP src/run_template_monad.mli
CAMLDEP src/template_monad.mli
OCAMLLIBDEP src/template_coq.mlpack
CAMLDEP src/plugin_core.ml
CAMLDEP src/run_template_monad.ml
CAMLDEP src/template_monad.ml
CAMLDEP src/constr_denoter.ml
CAMLDEP src/constr_quoter.ml
CAMLDEP src/constr_reification.ml
CAMLDEP src/denoter.ml
CAMLDEP src/quoter.ml
CAMLDEP src/reification.ml
CAMLDEP src/tm_util.ml
CAMLDEP src/g_template_coq.ml
make[4]: *** No rule to make target '/github/workspace/builds/coq/coq/_build_ci/metacoq/template-coq/src/tm_util.cmx', needed by 'src/template_coq.cmx'. Stop.
make[4]: Leaving directory '/github/workspace/builds/coq/coq/_build_ci/metacoq/template-coq'
Makefile:11: recipe for target 'template-coq' failed
make[3]: *** [template-coq] Error 2
make[3]: Leaving directory '/github/workspace/builds/coq/coq/_build_ci/metacoq/template-coq'
Makefile:61: recipe for target 'template-coq' failed
make[2]: *** [template-coq] Error 2
make[2]: Leaving directory '/github/workspace/builds/coq/coq/_build_ci/metacoq'
Makefile:92: recipe for target 'ci-local' failed
make[1]: *** [ci-local] Error 2
make[1]: Leaving directory '/github/workspace/builds/coq/coq/_build_ci/metacoq'
Makefile.ci:110: recipe for target 'ci-metacoq' failed
make: *** [ci-metacoq] Error 2
?
Jason Gross (Jun 03 2021 at 17:39):Is metacoq doing some sort of crazy build process where wrapping the coq binaries with a wrapper that prints things to stderr is going to mess things up?
Yannick Forster (Jun 03 2021 at 18:21):The only slightly crazy thing is that MetaCoq patches the extraction of cRelationClasses I think
Yannick Forster (Jun 03 2021 at 18:21):Because there is a bug in extraction
Yannick Forster (Jun 03 2021 at 18:22):But that seems unrelated at first
Matthieu Sozeau (Jun 04 2021 at 08:52):I think the problem lies maybe in g_template_coq.ml being there, it should be generated from g_template_coq.mlg. Did you clean before building?
Matthieu Sozeau (Jun 04 2021 at 08:52):It doesn't care about what coqc does I think. But the .mlg processing might be disrupted by your wrapper??
Jason Gross (Jun 04 2021 at 17:12):I don't clean specifically because I want to re-use the build artifacts (I expect that running make -f Makefile.ci ci-metacoq twice in a row should be idempotent). I have a dockerfile at https://github.com/coq/coq/issues/14453 which demonstrates a different but possibly related bug. It's pretty hard to debug this, though, because metacoq's test-suite is re-run from scratch every time I build and takes 40 minutes to run :-/
Jason Gross (Jun 04 2021 at 17:23):Reported test-suite issue as https://github.com/MetaCoq/metacoq/issues/563
Jason Gross (Jun 04 2021 at 17:23):@Matthieu Sozeau Can you reproduce the dockerfile issue? Do you have a dockerfile that uses CI artifacts and successfully builds metacoq?
Matthieu Sozeau (Jun 04 2021 at 17:25):Hmm, is the file taking time to build in the test-suite the live extraction one?
Matthieu Sozeau (Jun 04 2021 at 17:25):But yes, I suppose we can improve the makefile
Jason Gross (Jun 04 2021 at 17:27):Timing log for the second rebuild is at https://gitlab.com/coq/coq/-/jobs/1316144597, things over 10s are:
Time | Peak Mem | File Name
-------------------------------------------------------------
39m39.94s | 4024372 ko | Total Time / Peak Mem
-------------------------------------------------------------
6m56.68s | 4024372 ko | bugkncst.vo
3m06.72s | 1083852 ko | PCUICSafeReduce.vo
2m58.84s | 992812 ko | PCUICSafeConversion.vo
1m57.70s | 785816 ko | PCUICInductiveInversion.vo
1m28.76s | 917816 ko | PCUICSR.vo
1m18.53s | 802248 ko | PCUICParallelReductionConfluence.vo
1m04.73s | 1373264 ko | PCUICSafeRetyping.vo
0m58.01s | 1011208 ko | ErasureCorrectness.vo
0m49.98s | 786064 ko | Typing.vo
0m40.74s | 769208 ko | PCUICSafeChecker.vo
0m39.99s | 815808 ko | PCUICEquality.vo
0m38.52s | 766588 ko | PCUICPrincipality.vo
0m36.30s | 833820 ko | erasure_live_test.vo
0m35.74s | 746556 ko | PCUICNormal.vo
0m33.26s | 645780 ko | PCUICCanonicity.vo
0m32.88s | 690708 ko | PCUICTyping.vo
0m32.81s | 727004 ko | PCUICConversion.vo
0m31.02s | 731156 ko | PCUICConfluence.vo
0m28.75s | 555508 ko | PCUICClosed.vo
0m26.11s | 666244 ko | PCUICSpine.vo
0m25.82s | 621264 ko | PCUICSigmaCalculus.vo
0m25.75s | 733704 ko | PCUICParallelReduction.vo
0m25.51s | 704024 ko | PCUICPosition.vo
0m24.08s | 786404 ko | times_bool_fun.vo
0m23.56s | 746404 ko | param_original.vo
0m22.57s | 877840 ko | EOptimizePropDiscr.vo
0m22.53s | 563276 ko | PCUICLiftSubst.vo
0m22.49s | 639976 ko | PCUICCumulProp.vo
0m22.39s | 606008 ko | PCUICWcbvEval.vo
0m21.66s | 620428 ko | PCUICSubstitution.vo
0m19.07s | 560640 ko | Substitution.vo
0m18.33s | 635088 ko | PCUICWeakening.vo
0m18.05s | 493488 ko | Closed.vo
0m17.09s | 636528 ko | EWcbvEval.vo
0m16.74s | 735364 ko | ErasureFunction.vo
0m16.52s | 526864 ko | tauto.vo
0m15.70s | 606756 ko | PCUICInductives.vo
0m15.55s | 605804 ko | PCUICConvCumInversion.vo
0m15.36s | 567196 ko | PCUICWfUniverses.vo
0m14.50s | 594568 ko | PCUICNameless.vo
0m13.70s | 633464 ko | PCUICAlpha.vo
0m12.72s | 537992 ko | opaque.vo
0m12.50s | 566140 ko | PCUICContextConversion.vo
0m12.27s | 567276 ko | TemplateToPCUICCorrectness.vo
0m12.02s | 519492 ko | Weakening.vo
0m10.94s | 503060 ko | utils/wGraph.vo
0m10.57s | 703332 ko | ESubstitution.vo
0m10.44s | 500584 ko | LiftSubst.vo
Improving the makefile to not rebuild the test-suite would be very much appreciated
Jason Gross (Jun 04 2021 at 17:51):@Yannick Forster
Because there is a bug in extraction
What's the bug in extraction? I'm wondering if adding a few Extraction Inline directives might be a better strategy than patching the extracted files post-hoc
Emilio Jesús Gallego Arias (Jun 06 2021 at 16:23):https://github.com/coq/coq/issues/6614
Last updated: Jun 01 2023 at 13:01 UTC