Zulip Chat Archive

Stream: general

Topic: annotated lean files


view this post on Zulip Jason Rute (Apr 28 2020 at 12:05):

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

view this post on Zulip Jason Rute (Apr 28 2020 at 12:07):

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.

view this post on Zulip Jason Rute (Apr 28 2020 at 12:08):

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).

view this post on Zulip Jason Rute (Apr 28 2020 at 12:11):

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

view this post on Zulip Jason Rute (Apr 28 2020 at 12:19):

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 12:22):

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

view this post on Zulip Jason Rute (Apr 28 2020 at 12:24):

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!)

view this post on Zulip Mario Carneiro (Apr 28 2020 at 12:25):

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 12:26):

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 12:26):

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 12:27):

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

view this post on Zulip Jason Rute (Apr 28 2020 at 12:27):

Oh, I see.

view this post on Zulip Mario Carneiro (Apr 28 2020 at 12:28):

actually .\alpha might be in use somewhere

view this post on Zulip Jason Rute (Apr 28 2020 at 12:29):

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.

view this post on Zulip Jason Rute (Apr 28 2020 at 12:32):

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 12:40):

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

view this post on Zulip Jason Rute (Apr 28 2020 at 12:44):

how so?

view this post on Zulip Mario Carneiro (Apr 28 2020 at 12:45):

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

view this post on Zulip Patrick Massot (Apr 28 2020 at 12:45):

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).

view this post on Zulip Jason Rute (Apr 28 2020 at 12:49):

@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.

view this post on Zulip Jason Rute (Apr 28 2020 at 12:50):

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

view this post on Zulip Mario Carneiro (Apr 28 2020 at 12:50):

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

view this post on Zulip Patrick Massot (Apr 28 2020 at 12:52):

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

view this post on Zulip Marc Huisinga (Apr 28 2020 at 12:55):

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 ...)


Last updated: May 13 2021 at 22:15 UTC