program visualizer by Jonathan Blow

Stream: general

[Johan Commelin]

I'm watching a keynote by Jonathan Blow, in which he is demoing a program visualizer for all sorts of code quality metrics.

https://www.youtube.com/watch?v=IdpD5QIVOKQ&t=1166s

I think it would be really cool to have something like this for Lean code, and in particular Mathlib. We may not want the same metrics as he is using. But I can think of a whole bunch of metrics that would be useful in the Lean context.

[Bryan Gin-ge Chen]

If we can turn a Lean project into some kind of tree-like JSON object with nested subdirectories, modules, declarations with the numerical values that we're interested in attached to the declarations (or whatever we have as the child nodes), then from there it shouldn't be hard to build a similar interactive visualization using e.g. D3: https://observablehq.com/@d3/treemap/2

[Johan Commelin]

What is cool is that he can click on a node and it takes him to the source location. Sounds minor, but I think it massively changes how much one actually tweaks code, based on staring at the visualization.

[Johan Commelin]

I would be interested in seeing various forms of tech debt visualised like this.

[Damiano Testa]

The syntax of the commands does contain the location information, so there is certainly all that is needed for point-and-click to be available.

[Johan Commelin]

But how do you then open in the correct editor window?

[Damiano Testa]

I personally do not know, but Ctrl-Click takes you to places and this could use the same mechanism?

[Damiano Testa]

Also, if it is some external program, then code -r -g <file_path>:row:column from the commandline does the right thing for me. I imagine calling this from any external analyser would be easy to achieve?

[Johan Commelin]

Aah, does that allow you to specify the exact VS code window? Or should people only ever have 1 window open anyway?

[Damiano Testa]

I think that what is more important is figuring out what it is that we want to visualize: I am pretty sure that "prettifying" will not be the main technical point.

[Damiano Testa]

I am not sure. code -r means "recycle the open VSCode", but I do not know what happens if there are already multiple open sessions.

[Johan Commelin]

Damiano Testa said:

I think that what is more important is figuring out what it is that we want to visualize: I am pretty sure that "prettifying" will not be the main technical point.

I would start with nolint.json, and other forms of tech debt.

[Damiano Testa]

Right now, nolints are mostly un-documented functions, I think.

[Johan Commelin]

One thing I like about these visualisations is that you can measure things on a gradient. Not just: this style is fine, that style is forbidden.
You can see which files/dirs use very slow tactic calls. Or have superlong proofs. Or highly nested have-blocks.

[Damiano Testa]

How about figuring out uses of unfold in a file that is not where the definition is created?

[Johan Commelin]

Probably a lot of things wrt the module system can also be tracked and visualised

[Damiano Testa]

Ok, let's choose one simple example, and let's try to get it working!

[Damiano Testa]

Once the first one is ready, adding others will be likely straightforward.

[Julian Berman]

I have nothing to add to this conversation but it's a nice random bit of nostalgia + worlds colliding to see a Jonathan Blow talk on the Lean Zulip... I haven't seen this one but will have to give it a watch.

[Damiano Testa]

I do not know about external visualisers, but maybe if someone does, then simply knowing what format we should output would be almost the whole issue.

[Andrew Peterson]

I was just reading this thread and working on it: https://lean-experiment.vercel.app/mathlib.html I was doing it on web but we could put in vscode in a webview or whatever. Right now I just set it up to count bytes and filecount in different files.

[Johan Commelin]

Wow, that's cool.

[Damiano Testa]

Already hooking into that example something like

• proof length
• number of tactic calls
• distribution of tactic uses

would be very informative.

[Johan Commelin]

One reason I would like to have this external to VScode, is that you can then put it on a 2nd monitor. For some reason VScode doesn't like splitting a tab out onto a separate monitor.

[Johan Commelin]

Also, it would make it easier to connect to /

[Andrew Peterson]

