Topic: leanproject import-graph
Scott Morrison (Apr 08 2021 at 12:24):
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.
Eric Wieser (Apr 08 2021 at 12:48):
Do you have a fresh cache?
Bhavik Mehta (Apr 08 2021 at 14:16):
I had the same issue, but cd into src seemed to fix it
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?
Bhavik Mehta (May 03 2021 at 03:59):
Can confirm, I get the exact same thing
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.
Eric Wieser (May 03 2021 at 08:30):
Does Bhavik's previous remark help?
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