Updating Mathlib via VSCode menu does not work

Stream: general

[Michael Stoll]

I just had the following experience. In a project depending on Mathlib, I had updated Mathlib to v4.22.0-rc2. Now I wanted to update to the latest version (after a PR of mine was merged, so that I can use the new material it contains). So I commented out the rev = "v4.22.0-rc2 line in lakefile.toml and went to "Project actions/Update dependency". But I got a pop-up window saying that the dependency didn't need updating (even though another pop-up informed me that the extension had noticed that the configuration had changed).

Typing "lake update mathlib" in the terminal did work, though.

This is with v0.0.206 of the VSCode extension. After updating to 0.0.209, I don't even get the "Project actions" menu any more...?

@Marc Huisinga

[Ruben Van de Velde]

After changing the toml, did you restart code?

[Michael Stoll]

No. As far as I can remember, that hasn't been necessary (and I would think it bad UI design if it were).

After leaving and restarting code, the menu entry is still not there.

[Michael Stoll]

OK; the menu item appears when I'm on a Lean file, but not on lakefile.toml (maybe this can be changed?).

[Michael Stoll]

Hm. It does appear again after I make an edit to lakefile.toml...

[Marc Huisinga]

@Michael Stoll
vscode-lean4#637 ensures that the Lean-specific features of the VS Code extension activate when opening non-Lean files in a Lean project as well.

vscode-lean4#638 mitigates the specific 'Update Dependency' issue you ran into above (see the PR description for details).