The repo's at https://github.com/Andrewp2/lean-experiment btw, MIT license, I have it hosted on a vercel account (also there's some other stuff I'm working on the website, idk if we want to pull this out or w/e)

[Damiano Testa]

How about storing the syntax trees of all the commands into a file and then doing data analysis on that?

[Damiano Testa]

The whole tree for all the commands might be way too much information, but maybe we can agree on filtering out some parts of the tree.

[Johan Commelin]

@Damiano Testa How about this for an easy example: we show the file hierarchy, and the size of a node comes from its # loc. And then we color code according to number of porting notes in the file.

[Damiano Testa]

Ok, so basically, only the color coding is what is missing from the example above, right?

[Damiano Testa]

@Andrew Peterson how hard would it be to implement the color-coding?

[Damiano Testa]

To first approximation, porting notes can be simply a regex count.

[Andrew Peterson]

@Damiano Testa Should be pretty easy I think, as long as I can get the information in a json file or similar

[Damiano Testa]

Ok, so if you let me know an example format file, then I can produce the data.

[Damiano Testa]

Actually, when I read porting notes, I was thinking of adaptation_notes: the difference is that adaptation_notes are actual commands, while porting notes are comments.

[Damiano Testa]

This means that for porting notes, the count would only be a regex.

[Damiano Testa]

adaptation_notes could be counted exactly through parsing, but porting notes do not have this status.

[suhr]

You may also find this interesting: https://gtoolkit.com/
It has treemap views as well.

[Andrew Peterson]

https://lean-experiment.vercel.app/mathlib.html ok i added porting notes, adptation_notes, and notes total.

const portingNoteRegex = /porting note/gi
const adaptationNoteRegex = /#adaptation_note\b/gi

[Damiano Testa]

Is porting note case-insensitive? (It should be, I do not know if it is in the code above.)

[Andrew Peterson]

Yes, it's case-insensitive.

[Damiano Testa]

Sorry for the many requests, but would it be possible to filter out files that contain no matches?

[Damiano Testa]

Or at least sort files based on the number of notes.

[Andrew Peterson]

Ok, if you refresh it should filter out files that contain no matches. Idk if you want it so you can have it filtered or un-filtered, I can add that option if you want. I also added a view for comment ratio, i.e. ratio of comments to code.

[Damiano Testa]

This looks great, thanks!

[Damiano Testa]

I wonder if, to make this customizable, it would be reasonable to have your code generate its output reading an external file.

[Damiano Testa]

And the external file would contain the metrics to be used.

[Damiano Testa]

So, then we could produce all the metrics that we like and we could visualise them by just pointing your code to our files.

[Damiano Testa]

For instance, for porting notes, the file could contain a list of paths and counts.

[Damiano Testa]

json format was mentioned above, which would work and would probably be useful for more complicated metrics.

[Andrew Peterson]

It kinda already does that, I just have a build script running some regexes on a copy of mathlib i have locally that produces a JSON file, and then it visualizes that. So I think maybe I could modify it to do something like that

[Damiano Testa]

Ok, so if the URL of the json file could be an input, that would already be good!

[Johan Commelin]

Damiano Testa said:

Sorry for the many requests, but would it be possible to filter out files that contain no matches?

Instead of filtering them out, I would like to use the colour coding for this. My reasoning is that it will make it much easier to compare various parts of the library, and conclude "this corner is in a healthy state (wrt this metric), and that corner really needs some attention"

[Damiano Testa]

This way, we can produce the json files by meta-programming and then the data-producing part and the data-visualising parts are cleanly separate.

[Andrew Peterson]

Ok, I think I have it working. Actually some things seem a little strange but I'm still figuring it out. There's a schema on the page where you can upload your own JSON file, and then you can change the size and color of the treemap based on whatever properties you pick. it has an absolute and a relative coloring, so absolute is across the entire "level" you're looking at, while relative is relative to within a block, like relative within the "Algebra" block.

