Tactic hover and imports

Stream: general

[Damiano Testa]

When I hover over the name of a declaration, I can find the name of the module where that declaration is defined, which is great.

[Damiano Testa]

However, if I hover over a tactic I get the doc-string for the tactic, but not the module where the tactic is defined.

[Damiano Testa]

Here is an example:

example (a b : Nat) : a + b = b + a := by
        -- hover over `Nat.add_comm` to see `import Init.Data.Nat.Basic`
  exact Nat.add_comm ..
  -- hover over `exact`: no import shown!

[Damiano Testa]

Would it be possible to have some concrete module to refer to for tactics as well? I know that the syntax is extensible and it might get tricky, but probably there is some useful information that can be given!

[Damiano Testa]

For instance, could the hover show the module from there the doc-string comes?

[Johan Commelin]

Or the module where jump-to-defn would take you.

[Damiano Testa]

Yes, I am happy with having some import that has something to do with the tactic! Better answers will be loved more, but I'll be happy to try something out and see if it can be improved.

[Damiano Testa]

By the way, if you fell that more general pieces of syntax should get a similar treatment, I would also be happy to have a module references for commands!

[Julian Berman]

Note that go to declaration (as opposed to definition) will at least jump you to that module

[Julian Berman]

I'm not sure what keyboard shortcut that is in VSCode. Let's see...

[Julian Berman]

Oh, it's in the right click menu at least, so. That.

[Julian Berman]

It looks like peek declaration has no keyboard shortcut in VSCode but perhaps that gives you at least a temporary solution as well to wanting something like a hover. You can find that in the Keyboard Shortcuts menu (and then assign it whatever key you want)

[Damiano Testa]

Julian, thanks! I'll try this out as soon as I'm back at a computer!

[Damiano Testa]

Wow, thanks for the tip, Julian! Go to declaration also works when there is no doc-string!

[Damiano Testa]

This makes me think that it should be easy to also add the module information in the hover, but it certainly addresses most of my usage concerns!