Zulip Chat Archive

Stream: general

Topic: Dependency Graph


view this post on Zulip 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.

view this post on Zulip Eric Wieser (Jan 04 2021 at 10:31):

Do you care about dependent tactics too?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Henning Dieterichs (Jan 04 2021 at 10:36):

Do you care about dependent tactics too?

I'm fine with just the lemmas ;)

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jan 04 2021 at 10:38):

Again, leancrawler does that.

view this post on Zulip Patrick Massot (Jan 04 2021 at 10:38):

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

view this post on Zulip Henning Dieterichs (Jan 04 2021 at 10:39):

The python code is basically this, right?

view this post on Zulip Patrick Massot (Jan 04 2021 at 10:40):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 04 2021 at 10:46):

But not an argument against building another tool in Typescript

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Edward Ayers (Jan 04 2021 at 11:02):

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

view this post on Zulip Edward Ayers (Jan 04 2021 at 11:03):

Another dream is to have access to graph libraries like D3


Last updated: May 12 2021 at 04:19 UTC