The coloring is orange is low, blue is high, and black is specifically 0. I think actually I'll flip that around because blue is closer to black IMO.

[Damiano Testa]

Thanks! I agree with your choice of flipping the colors!

[Damiano Testa]

I tried the Entries schema with your test file and it only uses extra, or, likely, I did not understand how to use it!

[Damiano Testa]

The tree schema appears to work as I would expect it, though.

[Andrew Peterson]

Try clicking in once, I think it's just mistaken about where the root is

[Damiano Testa]

Ah, yes! Clicking in and then Choosing the Demo dir fixes it!

[Damiano Testa]

Maybe, for the custom format, assuming that Mathlib is the root dir is not expected.

[Andrew Peterson]

Yeah, I'll change that, and I also think there's something up with the relative coloring mode.

[Damiano Testa]

Thanks a lot! Btw, this looks like it could be very useful! We'll have to play with some more interesting custom data, though.

[Andrew Peterson]

Ok I think I got that all fixed, I'm gonna head out for now

[Adam Topaz]

@Damiano Testa a while ago I wrote some code that might be useful: https://github.com/adamtopaz/lean_constant_data

[Adam Topaz]

I haven’t read through the whole thread yet though

[Bryan Gin-ge Chen]

@Andrew Peterson 's lean-experiment site is cool! It'd be interesting to try and parse the output of lake build -v to visualize build timings as well. Then presumably we could get something like this added to radar (?). cc: @Joscha Mennicken

Declaration-level build timings would be even better too, but is there a way to set_option trace.profiler true in every file without actually adding it to the source?

[Henrik Böving]

You can set it as an option the lakefile

[Henrik Böving]

And Radar already does this for core: https://speed.lean-lang.org/lean4-out/b3b33e85d38317eca940e4a9653660e9f8b5682a/

[Johan Commelin]

@Andrew Peterson thanks for the rapid iteration!

1. Do you have any idea how hard it would be to make this into a local web app, so that features like "ctrl/shift/whatever clicking a node opens the file in VS code" become feasible?
2. Would it be possible to have further nesting? Atm it seems that all nodes go at most 2 levels deep. But on a sufficiently large screen, I can imagine have all ~7000 files of Mathlib in 1 huge treemap, organized according to the directory structure.

[Snir Broshi]

FWIW I believe any website can open a file in VSCode using vscode:// urls (it just asks the user for confirmation)

[Bryan Gin-ge Chen]

Looking at the help page on vscode:// URLs, wouldn't the webpage somehow need to know the path to my mathlib4 directory too?

[Snir Broshi]

Good point, but I believe it can link to trigger some functionality the Lean extension, so only the extension needs to know where your Mathlib is

[Bryan Gin-ge Chen]

Johan Commelin said:

1. Do you have any idea how hard it would be to make this into a local web app, so that features like "ctrl/shift/whatever clicking a node opens the file in VS code" become feasible?

It looks like it should be pretty easy to run locally with the vercel dev command -- you'd probably just have to modify the URLs to somehow get VSCode to open them.

[Bryan Gin-ge Chen]

Ah, I guess it wouldn't be hard to have a text form or something on the page where you could enter the path to your local mathlib4 directory, then the page could use that in its vscode:// URLs

[Johan Commelin]

Or even Snir's approach? But I guess that would need functionality in the Lean 4 extension that's not there yet? So then the text form would be good for a v1

[Bryan Gin-ge Chen]

OK, I was able to get vscode:// links working in https://github.com/Andrewp2/lean-experiment/pull/1 . (The correct command to get the app working locally is actually npm run dev) Only tested a little bit so there might be some weird behavior.

[Bryan Gin-ge Chen]

Andrew merged my PR so you should be able to test it now: https://lean-experiment.vercel.app/mathlib.html

I recommend opening your mathlib4 directory in VSCode before clicking links to files from the site. Also, both the browser and VSCode will ask for your permission to proceed so there's a little bit of pop-up overload, but it does seem to work for most files.

