Zulip Chat Archive

Stream: new members

Topic: leanproject import-graph

Jia Ming (Sep 24 2020 at 14:42):

Hello, I'm having trouble getting leanproject import-graph to work properly and I don't know what the problem is... I'm trying to find out the different dependencies of orders and filters but the import-graph command always show weird output. For example, after getting mathlib with leanproject get mathlib, running leanproject import-graph out.svg in the directory just gives me a long row of all the mathlib modules. and running leanproject import-graph --from order.basic only produces one node in the import_graph.dot file, order.basic.

Scott Morrison (Sep 24 2020 at 22:58):

If you want all the files that order.basic depends on (i.e. more fundamental files), you need to use --to rather than --from.

Scott Morrison (Sep 24 2020 at 22:59):

Could you verify that leanproject build succeeds in the directory you're running from? Perhaps tell us exactly which directory you're in, and show us the contents of leanpkg.toml (which should be in that directory).

Jia Ming (Sep 25 2020 at 10:59):

I'm in ~/Desktop/projects/mathlib. My leanpkg.toml file says this

name = "mathlib"
version = "0.1"
lean_version = "leanprover-community/lean:3.20.0"
path = "src"


Running leanproject build gives

Building project mathlib
configuring mathlib 0.1
> lean --make src

and running lean --make src doesn't say anything.

I tried many variants of leanproject import-graph including running it from ~/Desktop/projects/mathlib and ~/Desktop/projects/mathlib/src all of which returns a single node/row of output

Patrick Massot (Sep 25 2020 at 11:10):

I'm sorry I can't reproduce this issue.

Patrick Massot (Sep 25 2020 at 11:11):

What does leanproject --version tell you?

Jia Ming (Sep 25 2020 at 11:33):

leanproject, version 0.0.10

Patrick Massot (Sep 25 2020 at 11:42):

Which OS are you using?

Jia Ming (Sep 25 2020 at 11:51):

Linux Mint 20 Ulyana

Jia Ming (Sep 25 2020 at 11:53):

I tested graphviz on a dot file I found on this zulip server and it worked magnificently. It could be an OS problem cuz it doesn't work on my other computer with linux mint 20 (cinnamon) installed.

Jia Ming (Sep 25 2020 at 12:03):

hmm let me try on my windows dual boot

Patrick Massot (Sep 25 2020 at 12:03):

Here it works flawlessly on Ubuntu.

Scott Morrison (Sep 25 2020 at 12:22):

leanproject import-graph --to order.basic import.pdf

gives me

Patrick Massot (Sep 25 2020 at 12:26):

Maybe we should add an option to prune tactic.* files.

Scott Morrison (Sep 25 2020 at 12:32):

Perhaps to delete everything "above" tactic.basic?

Jia Ming (Sep 25 2020 at 12:54):

omg i must be doing something wrong, the exact same command as Scott Morrison's gives one node on my windows OS too.... leanproject get mathlib is the correct way to get mathlib right?

Patrick Massot (Sep 25 2020 at 12:58):


Jia Ming (Sep 25 2020 at 13:12):

Hmmm I'll try again next time when I'm more familiar with the system. I'll use my clumsily put together python script for now hahah. Thank you for your help!

Last updated: Dec 20 2023 at 11:08 UTC