Zulip Chat Archive
Stream: lean4
Topic: lake update silently fails
Patrick Massot (Oct 26 2023 at 16:37):
When running lake update foo with a typo in foo, there is no message at all. Example lake update std4 in Mathlib will produce no output at all.
Patrick Massot (Oct 26 2023 at 16:37):
By the way, Mario, I regularly get caught by the fact the repository is called std4 but the lib is std.
Mac Malone (Oct 26 2023 at 17:17):
@Patrick Massot This is expected but also undesirable. An issue for this would be great!
Patrick Massot (Oct 26 2023 at 17:20):
Last updated: Dec 20 2023 at 11:08 UTC