search

leanprover / vscode-lean4

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

"Download project" flow is confusing #530

Closed TwoFX closed 1 month ago

TwoFX commented 1 month ago

Description

The "Download project" command shows the following dialog: image

An easy mistake to make here is to paste in a Git repository URL immediately at this. This leads to a state where hitting Enter does nothing. The correct way to do it would be to first click on "Git repository URL" or hit enter while the text box is empty and then paste in the repository URL and hit Enter. This is easy to get wrong and we should restructure the dialog so that it's less easy to get stuck.

Context

As described in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/gitpod.2Fcodespaces.2Flocal.20installation.20for.20Lean.20repo/near/474783261

Steps to Reproduce

  1. Invoke the "Download project" command from the Forall menu
  2. Paste in a Git repo URL immediately
  3. Hit the Enter key -> nothing happens

Expected behavior: Either the flow makes this situation impossible or hitting Enter should do the right thing

Actual behavior: No thing happens and there is no feedback

Versions

0.0.178

Lean (version 4.9.0-nightly-2024-05-23, x86_64-unknown-linux-gnu, commit d984030c6a68, Release)

Linux markus-z16 6.10.11-200.fc40.x86_64 #1 SMP PREEMPT_DYNAMIC Wed Sep 18 21:09:58 UTC 2024 x86_64 GNU/Linux

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

mhuisi commented 1 month ago

Sorry, but this is not possible with VS Code's API. We can't remove the search bar and we can't make the search bar select "Git repository URL" for an arbitrary search string. You can find the whole quick pick API provided by VS Code here. There is also no other VS Code UI component we could use here.

The only options I see is that we can either have a template selector of this form here, we have no template selector at all or we re-implement the entirety of all VS Code UI components we use in commands for dialogs in separate webviews.

mhuisi commented 1 month ago

@bollu made me aware of the fact that there's some more API at window.createQuickPick that we could use to improve the UI of the quick pick mechanism, so I think that this is feasible after all.