Error message for non-existent file

Stream: lean4

[Julian Berman]

Very minor, but right now the error message for importing a nonexisting file within a correctly existing package returns a bit of a verbose error that mentions lake (with what I assume is considered an implementation detail of the import system?), e.g.:

1. `/opt/homebrew/Cellar/lean@4/HEAD-d5e05f3/bin/lake print-paths Init Mathlib.Not.Exist` failed:

   stderr:
   error: no such file or directory (error code: 2)
     file: ././Mathlib/Not/Exist.lean
   error: build failed

Is it reasonable to ask whether that can be shortened to just something like ./Mathlib/Not/Exist.lean does not existperhaps?

[Mac]

In order to provide a more concise error message here, the server would need to some how parse the result of the lake print-paths process to discover what the error was. Conceivably this could be done by augmented the JSON output with more information. I will talk to Sebastian and the other Lean devs to see if this whole interop could be improved.

[Julian Berman]

Another one to mention, which is more me being really dense :( so not sure if it can be improved -- I just wasted ~15 minutes trying to figure out why the heck I kept seeing "unknown package Test" in my editor, then repeatedly seeing lake build works just fine and scrambling to figure out the mistake

[Julian Berman]

The reason it turned out was because I had the wrong root dir when starting up the LSP. Of course this is me being bad because I knew and forgot that I needed to update that logic for Lake (which now of course I'm about to do)

[Julian Berman]

I don't know how to better detect that -- I guess LEAN_PATH was probably totally wrong and there was no package at all in the directory that was being used, but even a hint of that would have made my denseness go away sooner I suspect

[Scott Morrison]

The corresponding mistake with Lean 3 (either opening a single file, or opening a folder other than the one containing leanpkg.toml) is a perennial mistake, and we have to walk people through solving it on zulip frequently.

[Scott Morrison]

Having the VSCode Lean 4 extension volubly and helpfully identify this problem would be very helpful. Perhaps something for @Chris Lovett to look at?

[Julian Berman]

I think the VSCode extension should probably copy the logic we do in lean.nvim and then it becomes a lot easier for users -- unless of course that logic is wrong (which now I've fixed for neovim after the above) -- but I think the same root dir discovery should be possible in the VSCode extension too

[Sebastian Ullrich]

We actually have some logic for hinting at the correct directory to open in the server: https://github.com/leanprover/lean4/blob/3546104959f6048adfcbde5e72a1ca98abf03e6f/src/Lean/Util/Path.lean#L84-L92
But it's not triggered when using a package manager.

[Patrick Massot]

I've been meaning to write this for a while actually: one of the big surprises when I tried the Lean extension for vim was the total disappearance of this "open correct folder" issue. We had this issue so many times with beginners that I sort of assume it was unavoidable. Fixing this in the VSCode extension would be wonderful.