VS Code Extension Settings

Stream: lean4

[Marc Huisinga]

In the Lean 4 VS Code extension, there are several config settings where I am not quite sure what they are used for in practice or whether they are still being used at all.

If you or someone you know uses any of the following settings, please let me know:

1. lean4.toolchainPath: Used to override the Lean toolchain path. Could probably be replaced by using elan override instead?
2. lean4.enableLake: Can be used to disable Lake. Does anyone do this?
3. lean4.lakePath: Can be used to use a custom version of Lake. Could be replaced by calling VS Code with an adjusted PATH. @Mac Malone added this originally for debugging Lake; do you still use it?
4. lean4.serverEnv and lean4.serverEnvPaths: Used to add environment variables and paths to the PATH env variable. Could probably be replaced by calling VS Code with the corresponding environment variables, since the server inherits VS Code's process environment?

[Mac Malone]

@Marc Huisinga To (3) and (4), I added lean4.lakePath, lake4.serverEnv, lean4.serverEnvPaths a while back largely to help debug various Lake interactivity issues and to support precompileModules. While they could technically be solved by augmenting the environment, that is very inconvenient to do on Windows and also requires restarting the whole of VSCode each time. Luckily, there have not been very many interactivity issues with Lake recently, so I have not had to use them much recently, but I would like to keep at least lakePath around for future debugging. I am not sure if anyone else uses them.

[Marc Huisinga]

Mac Malone said:

Marc Huisinga To (3) and (4), I added lean4.lakePath, lake4.serverEnv, lean4.serverEnvPaths a while back largely to help debug various Lake interactivity issues and to support precompileModules. While they could technically be solved by augmented the environment, that is very inconvenient to do on Windows and also requires restarting the whole of VSCode each time. Luckily, there have not been very many interactivity issues with Lake recently, so I have not had to use them much recently, but I would like to keep at least lakePath around for future debugging. I am not sure if anyone else uses them.

Okay, I'll leave these settings for now, but will not support them for new features. Eventually, I'll replace all of them with a general setting that can add general environment variables to process.env and prepend entries to PATH in process.env without having to restart VS Code, which should hopefully cover all of these debugging needs.