Stream: MetaCoq

Topic: Failure in Coq's CI


view this post on Zulip Théo Zimmermann (Nov 18 2020 at 17:11):

I've seen this error on several PRs: https://gitlab.com/coq/coq/-/jobs/857883485

sigma.vo does not exist
MiniHoTT.vo does not exist
MiniHoTT_paths.vo does not exist
translation_utils.vo does not exist
param_original.vo does not exist
param_cheap_packed.vo does not exist
param_generous_packed.vo does not exist
times_bool_fun.vo does not exist
times_bool_fun2.vo does not exist
param_binary.vo does not exist
standard_model.vo does not exist
sigma.glob does not exist
MiniHoTT.glob does not exist
MiniHoTT_paths.glob does not exist
translation_utils.glob does not exist
param_original.glob does not exist
param_cheap_packed.glob does not exist
param_generous_packed.glob does not exist
times_bool_fun.glob does not exist
times_bool_fun2.glob does not exist
param_binary.glob does not exist
standard_model.glob does not exist
Makefile.coq:530: recipe for target 'install' failed
make[3]: *** [install] Error 1

It doesn't seem related to an error that would come from a recent overlay, so I'm signaling it to you.

view this post on Zulip Matthieu Sozeau (Nov 18 2020 at 18:23):

Thanks. Curiously our CI did not catch this

view this post on Zulip Matthieu Sozeau (Nov 18 2020 at 18:38):

Hopefully fixed now

view this post on Zulip Enrico Tassi (Nov 18 2020 at 22:05):

I did try to pin the merge commit for the "cumulative thing syntax" and I got the error @Théo Zimmermann reported, then the current master tip fcaf3e7cd38b289017d7316586c021979ebb0a72 but it does seems to work for me here: https://github.com/coq/coq/pull/13409
The log https://gitlab.com/coq/coq/-/jobs/858636887 says that the target 1 does not exist.

view this post on Zulip Matthieu Sozeau (Nov 19 2020 at 08:39):

The log with the error is still on the master tip fcaf3e ?

view this post on Zulip Matthieu Sozeau (Nov 19 2020 at 08:43):

Well I can see it is. Sorry, my fix was partial (the problem is a mishandling of the TIMED Makefile variable). It should now pass with the latest master tip

view this post on Zulip Matthieu Sozeau (Nov 19 2020 at 13:22):

I confirm, all the CIs I could check pass on metacoq now


Last updated: Aug 11 2022 at 02:03 UTC