find unused imports

Stream: general

[Floris van Doorn]

@Scott Morrison and @Alex J. Best recently talked about fixing https://github.com/alexjbest/dag-tools in the #rss steam. Did either of you get a working version eventually?

[Alex J. Best]

I think Scott and Mario wrote their own version in the end? In one of the #mathlib4 threads

[Mario Carneiro]

Oh, did we reinvent something? What's dag-tools?

[Andrew Yang]

discussion on Zulip about dag-tools

[Mario Carneiro]

discussion on #mathlib4 where Scott and I reinvent Alex's tool

[Alex J. Best]

Yeah I was a bit busy last week so couldn't follow too closely, but my impression is that compared to what me and Johan did the new code is likely faster and less complicated, perhaps at the expense of missing some less obvious ways files can depend on each other. I guess it is not 100% lean but thats also fine for this purpose. It also has the advantage that it works today, or at least that Scott knows how it works :smile:!

[Floris van Doorn]

Thanks for the pointers!

[Scott Morrison]

No.