Zulip Chat Archive

Stream: general

Topic: leanproject import-graph

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.

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: Dec 20 2023 at 11:08 UTC