Stream: MetaCoq

Topic: No rule to make target tm_util.cmx


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

?

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

view this post on Zulip Yannick Forster (Jun 03 2021 at 18:21):

The only slightly crazy thing is that MetaCoq patches the extraction of cRelationClasses I think

view this post on Zulip Yannick Forster (Jun 03 2021 at 18:21):

Because there is a bug in extraction

view this post on Zulip Yannick Forster (Jun 03 2021 at 18:22):

But that seems unrelated at first

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

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

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

view this post on Zulip Jason Gross (Jun 04 2021 at 17:23):

Reported test-suite issue as https://github.com/MetaCoq/metacoq/issues/563

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

view this post on Zulip Matthieu Sozeau (Jun 04 2021 at 17:25):

Hmm, is the file taking time to build in the test-suite the live extraction one?

view this post on Zulip Matthieu Sozeau (Jun 04 2021 at 17:25):

But yes, I suppose we can improve the makefile

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

view this post on Zulip Jason Gross (Jun 04 2021 at 17:50):

Improving the makefile to not rebuild the test-suite would be very much appreciated

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 06 2021 at 16:23):

https://github.com/coq/coq/issues/6614


Last updated: Aug 11 2022 at 03:02 UTC