Unused definitions

Stream: lean4

[Sky Wilshaw]

Is there a way to determine which definitions/theorems a given theorem depends on (for the purpose of deleting unused ones)?

[Bhavik Mehta]

I don't have an answer but I would also find this useful - especially if it's restricted to a particular folder / set of files rather than all of mathlib

[Patrick Massot]

There was a tool in mathlib3 but I don't think it got ported. It was https://leanprover-community.github.io/mathlib_docs/tactic/find_unused.html

[Sky Wilshaw]

This looks really useful!

[Scott Morrison]

This is should be easy to implement on top of src#Expr.getUsedConstants or src#ConstantInfo.getUsedConstants.

A nicer implementation than the mathlib3 approach would just be a command #find_unused in ..., that prints a list of the constants declared in the current file (up to this point) not used in the declarations constructed in the ....

I'd hope that this would actually be a relatively easy learning project for someone wanting to start metaprogramming.

[Sky Wilshaw]

Learning metaprogramming has been on my to-do list for a while - if I get time I might try to implement it, but don't let that stop anyone with more knowledge/experience than me.

[Kyle Miller]

I got sniped by this because of the breadcrumbs Scott laid out. It seemed like it would be straightforward to do this by starting with the whatsnew code, but there was a gotcha: certain declarations can be artificially used by additional internal declarations that Lean generates when processing.

This reports both unused declarations and declarations that have finally become used by the new declarations.

import Mathlib.Lean.Expr.Basic

open Lean Elab Command Meta

-- Generalized monad for `Lean.Name.isBlackListed`
def Lean.Name.isBlackListed' {m : Type → Type} [Monad m] [MonadEnv m]
    (declName : Name) : m Bool := do
  if declName == ``sorryAx then return true
  if declName matches .str _ "inj" then return true
  if declName matches .str _ "noConfusionType" then return true
  let env ← getEnv
  pure $ declName.isInternal'
   || isAuxRecursor env declName
   || isNoConfusion env declName
  <||> isRec declName <||> isMatcher declName

namespace Mathlib.FindUnused

/-- Remove all blacklisted names from the given environment.
This might not be accurate since the blacklist function is a heuristic. -/
def filterNames {m : Type → Type} [Monad m] [MonadEnv m] {α : Type _}
    (env : PHashMap Name α) : m (PHashMap Name α) := do
  let mut env' := env
  for (n, _) in env do
    if ← n.isBlackListed' then
      env' := env'.erase n
  return env'

/-- `#find_unused in $command` executes the command and then prints the
pre-existing unused declarations in this module that remain unused. -/
elab "#find_unused " "in" ppLine cmd:command : command => do
  let oldEnv ← filterNames (← getEnv).constants.map₂
  try
    elabCommand cmd
  finally
    let newEnv ← filterNames (← getEnv).constants.map₂
    let mut usedNames : NameSet := {}
    let mut uniquelyUsedNames : NameSet := {}
    let mut unusedNames : NameSet := {}
    for (_, c) in oldEnv do
      usedNames := usedNames.union c.getUsedConstants
    for (n, c) in newEnv do
      unless oldEnv.contains n do
        for n' in c.getUsedConstants do
          unless usedNames.contains n' do
            uniquelyUsedNames := uniquelyUsedNames.insert n'
          usedNames := usedNames.insert n'
    for (n, _) in oldEnv do
      unless usedNames.contains n do
        unusedNames := unusedNames.insert n
    let pp (names : NameSet) : CommandElabM (List MessageData) := do
      let consts := names.toArray
      let consts ← consts.mapM fun n =>
        return (← findDeclarationRanges? n, n, newEnv.find! n)
      let consts := consts.insertionSort fun (d?, _) (d'?, _) =>
        if let (some d, some d') := (d?, d'?) then
          Position.lt d.range.pos d'.range.pos
        else
          false
      let consts ← consts.mapM fun (_, n, c) =>
        return m!"{mkConst n (c.levelParams.map .param)}"
      return consts.toList
    let unusedNames' ← pp unusedNames
    let uniquelyUsedNames' ← pp uniquelyUsedNames
    unless unusedNames'.isEmpty do
      logInfo m!"Declarations that are still unused:{
        indentD <| .joinSep unusedNames' ", "}"
    unless uniquelyUsedNames'.isEmpty do
      logInfo m!"Declarations are only used by this command:{
        indentD <| .joinSep uniquelyUsedNames' ", "}"

[Kyle Miller]

def fAux (x : Nat) := x
def f (x : Nat) := fAux x
def g (x : Nat) := x

#find_unused in
def h (x : Nat) := f x

/-
Declarations that are still unused:
  g

Declarations are only used by this command:
  f
-/