lake hanging on new project

Stream: general

[Peter Nelson]

My lake is hanging in the following way:

peternelson@Peters-MacBook-Pro GitHub % rm -rf foo
peternelson@Peters-MacBook-Pro GitHub % lake new foo math
info: downloading mathlib `lean-toolchain` file
peternelson@Peters-MacBook-Pro GitHub % cd foo
peternelson@Peters-MacBook-Pro foo % lake exe cache get
info: foo: no previous manifest, creating one from scratch

And nothing further after waiting minutes.
Similar for lake build. I have killed any lean/lake related processes and vscode, and tried updating elan and a system reset, and the problem persists. Things work fine inside a mathlib directory.

Can anyone help?

[Peter Nelson]

And like magic, the problem disappeared after half an hour during which time I'd done nothing.

I think this has happened to me before, and I've been as baffled in the past as I am now. Does this kind of behaviour ring any bells?

[Sebastian Ullrich]

It could be temporary network issues since it was likely trying to download dependencies

[Peter Nelson]

Would that also be a problem with lake build?

[Sebastian Ullrich]

Sure, they are build dependencies

[Peter Nelson]

It would be nice to have lake indicate this failure mode rather than hang.

[Sebastian Ullrich]

You didn't specify your Lean version, this should be addressed by https://github.com/leanprover/lean4/issues/5615

[Sebastian Ullrich]

However given using Mathlib should have upgraded Lean, it may be a different issue after all

[Mauricio Collares]

I can confirm this still exists. If you have no internet connection and no manifest, you see:

$ lake exe cache get
info: MyProject: no previous manifest, creating one from scratch
error: external command 'curl' exited with code 6
error: leanprover-community/mathlib: Reservoir lookup failed
error: leanprover-community/mathlib: could not materialize package: this may be a transient error or a bug in Lake or Reservoir

but notice that no info message is printed before the Reservoir lookup (which is done via curl). If that stalls due to network issues, you'll get an apparent hang.

[Sebastian Ullrich]

Thanks for confirming, could you please leave a comment in the issue?