source code browser

Stream: general

[Johan Commelin]

Is there some way to easily turn a repo of Lean files into a hyperlinked bunch of HTML files? If we want to showcase some code to mathematicians, we should take into account that they have never heard of git or github before. Also, on github you can't click on an imported file, or a token, to go somewhere else. And we can't expect people who want to read some source files to install VScode before they are able to really use it.

[Johan Commelin]

So basically, I would like a read-only VScode that can easily be hosted somewhere. Just a bunch of static files.

[Kenny Lau]

I mean, for other languages (like Java) the corresponding website is grepcode

[Kenny Lau]

so I don't think things like this is very common

[Soham Chowdhury]

I think what @Johan Commelin has in mind is closer to Javadoc, Haddock, or agda --html.

[Mario Carneiro]

this has been a dream for some time

[Mario Carneiro]

My #explode command was actually working toward that goal

[Johan Commelin]

So, why is it easy in VScode?

[Mario Carneiro]

Currently it's a bit tough to get good data on what exists in a file

[Johan Commelin]

If VScode can figure out where to take me, if I Ctrl-click on something, can't it export a bunch of html files?

[Mario Carneiro]

Actually what you are describing sounds a bit different - the plan has been to show some abbreviated or expandable or indexed form of the file to make browsing easier

[Johan Commelin]

Ok, I guess that is harder.

[Johan Commelin]

I just figure that if Kevin publishes a paper, then he want to include a URL with a static view of his files that is easy to navigate.

[Johan Commelin]

GitHub isn't good enough.

[Soham Chowdhury]

It should be possible to dump source code into plain HTML files and then modify or hook into vscode-lean (I think) to use its symbol table to turn identifiers into links.

[Mario Carneiro]

I think Mizar has a pretty similar display to what you are suggesting, Coq too to some degree

[Mario Carneiro]

See, for example: http://www.mizar.org/version/current/html/polynom5.html#T74

[Soham Chowdhury]

https://agda.github.io/agda-stdlib/README.html
Just to be clear, @Johan Commelin, does this look like what you want?

[Soham Chowdhury]

Yeah, or that

[Johan Commelin]

Right, those are both good examples.

[Johan Commelin]

Althought the Agda one only has a bunch of comments and imports...

[Soham Chowdhury]

You can click on the imports to get to more interesting files.

[Soham Chowdhury]

Like this: https://agda.github.io/agda-stdlib/Category.Monad.html

[Johan Commelin]

I have very little fu in this regard. But it seems to me that it shouldn't be too hard to hack such a thing together, right?

[Mario Carneiro]

I really hope there is a more effective way to locate tokens than asking lean at each position what token is at that location (and where is it defined)

[Mario Carneiro]

otherwise this could take a really long time

[Johan Commelin]

Not longer then lean --make, right?

[Johan Commelin]

And this is something that you'll run only occasionaly.

[Johan Commelin]

So I really don't care about runtime.

[Mario Carneiro]

yes longer than lean --make

[Johan Commelin]

Ooh, hmmm

[Mario Carneiro]

I'm talking about asking lean at each character what is there, basically the software version of clicking everywhere to see what happens

[Johan Commelin]

But Lean stores this data already, right? We saw it sitting somewhere in some expr.

[Johan Commelin]

How does VScode figure this out? Only at runtime, when I click somewhere?

[Mario Carneiro]

Through the lean server API

[Mario Carneiro]

you click, VSCode sends lean a message asking "what is here", lean responds

[Johan Commelin]

I see. And that is going to be slow.

[Mario Carneiro]

if that is the only message you can send, then we are in trouble, but maybe there is a saner data structure being sent

[Soham Chowdhury]

Hm, isn't there a lexer/parser/AST-generator for Lean that we can hook into?

[Mario Carneiro]

see lean 4

[Mario Carneiro]

this is why many of the leandoc plans are waiting on lean 4

[Johan Commelin]

/me proposes :four_leaf_clover: as the default emoji for marking dreams and wishes that will be trivially realizable when Lean 4 emerges :stuck_out_tongue_wink:

[Mario Carneiro]

maybe we should make a list

[Johan Commelin]

Voila: https://leanprover.zulipchat.com/#narrow/search/.22lean.204.22

[Johannes Hölzl]

Apropos Lean 4: Leo gave a new talk at Galois inc. You find the slides on leanprover.github.io: http://leanprover.github.io/talks/LeanAtGalois.pdf Some new information about Lean4!

[Johannes Hölzl]

local constants are now called free variables :)

[Patrick Massot]

My Lean crawler does get access to some information. With more work we could maybe get something like what you want.

[Johan Commelin]

That would be really nice, Patrick!

[Patrick Massot]

I'm not sure it's worth the effort to fight Lean 3 here, but everyone should feel free to try

[Reid Barton]

I have a mostly working "API documentation" generator although I'm not sure yet that it is more useful than just reading the source files.

[Reid Barton]

I was hoping to look into how the editor integration works to see whether I could also produce hyperlinked source but I haven't gotten that far yet.

[Johan Commelin]

Cool! Please let us know if you get hyperlinking working!

[Reid Barton]

I do think probably the clearest use of such a tool is to advertise what we are doing in a way which is somewhat more transparent to people who are not already Lean users.

[Johan Commelin]

Right, and it might not be unthinkable that demand for such usage will increase in the next months. When the word spreads about the perfectoid project, and when more senior mathematicians hear about the teaching that Kevin and Patrick are doing.