lake exe graph --exclude-meta

Stream: general

[Yury G. Kudryashov]

The graph generated by lake exe graph --exclude-meta --to Mathlib.Logic.Equiv.Fin fin.pdf includes a lot of Mathlib.Tactic.* files. @Scott Morrison

[Kim Morrison]

Sorry, don't have time to look now. The code is pretty simple if you want to take a look. Perhaps @Jon Eugster can help?

[Eric Rodriguez]

image.png

It seems it just filters by name as opposed to anything else; I don't see an easy way to make it ignore files

[Kim Morrison]

I think when upstreaming it there was a search replace error. Most of the "Graph" in the screenshot should clearly be "Mathlib".

[Kim Morrison]

@Eric Rodriguez, there's no distinction between files and names here, no?

[Eric Rodriguez]

Oh, I see, I thought Names could only be for stuff in the environment, not file names too

[Jon Eugster]

Oh yes, my bad! I'll push a fix PR later today

(here it is: #10490)