fix: #115 : Infoview not working for external file

[lovettchris]

Fixes #115

Turns out the work to support "untitled" files broke the "ad hoc" files. Now I've tested the following scenarios:

• start vs code from start menu (not from a folder), File/Open file..., works (let's call this an "adhoc" file).
• start vs code from start menu (not from a folder), File/New file, set Lean4... works (let's call this an "untitled" file).
• start vs code from folder, open files in that folder, works!
  • now File/Open file... from somewhere else, also works!
  • now File/New file & set Lean4, also works!

This last option now has 3 LeanClients running, one for the folder, and one for the adhoc package root, and one for 'untitled' files.

For "adhoc" files the extension searches upwards in the directory hierarchy for a Lean package root and creates a new LeanClient for that root.

[gebner]

In this case should we walk up the directory structure and find the Leanpkg.lean in lib\lean\src

If the user opens that IO.lean file directly, then this would be the ideal behavior. (Maybe look for something else than Leanpkg.lean though, because that file no longer exists in recent nightlies.)

When the user opens that file via go-to-definition, it would also be reasonable to associate it with the lean server from the other file. An argument for reusing servers is that find-references only works across the same server.

[lovettchris]

Maybe look for something else than Leanpkg.lean though

Right I meant to say I would be looking for the usual package files leanpkg.toml or lean-toolchain..

[lovettchris]

@gebner ok, I did a big cleanup on when and how we walk directory looking for Lean package roots, they are now stateless helper functions. This also cleaned up some redundant calls to testLeanVersion that happen on first Lean extension activation - so the first lean file now gets to running LSP state a bit faster than before. I also implemented the adhoc directory walk which seems to be working nicely. For example, I do an adhoc open of a file deep in mathlib4 repo and it correctly finds the math4 root and opens only one LeanClient for all of mathlib4 which is the right thing to do. So I think this PR is in good state now and ready to merge.

[gebner]

Please stick to either async or sync. Reading a small local file is fast enough that sync would be okay, but mixing them is not really helpful (since it could still block). The exists operation is also deprecated (and shouldn't be used together with readFile due to the race condition where the file is deleted between the exists and readFile calls).

So either:

try {
  fs.readFileSync(url, {encoding: 'utf-8'}).toString()
  // ...
} catch (err) {
  // could check for err.code === 'ENOENT'
  return null;
}

Or async, which is just as easy:

try {
  (await fs.promises.readFile(url, {encoding: 'utf-8'})).toString()
  // ...
} catch (err) {
  // could check for err.code === 'ENOENT'
  return null;
}

I would also try to drop the duplicate existsSync check in readLeanVersion.

[lovettchris]

Generally I agree with you but the only reason I didn't use exists() here is because it is deprecated for some reason. In general I prefer all IO to be async as hard drives and network drives can have random very long delays depending on what's going on and I hate apps that force me to wait for them to do synchronous IO... but if you feel strongly about it I can change this to readFileSync - it will have ripple effects all over removing async behavior up the chain.

[gebner]

No, no, I think we completely agree. Async is better, we should be using it.

but the only reason I didn't use exists() here is because it is deprecated for some reason.

Ah, but the recommended replacement is not existsSync, but access or stat. To quote the docs:

Stability: 0 - Deprecated: Use fs.stat() or fs.access() instead.

Also in our use case it's recommended to use readFile and catch the file not exists error:

Using fs.exists() to check for the existence of a file before calling fs.open(), fs.readFile() or fs.writeFile() is not recommended. Doing so introduces a race condition, since other processes may change the file's state between the two calls. Instead, user code should open/read/write the file directly and handle the error raised if the file does not exist.

[lovettchris]

Yes, you are right about the race condition, and thanks for the pointer to fs.stat(). I filed a new work item to clean this up across the code base.