Tracking axioms

Stream: general

[Yaël Dillies]

I am close to completing the proof of a big theorem. However my project is still full of tiny sorries which are mathematically insignificant but might still be time-taking to eliminate. I would like to know which of those sorries are actually used in the final theorem so that I eliminate those first.

[Yaël Dillies]

Do we have the infrastructure needed to track down uses of sorryAx, or any other axiom?

[Kevin Buzzard]

I guess you could make a new axiom and then change a sorry to the new axiom and see if the proof uses it before filling it. But then you'd have to constantly recompile

[Yaël Dillies]

Yes, I am aware of this solution, but would like a more mature, industrial one

[Henrik Böving]

Yaël Dillies said:

Do we have the infrastructure needed to track down uses of sorryAx, or any other axiom?

I'm not aware of any but it should be rather easy to write a DFS through the transitive dependency closure of a particular theorem that marks a dependency whenever it uses sorry directly

[Henrik Böving]

import Lean

open Lean
structure State where
  sorryUsers : Array Name
  seen : Std.HashSet Name

abbrev M := StateT State CoreM

def seen (n : Name) : M Bool := do
  return (← get).seen.contains n

def notSeen (n : Name) : M Bool := do
  return !(← seen n)

def addSeen (n : Name) : M Unit := do
  modify fun s => {s with seen := s.seen.insert n}

def addSorryUser (n : Name) : M Unit := do
  modify fun s => {s with sorryUsers := s.sorryUsers.push n}

def isSorry (n : Name) : M Bool := do
  let env ← getEnv
  let some info := env.find? n | unreachable!
  match info with
  | .axiomInfo info => return info.name == ``sorryAx
  | _ => return false

partial def find (start : Name) : CoreM (Array Name) := do
  let (_, state) ← go [start] |>.run { sorryUsers := #[], seen := {} }
  IO.println s!"seen size: {state.seen.size}"
  return state.sorryUsers
where
  go (worklist : List Name) : M Unit := do
    match worklist with
    | [] => return ()
    | n :: worklist =>
      if ← seen n then
        go worklist
      else
        let env ← getEnv
        let some info := env.find? n | unreachable!
        match info with
        | .defnInfo .. | .thmInfo .. | .opaqueInfo .. | .ctorInfo .. | .recInfo .. | .inductInfo ..  =>
          addSeen n
          let consts ← info.getUsedConstantsAsSet |>.toList |>.filterM notSeen
          if ← consts.anyM isSorry then
            addSorryUser n
          go (consts ++ worklist)
        | .quotInfo ..   => addSeen n; go worklist
        | .axiomInfo .. => go worklist


#eval find ``Nat.add

@Yaël Dillies, note that if you run this on a declaration e.g. deep within mathlib this becomes a very expensive computation which you probably want to compile with a precompileModules setup.

[Henrik Böving]

So my own setup to run this on something deep inside of mathlib was a new lake math project with

@[default_target]
lean_lib «FindConsts» where
  precompileModules := true

and then the above code in FindConsts.Basic and finally

import FindConsts.Basic
import Mathlib

#time #eval find ``CondensedSet.ofSheafCompHaus

in FindConsts so that it uses the compiled version of FindConsts.Basic

[Daniel Weber]

There's https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.E2.9C.94.20Finding.20usages.20of.20.60sorry.60.20in.20external.20code/near/430509619

[Yaël Dillies]

Ha! I knew this had already been discussed somewhere :grinning:

[Yaël Dillies]

What do people think of including some version of this code in mathlib(/the mathlib repo but in a separate library)? I see this as a general-purpose util that people should have access to, just like lake exe mk_all

[Ruben Van de Velde]

Yes, that sounds like a good idea. Maybe even with import graph?

[Yaël Dillies]

Sounds sensible, but maybe Kim or Stuart have opinions here?

[Kim Morrison]

Yes, happy to have such functionality in import-graph.