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