Zulip Chat Archive

You can do this more efficiently, but in terms of where you get the stuff. The project level one I think you would just filter based on whether a declaration is from a module that's not from your project (or is in the current file).

Chris Bailey (Oct 12 2025 at 01:47):

The painful part is going to be going through the values if that's the degree of search you're talking about.

Asei Inoue (Oct 12 2025 at 07:18):

@Chris Bailey Thank you

Jon Eugster (Oct 12 2025 at 07:24):

I think something similar is done in import-graph although I don't know the details. I think Kim implemented that.

A PR adding such a tool to that package for others to use would be very welcome and desirable :)

Alastair Irving (Oct 12 2025 at 09:53):

I did something like this recently. I wanted to know how many of the results in the Math-inc proof of PNT were not actually being used. I used https://github.com/patrik-cihal/lean-graph which can graph the dependencies of a result or everything in a namespace. It was a bit hacky because I had to put everything in the project in a namespace but then I was able to use a simple Python script to analyze the dependency graph for unused parts. This motivated my issue https://github.com/patrik-cihal/lean-graph/issues/4 because that would make it easier to see what's in the current project and avoid putting everything into a namespace.

Ruben Van de Velde (Oct 12 2025 at 12:35):

There's code to do similar things in import graph as I recall

Kim Morrison (Oct 14 2025 at 10:56):

e.g. docs#Lean.Name.transitivelyUsedConstants.

Damiano Testa (Oct 20 2025 at 13:34):

Mathlib also has a #show_unused command:

import Mathlib

theorem X : True := trivial
theorem Y : True := trivial
theorem Z : True := X

#show_unused Z

Riccardo Brasca (Oct 20 2025 at 13:43):

I don't remember who wrote this script, but in practice it works (it's not super fast).

Last updated: Dec 20 2025 at 21:32 UTC