leanproject import-graph

Stream: new members

[Jia Ming]

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]

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]

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]

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

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

[dependencies]

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]

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

[Patrick Massot]

What does leanproject --version tell you?

[Jia Ming]

leanproject, version 0.0.10

[Patrick Massot]

Which OS are you using?

[Jia Ming]

Linux Mint 20 Ulyana

[Jia Ming]

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]

hmm let me try on my windows dual boot

[Patrick Massot]

Here it works flawlessly on Ubuntu.

[Scott Morrison]

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

gives me
import.pdf

[Patrick Massot]

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

[Scott Morrison]

Perhaps to delete everything "above" tactic.basic?

[Jia Ming]

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]

Yes.

[Jia Ming]

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!