There's a bug where some leaf rectangles don't link properly in VSCode: should be fixed in https://github.com/Andrewp2/lean-experiment/pull/2

[Andrew Peterson]

Cool, I'll try to get that merged in. I'm working on a tauri version so it can run on desktop

[Snir Broshi]

Why Tauri rather than a VSCode extension?

[Andrew Peterson]

It'll work with neovim/emacs, any editor if it's an external thing. But I could probably just do a vscode extension right after

[Snir Broshi]

In my experience, neovim/emacs users will refuse to download Electron/Tauri apps anyway

[Patrick Massot]

This is not true at all. I know dozens of neovim users and they all use a graphical web browser (except for blind people). With Electron there will be the reluctance to use of bloated slow software that has not much to do with neovim or emacs. But I don’t see any issue with using a Tauri app if there is something truly graphical to display.

[Snir Broshi]

I don't think you can make the claim "not true at all" about a statement prefixed with "in my experience".
You might have the opposite experience, but that shouldn't invalidate my own.
I will however contest that your experience might be biased as a neovim user, and point out that you equate "Electron" with "bloated slow software" which aligns with what I said.

Patrick Massot said:

I know dozens of neovim users and they all use a graphical web browser (except for blind people).

I don't see how this is related, although in the case of a browser I'd expect a correlation between neovim/emcas and using Firefox over Chromium based browsers.

[Snir Broshi]

In any case, the more the merrier, just thought I'd mention the possibility

[Gavin Zhao]

Very cool project! Small issue I noticed, when I hover on a top-level block (e.g. "Algebra") it says "0 LOC 0 PORTING NOTES", but I was expected to see the sum of all LOC and NOTES in its sub-rectangles.

image.png

[Gavin Zhao]

Also from the Rust source in tauri, is the analysis entirely textually based?

[Andrew Peterson]

@Gavin Zhao Just pushed a fix to that
Yup, just regexes/string matching

[Andrew Peterson]

So right now:
We have the website
There's a desktop/tauri version
And there's also a vscode extension. The VSCode extension just includes the treemap, not the rest of the website

The desktop version and vscode extension aren't published on anything, they're just in the repo and working on my machine. I'm working on getting a version that has a text box where you can put a regex in and it'll rescan and do the coloring for that, but there are some performance issues relating to rescanning the entire repo that I'm trying to fix now. I tried having a version that watched the folder, but I got rid of that and replaced it with a "rebuild" button that recalculated the JSON. I think in the end, most of the information we want we can only get at compile time anyway, so that'll just be a static file reproduced during compilation.

Right now everything is tied tightly to mathlib, just to get that working first before looking at other projects.

Both the desktop and vscode extension don't have that awkward double pop-up thing.

[Andrew Peterson]

https://github.com/Andrewp2/lean-experiment/issues/10 I opened an issue to talk about what metrics to include. I'm a beginner in Lean, so I don't know what metrics we want to capture exactly, so if you have any good ideas I can look into it.

[Gavin Zhao]

I think more opportunities lie in semantic analysis using InfoTrees and friends.

[Gavin Zhao]

Type-checking time will be an intersting one too :eyes:

[Andrew Peterson]

I technically have an infotree exporter, but it would take like 12 hours to actually export all the infotrees from mathlib. I might be doing something really dumb, but I'll keep looking into it and see if there's a way to get a good amount of information in 15 minutes instead of 12 hours.

[Andrew Peterson]

image.png
It took around 12 hours to run, but I got a snapshot of at least some information of all the infotrees. Unfortunately I've only tracked a few high level metrics for each file, the above image is showing size as "Infotree nodes total" and color as "infotree widget items".

I think tomorrow I'll try another export, but this time export the literal infotree data instead of just a high-level summary. If anyone cares to look, I pushed the JSON files including the infotree_treemap.json that is showed in this view here.

