Zulip Chat Archive

Stream: general

Topic: Browsing lean files like agda ones in browser


Rémi Bottinelli (Jan 07 2023 at 05:15):

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 (Jan 07 2023 at 05:26):

like this?

Rémi Bottinelli (Jan 07 2023 at 05:32):

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

Rémi Bottinelli (Jan 07 2023 at 05:34):

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

Adam Topaz (Jan 07 2023 at 15:09):

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 (Jan 07 2023 at 15:09):

Can we have both?

Henrik Böving (Jan 07 2023 at 15:16):

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

Henrik Böving (Jan 07 2023 at 15:17):

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

Henrik Böving (Jan 07 2023 at 15:59):

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 (Jan 07 2023 at 20:12):

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 (Jan 07 2023 at 20:14):

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 (Jan 09 2023 at 09:32):

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 (Jan 09 2023 at 11:08):

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


Last updated: Dec 20 2023 at 11:08 UTC