vscode-lean4 + elan prompting

Stream: lean4

[Julian Berman]

I recognize this isn't the fully supported setup (not having elan installed), but just out of curiosity nonetheless, can I get VSCode to not prompt me to install elan each time I open a project, particularly if the project uses the right version for the version of Lean installed?

[Kim Morrison]

I suspect Marc might merge a PR that allowed this, as long as there was no risk any reasonable user would ever enable it. :-)

[Marc Huisinga]

Julian Berman said:

I recognize this isn't the fully supported setup (not having elan installed), but just out of curiosity nonetheless, can I get VSCode to not prompt me to install elan each time I open a project, particularly if the project uses the right version for the version of Lean installed?

You can disable the 'Lean 4: Show Setup Warnings' setting. This will not disable any of the errors (Git/Curl/Lean/Lake not installed) and it will not disable the "missing Elan" error you get when attempting to create new projects using the VS Code extension, as we really need Elan for +toolchain flags there.

[Julian Berman]

Thanks, that's perfect!