## Stream: general

### Topic: Dependency Graph

#### Henning Dieterichs (Jan 04 2021 at 10:13):

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 (Jan 04 2021 at 10:31):

Do you care about dependent tactics too?

#### Eric Wieser (Jan 04 2021 at 10:31):

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

#### Patrick Massot (Jan 04 2021 at 10:32):

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 (Jan 04 2021 at 10:33):

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

#### Henning Dieterichs (Jan 04 2021 at 10:36):

Do you care about dependent tactics too?

I'm fine with just the lemmas ;)

#### Henning Dieterichs (Jan 04 2021 at 10:38):

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 (Jan 04 2021 at 10:38):

Again, leancrawler does that.

#### Henning Dieterichs (Jan 04 2021 at 10:39):

The python code is basically this, right?

#### Patrick Massot (Jan 04 2021 at 10:40):

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

#### Patrick Massot (Jan 04 2021 at 10:40):

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 (Jan 04 2021 at 10:43):

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 (Jan 04 2021 at 10:45):

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 (Jan 04 2021 at 10:46):

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

#### Eric Wieser (Jan 04 2021 at 10:46):

But not an argument against building another tool in Typescript

#### Henning Dieterichs (Jan 04 2021 at 10:47):

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 (Jan 04 2021 at 10:51):

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 (Jan 04 2021 at 10:52):

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

#### Bryan Gin-ge Chen (Jan 04 2021 at 10:57):

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 (Jan 04 2021 at 11:01):

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 (Jan 04 2021 at 11:02):

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