No progress indicator for a long time when downloading a project in VSCode

[kim-em]

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.

[tydeu]

I think the best solution here is to eagerly print the log lines for dependency resolution.

[utensil]

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.

[tydeu]

@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.

[utensil]

@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!

[mhuisi]

With leanprover/vscode-lean4#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.