counting classes and instances

Stream: general

[Jeremy Avigad]

Is there an easy way to get a rough (or exact) estimate of the number of classes and instances in Mathlib? grep and wc overcount the occurrences of the word "class" or "instance" in comments. I can try my hand at metaprogramming, but any pointers or hints will be appreciated.

[Mac Malone]

A quick-and-dirty approximation for a given namespace:

import Lean.Meta.Instances

open Lean Meta

def countClassesAndInstances [Monad m] [MonadEnv m] (ns := Name.anonymous) : m (Nat × Nat) := do
  let s := classExtension.getState (← getEnv)
  let classes := s.outParamMap.fold (init := #[]) fun a k _ => a.push k
  let classes := classes.filter ns.isPrefixOf
  let s := instanceExtension.getState (← getEnv)
  let instances := s.instanceNames.foldl (init := #[]) fun a k _ => a.push k
  let instances := s.erased.fold (init := instances) fun a k => a.erase k
  let instances := instances.filter ns.isPrefixOf
  return (classes.size, instances.size)

/-
classes: 144
instances: 1526
-/
#eval show CoreM _ from do
  let (numClasses, numInstances) ← countClassesAndInstances
  IO.println s!"classes: {numClasses}"
  IO.println s!"instances: {numInstances}"

/-
classes: 35
instances: 772
-/
#eval show CoreM _ from do
  let (numClasses, numInstances) ← countClassesAndInstances `Lean
  IO.println s!"classes: {numClasses}"
  IO.println s!"instances: {numInstances}"

[Eric Wieser]

With import Mathlib, that's

classes: 22071
instances: 1296

[Eric Wieser]

I assume those are backwards and I copied your code just before the edit!

[Jeremy Avigad]

Thanks! While waiting, I decided not to be so lazy, so I tried adapting some code that Floris once wrote. I came up with this, which reports almost the same results on an older version of Mathlib, i.e. 1293 classes and 22110 instances:

import Mathlib

open Lean Meta Elab Command

def getClassAndInstanceCounts : MetaM Unit := do
  let classes := classExtension.getState (← getEnv) |>.outParamMap
  let instances := instanceExtension.getState (← getEnv) |>.instanceNames
  logInfo m!"classes: {classes.size}"
  logInfo m!"instances: {instances.size}"

run_cmd liftCoreM <| MetaM.run' <| do
  getClassAndInstanceCounts

I guess Mac is filtering out anonymous classes and instances. I'll check to see how much of a difference that makes..

[Jeremy Avigad]

Oh, I see, Mac's code lets us filter for any prefix. Thanks!

[Mac Malone]

@Jeremy Avigad It also filters out instances which have been erased, which may or may not be desirable in your use case.

[Eric Wieser]

What does it mean for an instance to have been erased?

[Floris van Doorn]

I think it means you've written attribute [-instance] Foo. I believe those erasures a local, so it shouldn't matter.

[Eric Wieser]

I think attribute [local instance] Foo counts as an erased instance too? My understanding was that local instances were globally registered then globally erased, but that was a guess after a cursory read of the source.