Fancy hover for mathlib docs

Stream: mathlib4

[Geoffrey Irving]

If I'm using the VSCode plugin, and I hover over an operator or a function, I get full details for implicit arguments and such.

Would it be possible to get the same information into the mathlib web docs, with similar hover semantics? I realize that's a fairly big task, but it would be spectacular for understanding things, especially for lemmas that convert between different things with the same name.

[Yaël Dillies]

doc-gen used to be better in Lean 3. Can you check eg docs3#mul_assoc and see whether the information there is enough for your needs?

[Geoffrey Irving]

Not really. E.g., if I hover over one of the * instances or click on it, it says it's has_mul.mul. But the corresponding thing in VSCode hover would say that it's multiplying things of type G. This is important if there's a multiplication lemma that multiplies things of a variety of types.

Screenshot-2024-01-31-at-9.40.00AM.png

[Geoffrey Irving]

E.g., here's the types of a power operation using VSCode hover, with my cursor at the beginning of the proof block (which is semantically where the docs would want to operate as well, I think). Crucially, it lists the HPow types as ℝ ℤ ℝ.

Screenshot-2024-01-31-at-9.41.51AM.png

[Eric Wieser]

I think this is what LeanInk was intended to solve

[Eric Wieser]

But this is really hard to do well, because it requires either having:

• The full pretty-printed output of every declaration in mathlib available to download somewhere (this is likely enormous, certainly too large to embed statically)
• Lean running in browser (this is not particularly viable)
• A dedicated server to handle such queries against a running lean installation