Zulip Chat Archive

Stream: new members

Topic: leanproject import-graph


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

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

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

view this post on Zulip Jia Ming (Sep 25 2020 at 10:59):

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

view this post on Zulip Patrick Massot (Sep 25 2020 at 11:10):

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

view this post on Zulip Patrick Massot (Sep 25 2020 at 11:11):

What does leanproject --version tell you?

view this post on Zulip Jia Ming (Sep 25 2020 at 11:33):

leanproject, version 0.0.10

view this post on Zulip Patrick Massot (Sep 25 2020 at 11:42):

Which OS are you using?

view this post on Zulip Jia Ming (Sep 25 2020 at 11:51):

Linux Mint 20 Ulyana

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

view this post on Zulip Jia Ming (Sep 25 2020 at 12:03):

hmm let me try on my windows dual boot

view this post on Zulip Patrick Massot (Sep 25 2020 at 12:03):

Here it works flawlessly on Ubuntu.

view this post on Zulip Scott Morrison (Sep 25 2020 at 12:22):

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

gives me
import.pdf

view this post on Zulip Patrick Massot (Sep 25 2020 at 12:26):

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

view this post on Zulip Scott Morrison (Sep 25 2020 at 12:32):

Perhaps to delete everything "above" tactic.basic?

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

view this post on Zulip Patrick Massot (Sep 25 2020 at 12:58):

Yes.

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