Théo Zimmermann (Nov 18 2020 at 17:11): 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.
Matthieu Sozeau (Nov 18 2020 at 18:23):Thanks. Curiously our CI did not catch this
Matthieu Sozeau (Nov 18 2020 at 18:38):Hopefully fixed now
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.
Matthieu Sozeau (Nov 19 2020 at 08:39):The log with the error is still on the master tip fcaf3e ?
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
Matthieu Sozeau (Nov 19 2020 at 13:22):I confirm, all the CIs I could check pass on metacoq now
Last updated: Jun 03 2023 at 18:01 UTC