search

leanprover / vscode-lean4

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

Welcome page doesn't open #529

Open fpvandoorn opened 1 month ago

fpvandoorn commented 1 month ago

Description

If I (uninstall and re)install the extension, the welcome page does not open automatically (in contrast to what the README says). I am on Windows.

However, the ∀-symbol is always visible, so no need to create an empty file anymore before clicking it. (Related Lean PR: https://github.com/leanprover/lean4/pull/5559 )

mhuisi commented 1 month ago

It's worth pointing out that VS Code may not open the welcome page again if you uninstall and re-install the extension (it caches the VSIX and also some state). I believe it only does that on first install.

I've also seen this fail a few times on the first install for unknown reasons, but this is almost surely on VS Code's side. So it does work sometimes, and in case it doesn't, we provide instructions.

Having looked into this for a couple of hours before, I'm not sure what to do about this other than move away from VS Code's welcome page mechanism entirely and use a custom HTML page and custom state management to detect the first installation of the extension instead.

fpvandoorn commented 1 month ago

It's worth pointing out that VS Code may not open the welcome page again if you uninstall and re-install the extension (it caches the VSIX and also some state). I believe it only does that on first install.

Ok, I tried to avoid caching issues by uninstalling, closing VSCode, reopening VSCode and then installing, but that might not have been fully robust.

If you've already tried this hard before, feel free to close this as wontfix. The current situation definitely works fine.

mhuisi commented 1 month ago

Ok, I tried to avoid caching issues by uninstalling, closing VSCode, reopening VSCode and then installing

To my knowledge, the cache is permanent (or at least it definitely persists past closing VS Code).

If you've already tried this hard before

I think it's fine to keep it open. There's a work item somewhere in my backlog to replace the welcome page with a custom mechanism, and we can close this issue when that eventually happens.