Discussion about Lean Graph

Stream: general

[Yury G. Kudryashov]

I'm starting a thread for discussion of the recently announced Lean Graph https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Introducing.20Lean.20Graph.200.2E1

[Yury G. Kudryashov]

First few questions:

• is it hard to automate generation of the json file using lake instead of opening some file in the editor?
• is there an offline version?
• is there a version that generates .dot files?

[Adam Topaz]

Am I missing something about the graph visualization itself? How does one zoom in? Right now I see this:
Screenshot-2024-01-02-at-10-18-36-Lean-Graph.png

[Yury G. Kudryashov]

Yes, I opened and the graph started to zoom out without any reaction(UPD: I can mov it but can't zoom in) to keys/mouse scroll.

[Patrik Cihal]

Adam Topaz said:

Am I missing something about the graph visualization itself? How does one zoom in? Right now I see this:
Screenshot-2024-01-02-at-10-18-36-Lean-Graph.png

"ctrl + scroll wheel" should work

[Yury G. Kudryashov]

I really prefer to look at static objects when I analyze something. Can I stop the animation?

[Adam Topaz]

That's quite unintuitive. Is there a good reason not to just use scrolling directly?

[Chris Birkbeck]

Is there a way to share the graph it creates (other than sharing the .json)?

[Yury G. Kudryashov]

Also, can you hide auxiliary lemmas like Nat.add._match_1?

[Patrik Cihal]

Yury G. Kudryashov said:

First few questions:

• is it hard to automate generation of the json file using lake instead of opening some file in the editor?
• is there an offline version?
• is there a version that generates .dot files?

There is an offline version, however for now it requires building the app from source (look on GitHub). Automating would be quite complex and would probably require running the Lean langauge server in WASM. Don't know what you mean by .dot files...

[Adam Topaz]

Sorry if I'm just being stupid: where is get_graph_meta.lean?

[Yury G. Kudryashov]

https://graphviz.org/doc/info/lang.html

[Patrik Cihal]

Yury G. Kudryashov said:

I really prefer to look at static objects when I analyze something. Can I stop the animation?

Yes, setting in Force settings there should be stiffness slider. Setting it to 1, should stop the animation, however you should let it run for a while in order to group related theorems together.

[Patrik Cihal]

Chris Birkbeck said:

Is there a way to share the graph it creates (other than sharing the .json)?

Not yet. It's something I will probably add in the future if there is interest however. Shouldn't be hard.

[Patrik Cihal]

Adam Topaz said:

Sorry if I'm just being stupid: where is get_graph_meta.lean?

That is a reference to the old name of the file, now it's called DependencyExtractor.lean, you can get it under the File section in the web app.

[Yury G. Kudryashov]

By "automating" I meant "create a command like the existing lake exe graph that creates a json file", not "create a json file right there on the website".

[Patrik Cihal]

Yury G. Kudryashov said:

By "automating" I meant "create a command like the existing lake exe graph that creates a json file", not "create a json file right there on the website".

That would probably end up more complex. You would need to specify the imports to the theorem/namespace first and wouldn't even get much feedback whether are you pointing to an existing thing.

[Patrik Cihal]

Yury G. Kudryashov said:

By "automating" I meant "create a command like the existing lake exe graph that creates a json file", not "create a json file right there on the website".

Plus the fact that it needs to analyze the stuff in the meta environment, I'm not sure how all that would work.

[Adam Topaz]

It's still very possible to do, but you probably will have to parse and compile the file in question from the IO command itself. This is something that IMO would be worth doing, as it would follow the standard lean project workflow as opposed to copying and pasting some lean file into each project.

[Adam Topaz]

there are examples of obtaining a lean environment from a file in lean-training-data, for example.

[Adam Topaz]

A hacked together bare-bones version can be found here: https://github.com/adamtopaz/lean_grader/blob/9838ec05c56b92b677c73322288f26634b7f4b62/Main.lean#L7

[Yury G. Kudryashov]

@Scott Morrison What do you think about :up: and its co-existence with your ImportGraph?

[Yury G. Kudryashov]

Is it better to keep them separate or to somehow merge them (the parts that extract the graphs)?

[Patrik Cihal]

Adam Topaz said:

It's still very possible to do, but you probably will have to parse and compile the file in question from the IO command itself. This is something that IMO would be worth doing, as it would follow the standard lean project workflow as opposed to copying and pasting some lean file into each project.

Interesting, so the user would download a separate executable in this scenario?

[Yury G. Kudryashov]

The user would add lean-graph as a dependency for their project and run something like lake exe graph --import Mathlib Nat.zero_add

[Adam Topaz]

No, the user would add the tool as a dependency to their lean project in the lakefile as usual

[Patrik Cihal]

Yury G. Kudryashov said:

The user would add lean-graph as a dependency for their project and run something like lake exe graph --import Mathlib Nat.zero_add

I see. That's definitely better way to do this.

[Patrik Cihal]

Adam Topaz said:

A hacked together bare-bones version can be found here: https://github.com/adamtopaz/lean_grader/blob/9838ec05c56b92b677c73322288f26634b7f4b62/Main.lean#L7

Does this utilize the cache of the project?

[Adam Topaz]

Yes the imports should come from the preexisting oleans

[Adam Topaz]

If you just want the env from some imports there is a function called withImports or something like that in lean core that would help

[Adam Topaz]

If you want to run the commands in a certain file, that’s more complicated and that’s where code like in the link or that can be found in lean-training-data would be used

[Adam Topaz]

docs#Lean.withImports

[Patrik Cihal]

Adam Topaz said:

If you want to run the commands in a certain file, that’s more complicated and that’s where code like in the link or that can be found in lean-training-data would be used

What commands and what file?

[Adam Topaz]

https://github.com/semorrison/lean-training-data/blob/e0072c48bd926e51c49a8d77667395d57fe076c0/TrainingData/Frontend.lean#L270

[Adam Topaz]

Adam Topaz said:

docs#Lean.withImports

That doesn't work, but this is what I was thinking of: docs#CoreM.withImportModules

[Patrik Cihal]

I could also compress the extractor file contents, onto one line, at which point anyone can just paste and copy it directly into the file without any needs of downloads. Maybe that's what I'll do instead. I think that may be even easier for the users

[Patrik Cihal]

But that extraction by running an executable could definitely be added later.

[Patrik Cihal]

Chris Birkbeck said:

Is there a way to share the graph it creates (other than sharing the .json)?

You can share visualizations now.

[Chris Birkbeck]

Oh great!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Hey, this is cool! I just wrote a much simpler (Graphviz) version of this for myself in order to organize a large Lean file. I was viewing a graph of all the definitions in that file. Can I do that here? And have you thought about what kind of graph analyses might help understand intra-module and across-module dependency structures, as well as refactor files so that definitions with fewer dependencies are moved up?

[Patrik Cihal]

Wojciech Nawrocki said:

Hey, this is cool! I just wrote a much simpler (Graphviz) version of this for myself in order to organize a large Lean file. I was viewing a graph of all the definitions in that file. Can I do that here? And have you thought about what kind of graph analyses might help understand intra-module and across-module dependency structures, as well as refactor files so that definitions with fewer dependencies are moved up?

You can either extract the graph that starts from a single constant, or that starts from all constants in a namespace. If you want to view only the graph made by definitions, that's easy. After you extract the graph and open the JSON containing the extracted graph, there is a Filter section in the web app, so just unselect everything except definitions.

I haven't thought about that. Right now, I visualize it as if all of them were in a single file.

[Jon Eugster]

nice visualisation!

[Jon Eugster]

Yury G. Kudryashov said:

What do you think about :up: and its co-existence with your ImportGraph?

First, there is a mathlib PR (#9169) to split lake exe graph into it's own repo, so it can be used in other projects. The project is here: leanprover-community/import-graph.

Quickly glancing at the code, I think it could very well make sense to merge the lean code of the two projects. The Lean code in this project seems quite concise.

I also see no obstructions that lake exe graph (with some args) could create this .json file, which is used for the dynamic web graph, on demand.

@Patrik Cihal I'll dm you to ask about your plans and maybe I can also help combining the functionalities of the two.

[Patrik Cihal]

Sounds good!

[Chris Birkbeck]

The website seems to be down, is this no longer supported?