leanprover
No progress indicator for a long time when downloading a project in VSCode
When downloading a project using the VSCode extension, if that project is downstream of Mathlib there is a very long wait with no visual feedback or explanation of what is happening, while lake is cloning all of Mathlib.
This corresponds to the following terminal output:
/home/mhuisi/Lean/MathlibTest> lake exe cache get
<<<<<<< Very long pause here with no explanation of what is happening >>>>>>>>>>>>
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient to '././.lake/packages/LeanSearchClient'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
Even though I know this is an issue, the cancel button or ctrl-c is very tempting because it feels like something is wrong.
@tydeu, my suggestion here is to hard-code a check for Mathlib (yes, I know you don't like the idea :-) and before cloning Mathlib print a "info: cloning Mathlib, depending on your connection this may take some time".
There needs to be something to tell the user something is happening.
An alternative solution would be to investigate doing a shallow clone of Mathlib, but I'm not sure how viable that is.
See zulip discussion.
I think the best solution here is to eagerly print the log lines for dependency resolution.
I think the best solution here is to eagerly print the log lines for dependency resolution.
👍
And this would not be noisy as long as such print is erased like the building progress bar, or erased and updated to the final print for the finished clone like what is already printed out now.
Context: coming from zulip.
@utensil
And this would not be noisy as long as such print is erased like the building progress bar, or erased and updated to the final print for the finished clone like what is already printed out now.
Unfortunately, the solution in #5684 does not have any fancy ANSI updates. There are not many log lines, though, and lake update is an infrequently executed command, so hopefully it is not too noisy.
@tydeu No worries, my casual comment was only because I had no idea how many outputs would be there, and whether they are proportional to other informative outputs. Thanks!
With https://github.com/leanprover/vscode-lean4/pull/542 (still to be released), the progress bar now displays that something is going on in the background more clearly, even when the command doesn't report any output. This doesn't resolve this issue entirely, but it should help a bit.
A variant of this can happen with Reservoir lookups. To illustrate, look at the output of lake exe cache get on a new project if you don't have Internet connectivity:
$ 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
No info message is printed before the Reservoir lookup (which is done via curl). If you do have a flaky connection instead, the curl step can stall and produce the symptoms described here.
Is this still a thing? I see it's been closed.
I just saw a nice variant of this: I cloned compfiles and after lake exe cache get I immediately saw
info: tryAtEachStep: cloning https://github.com/dwrensha/tryAtEachStep
info: tryAtEachStep: checking out revision 'bd4b85d8a4a8110ae14ad917d09a8e8c5bb540fd'
(so I knew things were alive) and then a huuuge pause (I timed it at 23 seconds, long enough for someone to start thinking "is something broken?"), and then
info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision '19e565f28586cfabfa4b33ac0960048ab95497d8'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a'
...
For me it would be much better if the first info line ("cloning mathlib") appeared before the huge pause, because then you at least understand why there's a huge pause (checking out a revision doesn't take 23 seconds). Even better would be one of those ........ things with more dots appearing, I guess.
@kim-em I think the new version is a slightly different issue with the same effect. The previous issue did not print any log lines at all until everything was cloned. This is printing some, just not the currently cloning one. It is probably an overlooked case (e.g., not enough flushing).