Weird CI failure

Stream: general

[Anne Baanen]

I'm getting the following CI failure that I don't understand:

Setting up auth
  /usr/bin/git config --local --name-only --get-regexp core\.sshCommand
  /usr/bin/git submodule foreach --recursive git config --local --name-only --get-regexp 'core\.sshCommand' && git config --local --unset-all 'core.sshCommand' || :
  Error: fatal: No url found for submodule path 'class-number' in .gitmodules
  Error: The process '/usr/bin/git' failed with exit code 128

The only relation I can think of is that the Lean Forward organisation has a separate class-number repository that has mathlib as a dependency, but this commit was made on a clean copy of mathlib master. And neither repository has a .gitmodules file AFAICT

[Anne Baanen]

Other CI jobs with the same "Setting up auth" rule pass, but restarting the build doesn't seem to help.

[Oliver Nash]

Likewise I've suddenly started hitting this and I'm very confused. It is surely a coincidence but I've been tidying up branch#p-adic and just removed an empty folder (in that branch) called class-number!

[Eric Wieser]

https://github.com/leanprover-community/mathlib/runs/3115085697#step:2:149 is the same

[Johan Commelin]

Is there any reason why class-number could have ended up on the CI runners?
And is there a chance that CI runs aren't cleaning up after themselves well enough?

[Anne Baanen]

I haven't touched the class-number repo in a couple of weeks, it's in a different organisation and I don't think it involves any submodules. So I don't think that's the cause.

[Anne Baanen]

CI runners keeping around a bit too much state sounds possible.

[Anne Baanen]

Git doesn't track directories, so removing an empty directory from the repository sounds a bit suspicious...

[Oliver Nash]

Here's the commit where I remove an empty folder called class-number: https://github.com/leanprover-community/mathlib/commit/de03792d96f51fccc2813f98c156dca62b803173 but I _now_ note that earlier commits on that branch also hit the same error.

[Anne Baanen]

Yeah, looking at the diff saying "Submodule class-number deleted from 6330d4" this seems to be almost directly connected.

[Eric Wieser]

https://github.com/actions/checkout/issues/354

[Eric Wieser]

And also https://github.com/actions/checkout/issues/385

[Eric Wieser]

Which is specific to self-hoster runners

[Johan Commelin]

Good find! That sounds very related to the problems we are seeing!

[Eric Wieser]

So for now we can just clean up the worker and hope no one ever makes a submodule again

[Anne Baanen]

Issue 385 seems to be exactly what is going on here. Would a CI step that removes .gitmodules before checkout fix this?

[Bryan Gin-ge Chen]

Seems worth trying!

[Bryan Gin-ge Chen]

(I should add that I can't work on this until tonight, so if someone wants to take a shot at it, please do!)