Support of environment variables in lean.executablePath and lean.leanpkgPath

[letrec]

It would be nice if this "lean.executablePath": "${env:USERPROFILE}\\.elan\\bin\\lean.exe" worked. Currently have to specify absolute path like this: "lean.executablePath": "C:\\Users\\user\\.elan\\bin\\lean.exe".

[bryangingechen]

Yes, this would indeed be nice. This would best be done in VS Code itself. See these two issues: https://github.com/microsoft/vscode/issues/46471 and https://github.com/microsoft/vscode/issues/2809. However, we did implement a workaround for something similar in https://github.com/leanprover/vscode-lean/pull/134.

Note that if your .elan\bin directory is in your Windows path, the default values of lean and leanpkg should work (even in Windows, I just checked my setup). I understand that there may be reasons why you want to set things up differently though.

[letrec]

vscode-python supports this functionality for many its variables (python.condaPath, python.pythonPath, python.venvPath). https://github.com/microsoft/vscode-python/blob/bd942a0dadaed64061f0e4b6bb3d7bac6df5b2d2/src/client/common/configSettings.ts#L216 Not sure how easy it is to replicate this in vscode-lean.

[bryangingechen]

Thanks for the pointer. It looks like the meat of the code is here: https://github.com/microsoft/vscode-python/blob/bd942a0dadaed64061f0e4b6bb3d7bac6df5b2d2/src/client/common/variables/systemVariables.ts

We could probably just copy this into vscode-lean; I'll look into it in a few days (unless you'd like to take a shot at a PR?).

Edit: I probably won't get to this until next week at the earliest.