lake doesn't allow transitive dependencies to use non-default branches? #3167
Description
I'm not sure I'm diagnosing this correctly, but in the bump-3159 branch of https://github.com/leanprover-community/repl, in the folder test/Mathlib, I can't get lake update to succeed.
The situation here is that we have lakefile with:
require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "lean-pr-testing-3159"
and the lakefile in that branch of Mathlib itself says
require std from git "https://github.com/leanprover/std4" @ "lean-pr-testing-3159"
Running lake update there persistently gives the error message:
% lake update
mathlib: cloning https://github.com/leanprover-community/mathlib4 to './.lake/packages/mathlib'
std: cloning https://github.com/leanprover/std4 to './.lake/packages/std'
error: > git checkout --detach c70b9499d9af95eea6c5d7073874b7cf2c715afe # in directory ./.lake/packages/std
error: stderr:
fatal: reference is not a tree: c70b9499d9af95eea6c5d7073874b7cf2c715afe
error: external command `git` exited with code 128
despite c70b9499d9af95eea6c5d7073874b7cf2c715afe being the perfectly good HEAD of the lean-pr-testing-3159 branch at Std.