git error `cannot lock ref`

Stream: mathlib4

[Kevin Buzzard]

What have I done? (more importantly: how do I fix it?)

buzzard@buster:~/lean-projects/mathlib4$ git status
On branch master
Your branch is behind 'origin/master' by 174 commits, and can be fast-forwarded.
  (use "git pull" to update your local branch)

nothing to commit, working tree clean
buzzard@buster:~/lean-projects/mathlib4$ git pull
error: cannot lock ref 'refs/remotes/origin/sync/Algebra.Algebra.Basic': 'refs/remotes/origin/sync' exists; cannot create 'refs/remotes/origin/sync/Algebra.Algebra.Basic'
From github.com:leanprover-community/mathlib4
 ! [new branch]          sync/Algebra.Algebra.Basic -> origin/sync/Algebra.Algebra.Basic  (unable to update local ref)
buzzard@buster:~/lean-projects/mathlib4$

[Eric Wieser]

I don't think you're allowed to have a branch called foo/bar if the branch foo already exists

[Eric Wieser]

git branch -d origin/sync should do the trick

[Eric Wieser]

Or git fetch origin --prune, though that will delete a lot of dead branches

[Kevin Buzzard]

error: branch 'origin/sync' not found.

for the git branch -d suggestion

[Kevin Buzzard]

Eric Wieser said:

Or git fetch origin --prune, though that will delete a lot of dead branches

That fixed it. Thanks!

[Ruben Van de Velde]

Oh no, sorry about that branch name

[Eric Wieser]

git branch -dr origin/sync sounds like what I should have said

[Eric Wieser]

But --prune is usually safe unless you were planning to merge with a PR that bors has merged; and even then, you can get the refs back manually

[Kevin Buzzard]

I have no desire to have any branches at all locally other than master and the one I'm currently working on. Already git branch is unusable for me in mathlib3, and it's becoming unusable in mathlib4 (the output is too long).