Better import errors

[digama0]

This is not something I expect to get fixed overnight, but this is an issue to track improvements in import errors.

Currently, any errors in file A will cause file B that imports A to get an error at B.lean:1:1 which contains the dump of the lake invocation. This means that the error is both not localized to the actual failing import, and also the error itself is buried in a stream of other data.

If we play "what would Rust do", we shouldn't report import errors in file B at all, but rather we should put an error inside file A, while elaborating B, assuming we haven't already done so. LSP does allow you to do this. If A happens to be outside the project, then this may not be helpful, so in that case I would suggest putting the error on the import line for the first workspace file to import A.

[gebner]

See also the discussion at https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-dev/topic/LeanPaths/near/289386295

[Kha]

Which itself may be obsoleted by more recent discussion around integrating the language server into Lake.
It should be noted though that in contrast to rust-analyzer et al, the Lean 4 language server intentionally does not take a global, coherent view of the project. So there's no guarantee that import errors for A occurring in B are still actual errors in A and not from some previous version of the file.

[gebner]

I thought that was the last discussion on integrating the two, did a miss another one?

You're right about the need to show conflicting information though, when A has different errors from the worker and from the compilation attempt as a dependency. (This doesn't even need to be different versions of the file, it's also possible that the imported modules in the worker are out-of-date.)

[Kha]

Oops, without checking i assumed you linked to the previous discussion about extending the print-paths protocol https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-dev/topic/.5BRFC.5D.20Server.2FLake.20Import.20Interop

Btw, for --deps-json I did implement error reporting as I proposed in the above thread:

lean4/src/Lean/Elab/Import.lean

Line 47 in 7b7e2f5

errors : Array String := #[]

. It's a trivial extension.