I think the reason why it's slow is just that InfoTrees have a ton of data. For example, Analysis/Asymptotics/Defs.lean has ~ 1400 lines, but nearly 150,000 InfoTree nodes. So assuming that holds across mathlib, there's approx 100 infotree nodes for each line of code.

[Thomas Murrills]

This is really, really cool! :) I have a wish list for what sorts of displays we could have, in case it's useful.

I would love to go one step deeper visualization-wise. There are, I think, two sorts of things that could reasonably be "atomic":

• individual commands
• individual declarations

Note that a command may correspond to between 0 and arbitrarily many declarations (but no declaration corresponds to multiple commands).

We could further group declarations by type (e.g. def, theorem, inductive, structure, etc.—these have internal meaning beyond the syntax of the command itself). Arguably we ought to group instances, even though this is not a declaration type per se.

Attributes that can be used to color or size declarations include the expression size of the value (if they have one) and type, their visibility (public, private, @[expose]), other modifiers, attributes, terms, tactics, and notations used during elaboration of the declaration, and performance-related measurements, such as heartbeats used, profiling of things like instance synthesis, and elaboration time.

Some of these performance measurements might be more easily associated with commands, so we'd want to think about the visualizations that would be available here!

Some more specific ideas

• Something that would be really cool, but of which I'm not sure of the feasibility: the ability to write a Loogle query, then show (either by color or size) the declarations (and/or modules which house them) which satisfy the query. E.g. the visualization could show me a map of all declarations which mention Nat in the type.

• It might be interesting to visualize the scopes and declaration dependencies in some visibility-aware way. The demo this is based off of colored declarations by whether they call out to other modules. For us, it could be interesting to see how big the imported and exported scopes are, and how they're used. E.g., within a module, we could show boxes for the number of publicly imported declarations, the number of privately imported decls (and the meta ones as well), boxes for each of the declarations, and color by visibility. (Ideally we could also turn off displaying the imported scopes when convenient.) Modules with many public imports and many public exposed declarations could then be identified as targets for module-system optimization. It's a bit difficult to know what to do for aggregation here, though...maybe the scale is just "more public"?

• For visualizing tactic use, we could indeed look at the infotrees—we're likely curious about what tactics the user has actually written, though, so we ought to cross-reference with the syntax trees. The infotrees are useful for associating tactics with parent declarations, though. And I can imagine that we might also want to "count" tactics that are used indirectly, e.g. via macro expansion or autoparams, which would only show up in the infotrees.

Other thoughts

I don't know what the implementation limitations are, but I do agree with Johan's sentiment earlier that it would be really useful to be able to see everything at once. I'm not sure if it makes sense to only see two layers down all the time, since the resulting grouping mostly reflects less-relevant directory organization as opposed to the "actual" module leaves. We might be two layers from the bottom in one rectangle and 5 in another. Normalization mitigates this somewhat, but can drown out important signals from individual modules. Perhaps we could specify the number of layers from the bottom instead of the top? Also, maybe simply different aggregations, such as taking the max of values across modules, could help in specific cases?

I'm also a little skeptical of the "miscellaneous" groupings in principle; it suggests some organization of the directory which is not really there, but blends in with the rest.

However, I have no idea if this is simply a necessity for implementation! :)

[Thomas Murrills]

So, I am thinking about what the lean side of the implementation here could look like, and what json it could emit! :) The implementation question I'd like to ask is how feasible it is to generalize the schema to have a structure like, e.g.,

• module
  • command*
    • declaration*

where, crucially, we would need the ability to special-case certain entries, and can have different views that take advantage of those special cases.

For example, we might want to regard an import as a command, and associate with it the size of the imported scope, what modifiers it has (public/meta/all), and what module it points to. None of this data makes sense for other commands; a visualization that made use of these fields would have to ignore other non-import objects.

So, is it reasonable to create a json file that has all of this data, then dynamically filter away the things we don't want? For instance, maybe we want to collapse the "command" level entirely and just view declarations. Would that be doable, or would we need to preprocess these to be separate if we want to be reasonably performant?

