annotated lean files

Stream: general

[Jason Rute]

I made a project which annotates Lean files with all of the information from the Lean server shown graphically for every file in Lean core init and mathlib.

Screen-Shot-2020-04-28-at-8.04.08-AM.png

[Jason Rute]

I don't know that this is of interest to anyone, but I made it as a way to debug the information I was extracting from the Lean server in this project.

[Jason Rute]

If you are interested in using the Lean server programmatically (for example, through the new Lean client for Python) it is an easy way to see what information is available (and how messy it is).

[Jason Rute]

This isn't meant to compete with useful tools like Format Lean.

[Jason Rute]

I did find a weird quirk. Sometimes the last letter in a projection (if I'm using the right term) doesn't have any information. I don't know that this matters for vs code, but it is worth mentioning. For example, here is an example in algebra/archimedean.lean.
Screen-Shot-2020-04-28-at-8.18.57-AM.png

[Mario Carneiro]

I'm curious what that looks like if you throw some unicode in there

[Jason Rute]

What do you mean? If you have a file in mind, you can look at them all here. Many of the unicode characters show up. Some with better fixed width than others. (Fonts are hard!)

[Mario Carneiro]

I was thinking more of mocking up a small test file, rather than looking for good examples in mathlib

[Mario Carneiro]

I am wondering if it is still off by 1 character if the name of the projection has a unicode character in it

[Mario Carneiro]

because this is probably an off by one error in the accounting

[Mario Carneiro]

I don't think mathlib has any projections with unicode names

[Jason Rute]

Oh, I see.

[Mario Carneiro]

actually .\alpha might be in use somewhere

[Jason Rute]

Also it isn't always that way. If you look at algebra/archimedean.lean, you will see that sometimes the final p in .imp is missing information and sometimes it is not.

[Jason Rute]

Also, for those that just want to browse, if you hover over the annotations, you can see the information they display. (I used pp.all=true for the data by the way).
Screen-Shot-2020-04-28-at-8.31.51-AM.png

[Mario Carneiro]

I notice also in algebra/archimedean.lean that all the spans are messed up on L85-90

[Jason Rute]

how so?

[Mario Carneiro]

besides all being useless things talking about the exact tactic, they are mostly pointing at whitespace

[Patrick Massot]

This is a nice project! At some point I think we should have a way to produce the API docs including the full annotated source (hidden by default of course).

[Jason Rute]

@Mario Carneiro This is a quite common occurrence. The behavior seems to be that if it is inside of a tactic parser (terminology?) for, say, the exact tactic. Then every character which is not associated with something else is coded for that tactic. Since this is designed as a language server, I don't know if this enables certain behavior in vs code and emacs or if it is a bug.

[Jason Rute]

It even gets weirder when you have tactics inside tactics inside terms inside tactics. :slight_smile:

[Mario Carneiro]

I expect that you are the first person to try to visualize the data like this, and doubtless you will find many bugs

[Patrick Massot]

We should ping @Marc Huisinga who seems to be related to Lean 4 server mode.

[Marc Huisinga]

don't worry, i read pretty much everything on here! unfortunately i can't exactly say much about the server mode yet since i'm still working on getting the necessary glue code in place to get some very basic functionality (ideally so i can at least transition from emacs to vscode ...)