Dependency Graph

Stream: general

[Henning Dieterichs]

Is there a way to extract a dependency graph of all lemmas in some folder? (like this: https://leanprover-community.github.io/sphere-eversion/blueprint/dep_graph.html) It should consider @[simp] lemmatas.
Would love to integrate such a dependency graph into VS Code (like the info view) where you can click on lemmas to jump to their definition.

[Eric Wieser]

Do you care about dependent tactics too?

[Eric Wieser]

For lemmas, presumably you could "just" look at the term-mode proof for the lemma, and extract all the symbol names

[Patrick Massot]

The sphere eversion dependency graph is not generated by Lean (it couldn't be since it most of the project is not yet in Lean). It's generated by plasTeX.

[Patrick Massot]

What you want is closer to what leancrawler is doing. It generated the graph on the perfectoid home page for instance.

[Henning Dieterichs]

Do you care about dependent tactics too?

I'm fine with just the lemmas ;)

[Henning Dieterichs]

Eric Wieser said:

For lemmas, presumably you could "just" look at the term-mode proof for the lemma, and extract all the symbol names

Is there some lean command that does this? Should I use the lean CLI + a custom tool that parses the output?

[Patrick Massot]

Again, leancrawler does that.

[Patrick Massot]

The Lean side is https://github.com/leanprover-community/leancrawler/blob/master/src/leancrawler/deps.lean

[Henning Dieterichs]

The python code is basically this, right?

[Patrick Massot]

Yes. It parses a YAML file created by the Lean side.

[Patrick Massot]

To be honest I don't really remember the current state of this project, but I know Daniel Selsam used it more recently than I did.

[Henning Dieterichs]

Sadly, I don't know any python. Also, I think for integration into vscode, a typescript implementation might be more suited since vscode ships nodejs. Given the current size of the python codebase in lean-crawler, what do you think of a rewrite in typescript? I guess it shouldn't take longer than an evening.

[Patrick Massot]

Sure, this is a very simple project, and the python code gather statistics you don't care about in your project. However I should warn you that those graphs grow very fast. I'm afraid you won't have anything readable except in the simplest examples. You can watch the first part of my Pittsburgh talk last year for comments about that.

[Eric Wieser]

I'd be slightly tempted to integrate leancrawler into doc-gen, which is an argument for it remaining in python

[Eric Wieser]

But not an argument against building another tool in Typescript

[Henning Dieterichs]

I guess it also reports all definitios/lemmas inside of mathlib? Maybe some heavy filter could reduce the size. I don't know what a typical lean project looks like though.

[Henning Dieterichs]

I'm currently at about 120 lemmas and theorems for my program verification proof - I think it could be insightful to see their dependencies live in vscode. I guess this size is still very manageable.

[Alex J. Best]

Something in vscode that shows dependencies between lemmas even within the current file seems pretty useful.

[Bryan Gin-ge Chen]

It should be possible to make something useful with the Lean 3 widget framework and the Lean code in leancrawler. Making a nice-looking graph will probably be a pain since widgets can't currently call external JS libraries, though.

[Henning Dieterichs]

I already had a quick look at the widget framework. I would like the dependency view to be non-invasive and asynchronous though (i.e. I don't want the graph export to affect the proof checking and vice versa). The graph also shouldn't be rendered inside the info view but rather in its own view. I guess this makes it somewhat unsuitable for the widget framework?

[Edward Ayers]

Yeah that's right Henning. Async rendering and having custom windows is currently still 'future work'.

[Edward Ayers]

Another dream is to have access to graph libraries like D3