feature request: "go to next problem" should work on errors in imported files

[kim-em]

Suppose A.lean has an error, and B.lean imports A.lean.

If I have only B.lean open in VSCode, then I don't really get an actionable error. Jump to next error (F8) only takes me to the first line of B.lean, and then I have to read the lake output in the hover, identify the relevant file, and then open that.

It would be great if there was a convenient way to directly open A.lean at the underlying error.

I'm not certain that it should be F8 that does this. If it is, then Mario suggests that perhaps we could place the error squiggle from A.lean in B.lean: then F8 would hopefully open A.lean.

[antonkov]

Probably not fully resolving this, but DiagnosticRelatedInformation can be useful to point to the underlying error. It's displayed in the hover message as the link which opens the related file on click

My initial thought is to patch interactiveDiag to include DiagnosticRelatedInformation somewhere in compileHeader. @mhuisi do you think it's reasonable to look at as a first issue? Also please let me know if my suggestion is completely off or you have a better approach in mind :) otherwise happy to look more into that issue