Extension watches lean-toolchain files in subdirectories about vscode-lean4

[lovettchris]

I cannot repro this problem the following function has a check to see if the file changed is the "current" lean-toolchain being used by the project, if not then it is ignored.

    private async handleFileChanged(uri: Uri) {
        if (!this.leanVersionFile){
            this.leanVersionFile = uri;
        }

        if (uri.toString() === this.leanVersionFile.toString()) {
            const version = await this.readLeanVersion();
            if (version !== this.currentVersion){
                this.currentVersion = version;
                this.localStorage.setLeanVersion('');
                // raise an event so the extension triggers handleVersionChanged.
                this.versionChangedEmitter.fire(version);
            }
        }
    }

This is what I tried:

• load folder with a lean-toolchain at the root of the folder, and another lean-toolchain in a subfolder named Foo.
• Ensure the root version is being used.
• I then changed the lean-toolchain in the Foo folder

This caused the above code to execute but the if (uri.toString() === this.leanVersionFile.toString()) { caused it to skip and do nothing. So why do I look for all changes? In case the user deletes a file and the current this.leanVersionFile then moves to a different (perhaps inherited) file.

[gebner]

I tried this in the lean4 repository, which has neither a lean-toolchain nor a lakefile.lean (except in the src/lake submodule).

In case the user deletes a file and the current this.leanVersionFile then moves to a different (perhaps inherited) file.

Ah, so we actually look in the parent directories now? Cool. I think we should also do that on every file change event (instead of assuming that the changed file is now the new valid toolchain file).

[lovettchris]

Yes I do that already too, in response to the version change, the extension calls leanpkg.testLeanVersion which calls again to pkgService.findLeanPkgVersionInfo which walks up the hierarchy again, so it always uses the "best" file and if it is good, it raises an installChanged event which restarts the lean server, and when "lean --server" runs it seems to apply the same algorithm, searching up the folder hierarchy, so I think we're good.

[gebner]

Something's still not right then. When I open the lean4 directory in vscode, and then do cd src/lake && git checkout HEAD^^^^^^^^^, I still get a popup that the lean version changed. I'm pretty sure it's because we treat the first changed lean-toolchain file as the best file, even if it is in a subdirectory:

    private async handleFileChanged(uri: Uri) {
        if (!this.leanVersionFile){
            this.leanVersionFile = uri;
        }

[Kha]

The logic in getWorkspaceLeanFolderUri also looks a bit dubious - if a Lean file is part of a workspace, we should always use that workspace root to be consistent with the server (which is started from the workspace root, apart from #15).

[lovettchris]

When I open the lean4 directory in vscode, and then do cd src/lake && git checkout HEAD^^^^^^^^^

Yes, this is an odd case, lean4 has no toolchain, but it depends on a git submodule that does. So yes, this is picking up and using the lean-toolchain from lake. Is this not what you want though? What do you want in this case?

[lovettchris]

The logic in getWorkspaceLeanFolderUri also looks a bit dubious

Which part is dubious? Are you looking at this code?

        if (rootPath) {
            return Uri.joinPath(rootPath, '..');
        }

The reason for this the ".." is because the rootPath at this point is the full URI of the document which is something like file:///d%3A/Temp/lean_examples/Foo/Main.lean but we want the Uri of the folder containing this document.

[Kha]

As I wrote above, we should always look at the file in the workspace root if we're inside a workspace - both when listening for changes to it, and when actually reading the file. We can optionally do the upwards traversal in the case of non-workspace files, though I assume listening for changes doesn't work in that case because the API docs say it only works inside workspaces. In any case, this fringe use case should not affect the behavior inside workspaces, which is the important use case that we need to get consistent with the server.

[Kha]

More precisely, if we want to be fully consistent with elan, we could do an upwards traversal starting from the workspace root. This might be important if someone wants to manage multiple packages inside a single repo with a single lean-toolchain file in the repo root. Though again with the caveat that, if the traversal leaves the opened workspace(s), I believe the file watcher will cease functioning.

[lovettchris]

More precisely, if we want to be fully consistent with elan, we could do an upwards traversal starting from the workspace root

Great, that is exactly what findLeanPkgVersionInfo is doing. The only exception is when there is nothing in the workspace root and nothing in the parent hierarchy, which is the case that @gebner pointed to with the lean4 repo. I guess it is a bit inconsistent since it does not find the lean-toolchain in the lake submodule when you open lean4 but only when you change it with a git submodule update... So if you both want me to remove the "**/" I can easily do it...

[lovettchris]

Ok, I have fixed this in #83 (please try it again) - it now always applys the findLeanPkgVersionInfo algorithm no matter which file the file watcher found. I also fixed a bug in getWorkspaceLeanFolderUri so that if you open lean4 with D:\git\leanprover\lean4\src\lake\Lake\Version.lean in the editor it does NOT find the lake lean-toolchain file. Perhaps this is what both of you were seeing above which I agree is confusing. It now correctly uses workspace.getWorkspaceFolder(documentUri) to find the workspace folder and starts the search from there. So opening lean4 with no "(default)" toolchain installed now correctly shows this dialog: