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.

Reproduce the file A/file B import-error case described in the issue and inspect how LSP reports diagnostics during elaboration. Done means errors are localized to A when possible, or to the import line for the first workspace file when A is external, rather than reported only at B:1:1 with the lake dump.