Remove unnecessary codes

Stream: Is there code for X?

[Palalansoukî]

In running a large project, there are many definitions and theorems that were once needed but are no longer necessary. Is there any way to find out if such code can be safely removed? For instance, is it possible to list all definitions/theorems that could be affected by the removal of a particular definition/theorem (and vice versa)?

[Kyle Miller]

These are possible to compute, but I'm not sure if there's anything pre-made.

Not completely unrelated (it's at the level of modules instead of declarations) is Shake in mathlib, which is for computing more efficient imports: https://github.com/leanprover-community/mathlib4/blob/master/Shake/Main.lean

[Junyan Xu]

See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/jixia/near/450349637