search

Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
275 stars 26 forks source link

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

Open utensil opened 2 hours ago

utensil commented 2 hours ago

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.

image

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:

image

(some long warning omitted in between)

image

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

utensil commented 2 hours ago

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.