lean4
lean4 copied to clipboard
leanprover
Better import errors
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.
See also the discussion at https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-dev/topic/LeanPaths/near/289386295
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.
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.)
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: https://github.com/leanprover/lean4/blob/7b7e2f54dab95825a78a0d6b4c9420e794c5931d/src/Lean/Elab/Import.lean#L47. It's a trivial extension.