Zulip Chat Archive

Stream: new members

Topic: leanproject: "dot" not found in path

Antoine Chambert-Loir (Dec 19 2022 at 13:37):

Trying to learn how to port sth to mathlib4, I follow Scott's video scrupulously, and I get this error message, regarding import-graph:

8:34) pro-acl > leanproject import-graph --to data.rat.order --exclude-tactics  data.rat.order.pdf
[Errno 2] "dot" not found in path.

Any help?

Eric Wieser (Dec 19 2022 at 13:37):

You likely need to install dot / graphviz

Patrick Massot (Dec 19 2022 at 13:58):


Kevin Buzzard (Dec 19 2022 at 14:17):

But if you just want to know the state of data.rat.order, you can look here.

Last updated: Dec 20 2023 at 11:08 UTC