Likewise, can we go in the other direction, and create more groupings? Let's say we want to show declarations, but group them into rectangles with different-colored borders depending on whether they're defs, theorems, etc., which would (in this setup) be recorded in a field in the declaration json itself. Is grouping like this feasible to do on the web side, or would we need to embed this in the structure of the json from the outset?

Anyway, very excited about this, and I'd be very happy to contribute! :)

[Greg Shuflin]

Patrick Massot said:

This is not true at all. I know dozens of neovim users and they all use a graphical web browser (except for blind people). With Electron there will be the reluctance to use of bloated slow software that has not much to do with neovim or emacs. But I don’t see any issue with using a Tauri app if there is something truly graphical to display.

I typically use Neovim as my editor and I have no issue in principle with using a Tauri app. I'd much prefer it to a vscode plugin in fact because I don't use vscode.

[Andrew Peterson]

image.png
Ok, here's a version that gets rid of the 2-level thing so you can see all the leaf files at the same time. I had to change around the colors a little bit due to an issue with 1px size files and how borders work, so now if a value is exactly 0 it gets a light red/dark red color. This change enabled me to get rid of the Miscellaneous groupings, that was previously necessary to keep text from overlapping. Instead the text is now at the bottom. It also shows all the values associated with that leaf on hover.

I haven't heard of Loogle before, I'll have to take a look into it. The only major implementation limitation right now that I can think of is that on the website, the SVG and data has to be hosted somewhere, built during compilation, etc. If we're on the desktop/vscode extension and there's a local copy of mathlib then I can build new treemaps just right there on the client.

[Johan Commelin]

@Andrew Peterson This is really cool! Thanks so much!

One tiny request: filename paths are in all caps. Do you think you could change that, so that it reflects the mixed-caps names faithfully.

[Andrew Peterson]

@Johan Commelin Done!

[Andrew Peterson]

image.png
image.png

Ok updates:

I kept trying to export infotree data, but it kept blowing up no matter what I did, until I limited nodes by expr.sizeWithoutSharing to 50,000. Apparently at some points this can be over 3.3 GB inside a single string! I now have some summary metrics based on infotree metrics on my local machine. I haven't yet merged that data into the website but I could do that tomorrow. You can see the different metrics I've added so far in the screenshot.

I took a quick look at Loogle's internals, it seems plausible to integrate something like that directly into the vscode extension, if not literally through the Loogle CLI then just by slinging some code around until it works.

Just for fun, I made a 3d view of the treemap data formatted into the style of a city using Three.js as a part of Genuary. I even integrated the Rapier physics engine, so you can actually run into buildings and can turn gravity on. The city only contains information on LOC right now. It would be cool if one day I could advance it far enough where you could walk into each building and see the lean proofs inside, perhaps even with some diagrams and portals you could walk through to other buildings.

[Kevin Buzzard]

The mathlib metropolis!

[Robin Carlier]

The 3d view idea is insanely cool.

[Thomas Murrills]

Unless I’m misinterpreting, I think we should be able solve the InfoTree issue by handling them within lean, and only exporting from lean the metrics we care about! :)

[Bryan Gin-ge Chen]

This is a random thought but I wonder if we could incorporate this into radar somehow. @Joscha Mennicken recently added radar’s benchmark suite to mathlib in #33762 and there are instructions there for how to add new metrics, so maybe being able to see these visualizations on each benchmarked commit wouldn’t be too hard to add?

[Joscha Mennicken]

Radar is focused on lean/mathlib performance, and only tracks per-module file size (in lines) and build instruction count. It sounds like you would want more per-file info in the visualizations, but those would probably not be worth the cost of tracking them in the benchmark suite.

I think it makes sense for this kind of visualization to be a separate tool, though of course radar could link to visualizations like it already does for the lakeprof report.