Zulip Chat Archive
Stream: general
Topic: mathlib CI submodule error
Adam Topaz (Jun 03 2022 at 16:23):
Does anyone understand where the following error comes from?
https://github.com/leanprover-community/mathlib/runs/6729106015?check_suite_focus=true
Adam Topaz (Jun 03 2022 at 16:23):
ping @Jack M
Adam Topaz (Jun 03 2022 at 16:24):
I suspect it's some issue with @Jack M 's git setup, but we can't figure out what the issue is.
Adam Topaz (Jun 03 2022 at 17:03):
The PR #14542 has the same error. It seems that both @Jack M and @Michael Blyth have some issue with their setup. Does anyone have any ideas?
Sebastian Ullrich (Jun 03 2022 at 17:21):
It looks like some impurity from the runner machine to me, i.e. not your fault
Adam Topaz (Jun 03 2022 at 17:22):
I mentioned this in the maintainer stream.
Reid Barton (Jun 03 2022 at 17:56):
On lines 309-310 the log says
/usr/bin/git reset --hard HEAD
HEAD is now at d60657c3e Added the concept of a line in projective space.
which is the commit with the submodule
Reid Barton (Jun 03 2022 at 18:05):
I suspect that whatever runner tried to build that commit with a submodule is now stuck
Adam Topaz (Jun 03 2022 at 18:18):
Aha, so the current CI run on master made it past the checkout step, which is promising.
https://github.com/leanprover-community/mathlib/runs/6730598604?check_suite_focus=true
It does indeed look like the issue is with a single runner.
Gabriel Ebner (Jun 03 2022 at 18:44):
Did somebody do something to fix the error? It looks like nael is fine again.
Yaël Dillies (Jun 03 2022 at 18:45):
Oh yes, hello, I am fine!
Gabriel Ebner (Jun 03 2022 at 18:47):
I was talking about nael the VM, not Yaël the person. :smile:
Adam Topaz (Jun 03 2022 at 18:49):
The only thing I did was delete the (empty) folder from same branch as the commit that Reid mentioned and pushed to that same branch
Adam Topaz (Jun 03 2022 at 18:50):
branch#projective_linear_subspace
Last updated: Dec 20 2023 at 11:08 UTC