Browsing lean files like agda ones in browser

Stream: general

[Rémi Bottinelli]

Hey! I know with agda it's possible to compile to html, and then you get a nice syntax-highlighted hierarchy of files where everything is clickable, leading to the definition. Is there a way to achieve the same with lean (more specifically mathlib) ? The difference to the official docs is that we'd see the source code in its entirety, and it would just be the source code, no javascript calling external resources. Thanks!

[Mario Carneiro]

like this?

[Rémi Bottinelli]

Almost: I'd like to be able to click on any lemma/def and be brought there too.

[Rémi Bottinelli]

As an example: https://www.cs.bham.ac.uk/~mhe/papers/ordinals/ordinals.html#8020

[Adam Topaz]

I agree it would be nice to be able to click lemmas and defs. But with lean it's very useful to see the local context as you step through the tactics, which is possible to do with the link Mario shared

[Adam Topaz]

Can we have both?

[Henrik Böving]

You can click things in the context view by the way.

[Henrik Böving]

Just not the lemma declaration itself but I can see whether that's fixable..

[Henrik Böving]

Hmmm, I don't think it is without some extra work unfortunately, the export by LeanInk does not differentiate between hovers on a lemma and hovers of a goal state so I cannot really know whether I am looking at a hypothesis with a local name or a hypothesis within a goal view. If we want to support it that is some extra work on LeanInks side whcih would in turn also drive it further into incompatibility with Alectryon

[Niels Voss]

I know this isn't really the same as reading the source code, but if you click on the "equations" button in the official docs, it tells you what the definition is (the code differs a bit from the actual code, as it seems to omit proofs).

[Niels Voss]

As a side note, do you know what allows GitHub to show references and definitions for some bits of java code when you click on it? It doesn't seem to work in the middle of code blocks, only on definitions. Something like this for Lean would basically be like what is suggested.
image.png

[Rémi Bottinelli]

Adam Topaz said:

I agree it would be nice to be able to click lemmas and defs. But with lean it's very useful to see the local context as you step through the tactics, which is possible to do with the link Mario shared

Yeah, the local context thing is very nice! without this interactivity, stepping through a proof without lean by your side is almost impossible I guess.

[Alex J. Best]

Niels Voss said:

As a side note, do you know what allows GitHub to show references and definitions for some bits of java code when you click on it? It doesn't seem to work in the middle of code blocks, only on definitions. Something like this for Lean would basically be like what is suggested.
image.png

See https://docs.github.com/en/repositories/working-with-files/using-files/navigating-code-on-github, I think the main repo is https://github.com/github/semantic/ which uses tree-sitter. @Julian Berman wrote a tree sitter parser for lean 4 (https://github.com/Julian/tree-sitter-lean) but I think we are probably quite a way away from nice github reference support at this point