dependency graphs

Stream: general

[Samiha Sharlin ⚛️]

Hi,

I am trying to generate a dependency graph for a lean file inside mathlib. However, I think it generates the output file for the whole project instead of that proof ( analysis.special_functions.stirling.pdf ). Is there documentation for the options we can use?

I saw " --exclude-tactics" and some other commands in mathlib port discussions, but I couldn't run "--exlcude-tactics" either. There's no error message, but I am getting these kind of outputs: Screenshot-2023-01-09-at-1.14.59-PM.png

[Moritz Firsching]

stirling.pdf

firsching@euler ~/mathlib (master)> leanproject import-graph --to analysis.special_functions.stirling --exclude-tactics stirling.pdf --port-status

seems to work for me. From the screenshot it looks like you are inside the src, but I guess that shouldn't make a difference...

[Yakov Pechersky]

@Samiha Sharlin ⚛️ , you need to upgrade your leanproject. Right now, you're hitting an error where you're using a flag that your older version doesn't have, and it's exiting early without printing the error.

To upgrade, one possible command is to run "pip install -U mathlibtools"

[Samiha Sharlin ⚛️]

Moritz Firsching said:

stirling.pdf

firsching@euler ~/mathlib (master)> leanproject import-graph --to analysis.special_functions.stirling --exclude-tactics stirling.pdf --port-status

seems to work for me. From the screenshot it looks like you are inside the src, but I guess that shouldn't make a difference...

Thank you for sharing the PDF! I just tried the command outside src directory, and yet having the same issue.

[Samiha Sharlin ⚛️]

Yakov Pechersky said:

Samiha Sharlin ⚛️ , you need to upgrade your leanproject. Right now, you're hitting an error where you're using a flag that your older version doesn't have, and it's exiting early without printing the error.

To upgrade, one possible command is to run "pip install -U mathlibtools"

Thanks! Do you know which version works? Currently, I am running in 1.3.2 Screenshot-2023-01-09-at-6.35.14-PM.png

[Yakov Pechersky]

Can you try the same command as before (leanproject import-graph ... ), only with the debug flag? leanproject --debug import-graph ...

[Samiha Sharlin ⚛️]

Screenshot-2023-01-09-at-6.53.02-PM.png