Get all theorems from Mathlib

Stream: lean4

[Max Nowak 🐉]

Is there a way that I can obtain ≈1000 (or all :smiling_devil: ) theorems from Mathlib in a metaprogram? I have the following code, but has extreme performance problems.

import Lean
import Mathlib

open Lean

def hasPrefix (pre : Name) (name : Name) : Bool :=
  let comps := name.components.toArray
  let preComps := pre.components.toArray
  comps[:preComps.size] == preComps

elab "#bench" : command => do
  let env <- getEnv
  let mut mathlibModules := env.allImportedModuleNames |>.filter (hasPrefix `Mathlib.Data.Int .)
  if mathlibModules.size > 3 then
    mathlibModules := mathlibModules[:3]
    dbg_trace "Too many modules, truncating to just {mathlibModules}"
  let mathlibModuleIdxs := mathlibModules.map (env.moduleIdxForModule? . |>.get!)

  -- The following is the slow part:
  let tmp := mathlibModuleIdxs.map (fun x => env.declsInModuleIdx x |>.toArray)
  let tmp2 := tmp.flatten
  logInfo m!"Have {tmp2.size} declarations from {mathlibModules}"

#bench

[Alex J. Best]

If env is your current environment (which should be everything if you already have import Mathlib) then env.constants (docs4#Lean.Environment) should be all theorems.
Of course there are lots so things might eventually be slow but this works

import Mathlib.Data.Nat.Basic

import Lean
import Mathlib

open Lean

def hasPrefix (pre : Name) (name : Name) : Bool :=
  let comps := name.components.toArray
  let preComps := pre.components.toArray
  comps[:preComps.size] == preComps

elab "#bench" : command => do
  let env <- getEnv
  logInfo m!"Have {env.constants.size} declarations"
  logInfo <| toString <| (env.constants.toList.take 1000).map Prod.fst

#bench

[Alex J. Best]

You might also want to look at how the mathlib linters function https://github.com/leanprover-community/mathlib4/blob/e54ba2250be1bd7bbb68497a3781dc62ca072d79/scripts/runLinter.lean#L32, these run over all declarations and are pretty efficient

[Alex J. Best]

I see you only want mathlib theorems, maybe docs4#Std.Tactic.Lint.getDeclsInPackage is the right answer in that case

[Max Nowak 🐉]

getDeclsInPackage looks very promising! Thanks a lot