Zulip Chat Archive

Stream: general

Topic: leanproject import-graph


view this post on Zulip Scott Morrison (Apr 08 2021 at 12:24):

Is leanproject import-graph working for others? When I run, e.g. leanproject import-graph i.pdf, I just get a giant row of nodes, with no edges.

view this post on Zulip Eric Wieser (Apr 08 2021 at 12:48):

Do you have a fresh cache?

view this post on Zulip Bhavik Mehta (Apr 08 2021 at 14:16):

I had the same issue, but cd into src seemed to fix it

view this post on Zulip Scott Morrison (May 03 2021 at 02:10):

When I run leanproject import-graph i.pdf in mathlib, I get a PDF containing nodes but no edges. Can anyone else confirm?

view this post on Zulip Bhavik Mehta (May 03 2021 at 03:59):

Can confirm, I get the exact same thing

view this post on Zulip Gabriel Ebner (May 03 2021 at 08:24):

I get the usual hairy mess. I'm running leanproject import-graph i.pdf directly from the mathlib directory, on linux.

view this post on Zulip Eric Wieser (May 03 2021 at 08:30):

Does Bhavik's previous remark help?

view this post on Zulip Scott Morrison (May 03 2021 at 08:31):

(Oops, forgot I'd asked about this earlier!!)


Last updated: May 15 2021 at 22:14 UTC