Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Theorem-level dependency graph

Yury G. Kudryashov (Dec 16 2025 at 15:15):

I've just completed the proof of the main theorem in https://github.com/urkud/SardMoreira/. The repository has a bunch of theorems that I added because they seemed useful, then never used for the final proof. Is there something like lake exe graph for theorems? E.g., I would love to move those unused theorems to a new file Unused.lean, then go through the dependency graph of the rest and PR stuff to Mathlib.

Damiano Testa (Dec 16 2025 at 15:20):

I do not know of any automation, but I found #show_unused very helpful for this kind of process.

Yury G. Kudryashov (Dec 16 2025 at 15:29):

Thanks!

Johan Commelin (Dec 16 2025 at 16:13):

cc @Adam Topaz

Damiano Testa (Dec 16 2025 at 16:19):

Btw, there are rumours of a #mwe producer, which could likely be repurposed into this kind of behaviour.

Adam Topaz (Dec 16 2025 at 16:50):

@Yury G. Kudryashov I'm working on such things now, but nothing is ready yet. In the meantime, you can use Lean.Name.transitivelyUsedConstants to get the transitive dependencies of some constant in the environment.

Adam Topaz (Dec 16 2025 at 16:51):

Give me about 5 mins and I'll tell you what your theorems in MainTheorem.lean depend on.

Adam Topaz (Dec 16 2025 at 16:59):

Here's the list of constants defined in your project which your main theorems depend on:
data

Adam Topaz (Dec 16 2025 at 16:59):

I got this by running the following script at the bottom of your MainTheorem.lean file:

open Lean in
#eval show CoreM Unit from do
  let env ← getEnv
  let consts : NameSet :=
    env.constants.map₂.foldl (init := {}) fun n a _ => n.insert a
  let deps ← consts.transitivelyUsedConstants
  let mut filteredDeps : NameSet := {}
  for dep in deps do
    if (← dep.isBlackListed) then continue
    let some mod := env.getModuleFor? dep | continue
    unless mod.getRoot == `SardMoreira do continue
    filteredDeps := filteredDeps.insert dep
  IO.FS.withFile "data" .write fun handle => do
    for dep in filteredDeps do
      handle.putStrLn dep.toString