lake failing with git error

Stream: lean4

[Scott Morrison]

In https://github.com/leanprover-community/mathlib3-port, the first run of lake buildgives various output, amongst which there is error: git exited with code 128.

Subsequent runs just fail with this error:

$ lake build
leanbin: trying to update ./lean_packages/leanbin to revision master
mathlib: trying to update ./lean_packages/mathlib to revision 64f9c43eb9a75fb4c5989ac711623d06e9696e60
error: git exited with code 128
error: build failed

[Scott Morrison]

I'd like to know the git command that lake is running in order to diagnose the problem.

[Scott Morrison]

@Mac or otherwise, is there a way to uncover this easily?

[Scott Morrison]

In the meantime, the problem seems to have gone away. The only thing I seem to have changed is to rename the repository, and the dependent repository, so they don't have - in the name. If that rings any bells, perhaps this is worth investigating. Otherwise, it's just a generic request for better error reporting from lake when git fails!

[Mac]

@Scott Morrison feel free to post this issue on Lake (i.e., logging for the executed Git command). Sorry that I haven't be speedily addressing your comments this week. I have been otherwise occupied.

[Scott Morrison]

No worries! I'll see if I can make a repro later.

[Alexander Bentkamp]

I just had the same issue. I was able to work around it by manually cloning the dependencies into lean_packages.