Setup guide can't actually be reopened

[meithecatte]

Description

After clicking "mark done", the setup guide doesn't reopen when requested.

Steps to Reproduce

1. Install the leanprover extension
2. See that it opened a helpful setup guide. The first step tells you how to reopen it – cool!
3. Click the "Mark done" button.
4. "Ah, that marks the entire thing as done, not just this dummy step"
5. Attempt to reopen the setup guide:

Expected behavior: The setup guide reopens as advertised.

Actual behavior: An "Activating extensions" notification is present for a few seconds. Nothing else happens.

Versions

Reproducible with vscode-lean4 v0.0.140 (latest release) and v0.0.143 (latest pre-release).

vscode version information:

Version: 1.88.1
Commit: e170252f762678dec6ca2cc69aba1570769a5d39
Date: 2024-04-15T16:24:54.129Z
Electron: 28.3.1
ElectronBuildId: undefined
Chromium: 120.0.6099.291
Node.js: 18.18.2
V8: 12.0.267.19-electron.0
OS: Linux x64 6.8.7-zen1-1-zen

Impact

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

[mhuisi]

I can't seem to reproduce this, unfortunately. What happens if you click 'More' in the general VS Code 'Welcome' page and then select 'Lean 4 Setup'? You can open the 'Welcome' page in VS Code using the builtin 'Help: Welcome' command (Ctrl+Shift+P > Type in 'Help: Welcome')

[mhuisi]

I managed to reproduce this once at some point and I wasn't able to open the 'Welcome' page anymore, either. I don't see how this issue could possibly be on our end though, and I haven't encountered it since.

Please comment on this issue if you are still encountering this problem.