Local toolchain setting is intransparent and can't be reset about vscode-lean4

[Vtec234]

Why don't we just use a standard VSCode setting for the toolchain version? Local storage is useful for persisting internal objects, but it doesn't sound appropriate for user-controllable settings.

[tydeu]

But note that a Workspace settings ONLY applies to that work space, if you opened a different Lean 3 folder it will NOT apply the result of your previous Select Toolchain choice because it is a different workspace.

I would think this would be the desired behavior? Support for different toolchain settings for different workspaces seems ideal.

[lovettchris]

I agree we need to make it more clear when you have chosen something in Select Toolchain (this is why originally I wanted to edit your lean-toolchain file to make it very explicit what you just did. I stored it in the Workspace settings because you didn't want me to edit the lean-toolchain file. There is an undiscoverable way to "reset" your "Select Toolchain" choice and that is to select "Other..." and type just the word "lean". Now it will revert back to using your lean-toolchain file.

But note that a Workspace settings ONLY applies to that work space, if you opened a different Lean 3 folder it will NOT apply the result of your previous Select Toolchain choice because it is a different workspace.

[lovettchris]

Here's my proposed fix for this issue. First, the PR# #83 makes select toolchain less common by setting a (default) toolchain when there is no elan installed.

Then I added the following UI to show "(workspace override)" on the toolchain that is currently overriding the version in the current workspace:

and you can see there is now an explicit "Reset workspace override..." menu item, when the user picks this option the "(workspace override)" is removed and the folder falls back on the lean-toolchain specified in that folder or the (default) toolchain if there is one. After doing this Select Toolchain will show the following:

This is now implemented in PR# #83 since it was all closely related to changes already made there.