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
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):
leanpkg.toml file says this
[package] name = "mathlib" version = "0.1" lean_version = "leanprover-community/lean:3.20.0" path = "src" [dependencies]
leanproject build gives
Building project mathlib configuring mathlib 0.1 > lean --make src
lean --make src doesn't say anything.
I tried many variants of
leanproject import-graph including running it from
~/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):
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
Patrick Massot (Sep 25 2020 at 12:26):
Maybe we should add an option to prune
Scott Morrison (Sep 25 2020 at 12:32):
Perhaps to delete everything "above"
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: May 11 2021 at 00:31 UTC