Support `${workspaceFolder}` and similar variables in `lean4.toolchainPath` about vscode-lean4

[Kha]

If lean-toolchain could allow a relative path, that would also work for me.

Contributions welcome by the way :)

[mhuisi]

We want to remove this setting in the future. Is there another way that you can set up the project to use your modified version of Lean? (E.g. using Elan or your lean-toolchain file)

[eric-wieser]

If lean-toolchain could allow a relative path, that would also work for me.

The current elan override mechanism doesn't work because it is overridden by the lean-toolchain of subdirectories, while the current elan toolchain link doesn't work because it is globally scoped, so it is not possible to have two checkouts of my workspace on the same computer and use them in parallel.

[Kha]

The current elan override mechanism doesn't work because it is overridden by the lean-toolchain of subdirectories

How many are there that you can't repeat this for each subdirectory?

[mhuisi]

I assume hosting the modified version of Lean in a public GitHub repository and referring to that in your lean-toolchain is not an option (e.g. because the project is private)?

To be clear, I consider this to be an Elan issue. lean4.toolchainPath should never be used for any serious project setups. It's a quick and dirty hack intended for debugging.

[eric-wieser]

To be clear, I consider this to be an Elan issue.

That's fair. Is the intent for the extension to not know about toolchains at all in future, and just assume that lake or lean are on the path?

lean4.toolchainPath should never be used for any serious project setups. It's a quick and dirty hack intended for debugging.

Isn't it currently used by lean itself?

[Kha]

Isn't it currently used by lean itself?

No, we use toolchain link

[eric-wieser]

Ah, so does that mean it's not currently possible to have two configured (ie both set up for modification of their own lean files) checkouts of different branches of the Lean4 repository on the same computer?

[mhuisi]

Is the intent for the extension to not know about toolchains at all in future

We certainly want to move more in this direction, but there's still a couple of features that will need to rely on the toolchain version, unfortunately.