Add code lenses to definitions showing amount of references

[Garmelon]

This seems to fail for structure definitions (though not for the structure's fields), and I haven't tested it a lot. It may also make sense to exclude type class instance definitions, since they're usually only used implicitly?

To make the code lenses clickable seems to require editor-specific code responding to the Command in the CodeLens. (Here is how rust-analyzer names its show-references code lens command)

I'm not entirely sure whether the definition itself should count as a reference. I think it makes more sense not to count it, but VSCode includes it when displaying references (note the 3 references code lens above VSCode's References (4)):

Finally, VSCode doesn't seem to update the code lenses immediately after a workspace/codeLense/refresh notification, but requires some sort of re-render of the file (e. g. switching to another file and back). I haven't yet tried to figure out how to fix this, or how other LSPs handle this situation, but it can get annoying quickly when editing structs/inductives.

[Kha]

I'm not entirely sure whether the definition itself should count as a reference. I think it makes more sense not to count it

I agree (and would assume other language servers do the same). The confusing display really is VS Code's fault.

[gebner]

Personally I find it extremely annoying to show the references as code lenses. They clutter the editor and don't show any information I couldn't very easily get otherwise. At the very least this needs a configuration option. (For comparison, the typescript language server also has such a configuration setting, that defaults to off. The python extension doesn't even have that option and never shows code lenses for references.)

[Kha]

A Lean.Option, to be passed in by the editor extension, seems sensible. Rust analyzer has a pretty thorough set of options, defaulting to off for references.

[gebner]

A Lean.Option, to be passed in by the editor extension, seems sensible.

There is also the initializationOptions field and the workspace/configuration request in LSP.

[Kha]

Ah, that probably makes more sense.

[Kha]

The OmniSharp code lenses, which are the ones featured in the VS Code docs, seem to default to on. As for usefulness, I will have to give it a try in practice, but I assume the intention is to give you information that you might otherwise not have looked up. A small helper function that for example ends up with 1 or even 0 references after a refactoring is suspicious and one might want to take a look at whether it should be eliminated.

[gebner]

A general issue with showing code lenses (and other highlighting) from ilean data is that it will be out-of-date and incorrect most of the time while editing since they're only updated when the file is finished compiling iirc. (If you insert a line, then all references below will be on the wrong line.)

[Kha]

Do you mean because of the information the watchdog has or because of when & how VS Code updates lenses? Currently new ilean information is sent to the watchdog whenever the file is completely elaborated, but we were thinking about splitting this into incremental updates after each command.

[gebner]

Currently new ilean information is sent to the watchdog whenever the file is completely elaborated

Yes, that's the issue I was worried about.

but we were thinking about splitting this into incremental updates after each command.

Just make sure you're not sending the whole ilean every time, like we do with the diagnostics. :-)

but I assume the intention is to give you information that you might otherwise not have looked up.

That's a very weak justification for a disruptive change. Anyhow, I tried to find issues documenting a rationale for enabling/disabling references code lenses in the vscode repo but couldn't really find anything. The commit introducing the references code lens did not help me understand their purpose either: microsoft/vscode#18205

[Kha]

Heh, there is no motivation in rust-lang/rust-analyzer#5836 either except for a few hearts and thumb-ups. Then I guess we'll just have to evaluate individually whether we find it useful enough to turn on :) .

[Garmelon]

The reason for structs not working is that the <struct>.mk definition appears on the same line as the struct's definition itself, even though it isn't actually present in the source file directly. The LSP server then detects two definitions on the same line and doesn't display a lens since it would be ambiguous what the lens refers to.

[Kha]

Structure constructors look like an interesting (but not unique) edge case. We definitely want clicking on RefInfo.mk references to go to the RefInfo declaration. Should it also be included in the references window though? One potential solution is to not store RefInfo.mk as an entity on the ilean level at all but immediately identify it with RefInfo, much like duplicate signature/body fvars are handled.

[Vtec234]

Personally I find it extremely annoying to show the references as code lenses. They clutter the editor and don't show any information I couldn't very easily get otherwise. At the very least this needs a configuration option.

I agree with Gabriel -- this effectively doubles the vertical space used by inductives and structures, and the same information can be easily obtained via 'find references'. I think code lenses do have their use cases:

give you information that you might otherwise not have looked up

Indeed this sounds like what we really want, but with the proviso that the information be usually actionable, ideally appearing together with an associated code action. For example, it's not really helpful to know that a definition has 5 or 6 references, but it could be helpful to know it has 0, i.e. it's dead code. However this is usually shown as a lint (i.e. a squiggly) in other languages (e.g. Rust), so does not imo justify a code lens. I would be okay with exposing this behind an off-by-default flag.

[Garmelon]

The way vscode handles code lens updates is a bit weird, so getting them to update properly when the file is changed is not easy.

First of all, vscode usually only resolves code lenses visible in the editor (or at least near the visible area?). It leaves a space for other code lenses so the editor doesn't jump around too much though.

After changing a file, vscode seems to re-request and then re-resolve the code lenses automatically. Also, when switching to a file (or re-focusing the editor), it seems to re-request and re-resolve the code lenses. However, it doesn't seem to react to workspace/codeLens/refresh (from what I can tell, still testing)? There seems to be the assumption that code lenses resolved after an edit notification must immediately resolve according to the new file state, and vscode only seems to update code lenses after an action by the user.

Because of the asynchronous nature of the FileWorker elaboration, it would maybe make sense to delay codeLens/resolve requests until the worker has found the corresponding definition again, or until it has reached the end of the file and ensured that there exists no corresponding definition (at which point a workspace/codeLens/refresh would definitely be necessary).

I think the reference code lenses should be disabled by default, as the jank while editing is annoying, but enabling them after editing or while browsing the code might be useful to some.

[Kha]

I'll close this for now because there is opposition and some technical hurdles to enabling it by default, and we don't support any kind of configuration yet. But we should revisit this in the future.