Feature: Declarative IDE Hints

[enigmurl]

I am interested in this project and would like to offer help. In particular, when working on lean I have often felt that in addition to an interactive proof, it would very helpful to have live annotations at several places through the document.

For instance, in something similar to #check, rather than having to scroll over check, it would be nice if it just always appeared, similar to Rust type hints if you've ever seen it in RustRover. Below, the /- -/ denote where the IDE annotations would go.

theorem example_lemma (h: 1 ≤ 2) : 2 ≤ 3 := by sorry 
#check example_lemma /- (h: 1 ≤ 2) : 2 ≤ 3 -/

Similarly, rather than having to move cursor to see the proof goal, it would be helpful if the goal for various parts of the proof were shown automatically (in particular whenever the main goal changes, or some other heuristic). Say, something like this:

theorem a_le_b (h : a ≤ b) : 0 ≤ b - a := by
  /- 0 ≤ b - a -/
  suffices a + -a ≤ b + -a by
    rw [add_right_neg] at this
    rw [sub_eq_add_neg]
    /- 0 ≤ b + -a -/
    exact this
  apply add_le_add_right
  exact h

Does this sound interesting? If so, I would be willing to help out with development.

[onriv]

@enigmurl Thans for the first issue! Yeah I did not use RustRover before but I am using Intellij Idea quite frequently. Indeed I think keeping these infomation inside the editor is interesting and sweet. In this way it maybe more focusing on the workflow. But currently there are some hard parts for the implementation maybe.

1. Sometimes the status and goals for a proof in lean can be quite big. I am not sure if it's helpful in these cases or not.
2. I found that Inlay Hints and [the SDK document]() seems the IJ way to put these extra infomation insdie the editor. But currently it seems no cases that puts a multiline infomation (sometimes quite big) inside the editor and I dont know if it's possible.
3. The inlay hints implementation seems quite related to PSI. But currently the project does not involve any PSI relavant codes yet. I don't know how lsp4ij handles this though. It seems this is also relevant to https://github.com/redhat-developer/lsp4ij/issues/382
4. There is also something like LineExtensionInfo in intellij-community. It seems easier to integrate but maybe not enough for this case since it only contains one line.
5. There is also Inline Debugger but no sdk document for plugin doing things like this.

Yeah so it's interesting but maybe hard. Currently I am still working on the some more basic functionalities. Yeah if possible you can check the currently codebase and see how to do this! Feel free to contact anytime here or zulip!

[angelozerr]

Displaying those information is possible with LSP Inlay Hint. If your language server can support inlay hint, LSP4IJ will render it.