Feature request: Jump to corresponding file and line in trouble.nvim diagnostics

[utensil]

When using lean.nvim with trouble.nvim (similar to VSCode Problems panel), it would be nice if clicking on a Lean error message could go to the corresponding file and line, currently clicking on something like

 error: ././././LibraryName/FileName.lean:112:4: error message

in the diagnostic output has no effect.

Context:

Zulip

More information:

To reproduce, assuming you have 2 files, A.lean and B.lean, and B imports A. Now introduce an error in A, e.g. a typo of a type. If we open A.lean with lean.nvim, trouble will have a diagnostic message that can successfully jump to the error line, e.g.

But if we open file B, as the error comes from A, B will have a long error at where A is imported, but no way to jump to the acual error line in A:

(some long warning omitted in between)

It can only jump to the import of A, which is difficult to dive in for the cause of the error in A.

[utensil]

In retrospect, I think it's unlikely for lean.nvim to support this, unless lean.nvim actively triggers an extra diagnostic for A even when A is not open, as the diagnostic for B could only jump to where A is imported, it can't have a second file location to jump to, except maybe if there is some kind of "nested diagnostic" design of Neovim and trouble.