Error when updating Mathlib

Stream: mathlib4

[Michael Stoll]

I just tried to update Mathlib in EulerProducts via the ∀ menu and got the error message

Cannot read 'lake-manifest.json' file at /home/mstoll/.elan/toolchains/leanprover--lean4---v4.14.0-rc2/src/lean/lake-manifest.json.

which is a bit strange, since there is no lake-manifest.json there (so the error is sort of OK, but why was it looking for this file?).

Updating manually on the command line via lake update mathlib afterwards worked OK.

[Marc Huisinga]

I assume you had a file from core open and focused when trying to update Mathlib?

The VS Code extension figures out the project to execute commands in from the tab that is currently active. If you had a tab with a core file open, it will attempt to run the update in core, which obviously doesn't have a lake-manifest.json file.

Could you create an issue in vscode-lean4 to improve this error message for this kind of common mistake?

[Michael Stoll]

The only files I had open were from my project, plus (apparently, without me noticing) the "Welcome" tab with the "Lean 4 Setup" (no idea where this came from). Could this have a similar effect?

[Marc Huisinga]

No. If you really had a file from your project open and not one in core, it should attempt to update your project.

Can you still reproduce this issue reliably?

[Michael Stoll]

After having updated manually, I cannot reproduce it now.