metacoq icon indicating copy to clipboard operation
metacoq copied to clipboard

Published 20 hours ago • verified publisher icon MetaCoq

ci-local-noclean target fails

Open JasonGross opened this issue 4 years ago • 1 comments

At https://github.com/coq-community/run-coq-bug-minimizer/runs/4123345900?check_suite_focus=true#step:5:46597

*** No rule to make target '/builds/coq/coq/_build_ci/metacoq/template-coq/gen-src/datatypes.cmx', needed by 'gen-src/metacoq_template_plugin.cmx'.  Stop.

You can recreate this (for now) by downloading the artifacts at https://gitlab.com/coq/coq/-/jobs/1750733291/artifacts/download and https://gitlab.com/coq/coq/-/jobs/1750733365/artifacts/download. This is at coq/coq@0e663cc0d89ef05d5396a244eb4fb23181fc9d78

JasonGross avatar Nov 10 '21 18:11 JasonGross

This issue is still making metacoq failures unminimizable at https://github.com/coq/coq/pull/15770#issuecomment-1059719299

JasonGross avatar Mar 05 '22 16:03 JasonGross