search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
145 stars 43 forks source link

feature request: more visible feedback when creating a new project #457

Open TwoFX opened 2 months ago

TwoFX commented 2 months ago

Proposal

When creating a new Lean project using mathlib from the extension, a lot of stuff happens: elan pulls in the correct Lean version, the cache tool is built and downloads the cache, etc. Depending on the internet connection, this can take a minute or two. While this is running, the only feedback the user receives is a small window in the lower-right corner of the screen. For me, it looks like this:

image

It actually took me a while to spot it, for a few seconds I thought that creating the project had silently failed. The messages in the box are also quite technical, as a new user I would find it hard to tell from this screenshot that yes, the project is being created, I just have to be patient.

For this reason, I think that it would be good to provide more and clearer feedback that creating the project is in progress.

Community Feedback

I didn't start a Zulip discussion because this is a pretty clear new user papercut to me, but if you want a discussion I can start one.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

mhuisi commented 2 months ago

This is unfortunately the only way we can display progress in VS Code and the other places where we could display it are even worse in terms of discoverability: https://code.visualstudio.com/api/references/vscode-api#ProgressLocation

The messages in the box are also quite technical, as a new user I would find it hard to tell from this screenshot that yes, the project is being created, I just have to be patient.

The start of the message is the non-technical description ("Updating dependencies"), what follows is command being executed and the output of the command. Clicking the (Details) link will also take you to more explicit output. It has to be a link and not a button because VS Code does not let us contribute additional buttons to the progress notification. I suppose we could auto-focus this view by default for certain operations, though I suspect that this will also be annoying to users.

I've certainly thought that this is sub-optimal a couple of times myself, but all-in-all, I don't really see what we could do about this given the constraints of VS Code.

TwoFX commented 2 months ago

I think it would already help if the box contained something high-level like like "Creating new Lean project" or "Busy creating new Lean project" in front of "Updating dependencies".