lake update failing with git error

Stream: lean4

[Bhavik Mehta]

Running lake update in a repo of mine is giving this error:

$ lake update
error: external command 'git' exited with code 1

How can I figure out what's going on here? Git is otherwise working as normal for me

[Bhavik Mehta]

Ah, the verbose option. I'm still not sure what the fix is though:

trace: ././.lake/packages/mathlib> git fetch --tags --force origin
trace: stderr:
error: cannot lock ref 'refs/remotes/origin/jt496_brooks': is at 756d8e3dbdf1959dc91b6dc74b8c29756e915825 but expected 9fbf12e16956d0ae7c908fed62da8f0d69c32c33
From https://github.com/leanprover-community/mathlib4
 ! 9fbf12e169..3058685a7a  jt496_brooks -> origin/jt496_brooks  (unable to update local ref)
 + b1b71c3f05...dadb75c188 update-dependencies-bot-use-only -> origin/update-dependencies-bot-use-only  (forced update)

[Kim Morrison]

Have you tried nuking the .lake/packages/mathlib directory?

[Bhavik Mehta]

That seemed to work - it made git use 300% of my CPU, but it worked! Thanks!

[Kim Morrison]

I usually assume "cannot lock ref" means git got into a bad state, that rarely reproducible,.

[Edison Xie]

same error happened to me... is there anything wrong with v19.0 -rc3?

[Kevin Buzzard]

I had a git error code 128 yesterday with a failing lake update mathlib but the usual faffing around fixed it in the end.

[Edison Xie]

mine is fixes using nuke mathlib directory but I doubt that's the normal way to do... (