Correct declaration, proof, recursion, and dependency metrics

LeanMetrics/Authored.lean

@@ -7,7 +7,6 @@ module
 
 public import Lean.Environment
 import Lean.AuxRecursor
-import Lean.Class
 import Lean.DeclarationRange
 import Lean.Meta.Match.MatcherInfo
 import Lean.ProjFns
@@ -38,26 +37,10 @@ For example a constructor, a `where` helper, a `deriving` instance, or a parser
 def hasOwnDeclaration (env : Environment) (n : Name) : Bool :=
   (declRangeExt.find? env n).isSome && !sameOrigin env n n.getPrefix
 
-/-- Whether structure `s` has `target` among its ancestors. -/
-partial def hasAncestor (env : Environment) (s target : Name) (visited : NameSet := {}) : Bool :=
-  if visited.contains s then false
-  else (getStructureInfo? env s).any fun info =>
-    info.parentInfo.any fun p =>
-      p.structName == target || hasAncestor env p.structName target (visited.insert s)
-
-/-- Whether `n` converts a structure to one it builds on: the coercion `extends` generates, or a
-`toX` in the structure's namespace when the structure is a class or `X` is an ancestor
-(`Field.toSemifield`). -/
+/-- Whether `n` is a parent projection registered by `extends`. Names alone are not evidence:
+an author can write an ordinary function such as `Box.toNat` in a class namespace. -/
 def isParentProjection (env : Environment) (n : Name) : Bool :=
-  match getStructureInfo? env n.getPrefix, n with
-  | none, _ => false
-  | some info, .str p s =>
-    info.parentInfo.any (·.projFn == n) ||
-      (s.startsWith "to" && s.length > 2 &&
-        let target := (s.drop 2).toString
-        (target.startsWith "OfNat" && target.any Char.isDigit) || isClass env p ||
-          (getStructureInfo? env (.mkSimple target)).isSome && hasAncestor env p (.mkSimple target))
-  | some info, _ => info.parentInfo.any (·.projFn == n)
+  (getStructureInfo? env n.getPrefix).any fun info => info.parentInfo.any (·.projFn == n)
 
 /-- Namespaces of tactic implementations. -/
 def tacticNamespaces : List Name :=

LeanMetrics/Driver.lean

@@ -42,10 +42,10 @@ partial def Output.render (o : Output) (indent : String := "") : String :=
 
 /-- Version of the output format, raised whenever a column is renamed, removed or changes
 meaning. -/
-def schemaVersion : Nat := 1
+def schemaVersion : Nat := 2
 
 /-- The version of `lean-metrics`, reported in its output. -/
-def toolVersion : String := "0.1.0"
+def toolVersion : String := "0.2.0"
 
 /-- What to measure and how to report it. -/
 structure Options where

LeanMetrics/Metrics/Declarations.lean

@@ -8,6 +8,7 @@ module
 public import LeanMetrics.Basic
 import LeanMetrics.Stats
 import LeanMetrics.Syntax
+import Lean.Elab.PreDefinition.WF.Eqns
 
 /-! # Declarations
 
@@ -75,7 +76,7 @@ def declarations : Metric where
         counts := counts.insert k (counts.getD k 0 + 1)
         if k != "example" && (signatureBinders d).any isImplicitBinder then
           nImplicit := nImplicit + 1
-    -- `deriving` clauses and `attribute [instance]` commands also declare instances
+    -- `deriving` creates instances; `attribute [instance]` only registers existing constants.
     let mut nDerived := 0
     let mut nAttrInstance := 0
     for f in ctx.files do
@@ -90,7 +91,7 @@ def declarations : Metric where
         for a in nodesOfKind ``Command.attribute c do
           if (attributesUnder a).contains `instance then
             nAttrInstance := nAttrInstance + 1
-    counts := counts.insert "instance" (counts.getD "instance" 0 + nDerived + nAttrInstance)
+    counts := counts.insert "instance" (counts.getD "instance" 0 + nDerived)
     let n (k : String) := counts.getD k 0
     let nDefLike := defLike.foldl (· + n ·) 0
     return { columns :=
@@ -99,7 +100,8 @@ def declarations : Metric where
       #[("n_def_like", toJson nDefLike),
         ("def_like_to_theorem_ratio", ratio nDefLike (n "theorem")),
         ("n_decls_implicit_args", toJson nImplicit), ("n_new_classes", toJson (n "class")),
-        ("n_new_instances", toJson (n "instance"))] }
+        ("n_new_instances", toJson (n "instance")),
+        ("n_instance_attribute_commands", toJson nAttrInstance)] }
 
 /-- Metric `implicit_args`: Binder groups in declaration signatures, by kind. -/
 def implicitArgs : Metric where
@@ -125,7 +127,7 @@ def proofMode : Metric where
   needsSource := true
   run ctx := do
     let bodies := ctx.declarations.filter isTheorem |>.filterMap bodyOf?
-    let nTactic := (bodies.filter isTacticBody).size
+    let nTactic := (bodies.filter (isTacticBody ∘ unwrapProof)).size
     let nTerm := bodies.size - nTactic
     return { columns := #[("n_pm_term", toJson nTerm), ("n_pm_tactic", toJson nTactic),
       ("pm_term_ratio", ratio nTerm bodies.size)] }
@@ -153,18 +155,20 @@ def reducibility : Metric where
       ("red_irreducible_per_def", ratio nIrreducible nDef 4),
       ("red_abbrev_per_def", ratio nAbbrev nDef 4)] }
 
-/-- Metric `recursion_style`: `termination_by` and `decreasing_by` clauses. -/
+/-- Metric `recursion_style`: Source termination annotations and authored definitions Lean
+compiled with well-founded recursion, including inferred measures and counting each once. -/
 def recursionStyle : Metric where
   name := "recursion_style"
-  description := "`termination_by` and `decreasing_by` clauses"
+  description := "termination annotations and definitions compiled with well-founded recursion"
   needsSource := true
   run ctx := do
     let cmds := ctx.files.foldl (· ++ ·.commands) #[]
     let sum (k : SyntaxNodeKind) := cmds.foldl (· + countKind k ·) 0
     let t := sum ``Termination.terminationBy
     let d := sum ``Termination.decreasingBy
+    let wf := (ctx.authored.filter fun n => (Elab.WF.eqnInfoExt.find? ctx.env n).isSome).size
     return { columns := #[("n_rec_termination_by", toJson t), ("n_rec_decreasing_by", toJson d),
-      ("n_rec_well_founded", toJson (t + d)),
-      ("rec_uses_well_founded", toJson (decide (t + d > 0)))] }
+      ("n_rec_well_founded", toJson wf),
+      ("rec_uses_well_founded", toJson (decide (wf > 0)))] }
 
 end LeanMetrics

LeanMetrics/Metrics/Graph.lean

@@ -8,6 +8,8 @@ module
 public import LeanMetrics.Basic
 public import LeanMetrics.Authored
 import LeanMetrics.Stats
+import LeanMetrics.Syntax
+import Lean.Elab.DeclarationRange
 import Lean.Meta.Instances
 import Lean.ProjFns
 import Lean.Util.Recognizers
@@ -185,13 +187,32 @@ private def log10Nat (x : Nat) : Float :=
   let shift := x.log2 - min x.log2 52
   (x >>> shift).toFloat.log10 + shift.toFloat * Float.log10 2
 
+/-- Local instance registrations disappear on import. Recover their declaration identities
+from source selection ranges, including anonymous and private instances. -/
+private def sourceInstances (ctx : Context) : NameSet := Id.run do
+  let mut positions : Std.HashSet (Name × Nat × Nat) := {}
+  for file in ctx.files do
+    for cmd in file.commands do
+      for decl in declarationsOf cmd do
+        if decl.isOfKind ``Parser.Command.instance then
+          if let some pos := (Elab.getDeclarationSelectionRef decl).getPos? then
+            let p := file.fileMap.toPosition pos
+            positions := positions.insert (file.module, p.line, p.column)
+  let mut names : NameSet := {}
+  for n in ctx.authored do
+    if let some mod := ctx.moduleOf? n then
+      if let some ranges := declRangeExt.find? ctx.env n then
+        let p := ranges.selectionRange.pos
+        if positions.contains (mod, p.line, p.column) then names := names.insert n
+  return names
+
 /-- Metric `dep_graph`: Shape of the declaration dependency graph: degrees, roots and leaves,
 longest chain, and sharing of sub-results. -/
 def depGraph : Metric where
   name := "dep_graph"
   description := "shape of the declaration dependency graph: degrees, roots and leaves, longest \
     chain, and sharing of sub-results"
-  needsSource := false
+  needsSource := true
   run ctx := do
     let g := depGraphOf ctx
     let idx : Std.HashMap Name Nat := g.internal.foldl (fun m n => m.insert n m.size) {}
@@ -246,8 +267,9 @@ def depGraph : Metric where
     let extAll : NameSet := ext.foldl (fun s e => e.foldl (·.insert ·) s) {}
     let rootCost := root?.map (cost[·]!) |>.getD 0
     -- instances first: Prop-valued ones are theorems, and every instance is also a definition
+    let declaredInstances := sourceInstances ctx
     let kinds := g.internal.map fun c =>
-      if isInstanceCore ctx.env c then "instance"
+      if declaredInstances.contains c || isInstanceCore ctx.env c then "instance"
       else match ctx.env.find? c with
         | some (.thmInfo _) => "theorem"
         | some (.defnInfo _) | some (.opaqueInfo _) | some (.inductInfo _) => "def"
@@ -266,6 +288,7 @@ def depGraph : Metric where
       ("ext_deps_per_decl_mean", mean (ext.map (·.size)) 2), ("n_ext_consts", toJson extAll.size),
       ("longest_pole", toJson (maximum depth)),
       ("root", toJson ((root?.map (displayName g.internal[·]!)).getD "")),
+      ("root_id", toJson ((root?.map (toString g.internal[·]!)).getD "")),
       ("cost_root_log10", if rootCost == 0 then .null else decimal (log10Nat rootCost)),
       ("reachable_from_root", toJson reachable),
       ("compression_log10", if rootCost == 0 || reachable == 0 then .null
@@ -280,7 +303,14 @@ def depGraph : Metric where
       ("n_theorems_single_use", count fun i => kind i == "theorem" && inDeg[i]! == 1),
       ("n_defs_unused", count fun i => kind i == "def" && inDeg[i]! == 0),
       ("n_defs_no_theorem_user", count fun i => kind i == "def" && !usedByTheorem.contains i)]
-    let edges := g.edges.map fun (d, u) => Json.arr #[displayName d, displayName u]
-    return { columns, details := Json.mkObj [("edges", Json.arr edges)] }
+    -- Private declarations can have the same user name in different modules. Preserve Lean's
+    -- unique names as IDs and keep their readable names separately, including isolated nodes.
+    let nodeNames := g.internal.foldl (·.insert ·) extAll
+    let nodes := nodeNames.foldl (init := #[]) fun acc name => acc.push <| Json.mkObj [
+      ("id", toJson name.toString), ("name", toJson (displayName name)),
+      ("module", toJson ((ctx.moduleOf? name).map toString |>.getD "")),
+      ("internal", toJson (idx.contains name))]
+    let edges := g.edges.map fun (d, u) => Json.arr #[toJson d.toString, toJson u.toString]
+    return { columns, details := Json.mkObj [("nodes", Json.arr nodes), ("edges", Json.arr edges)] }
 
 end LeanMetrics

LeanMetrics/Metrics/Imports.lean

@@ -188,7 +188,9 @@ def importMinimizability : Metric where
     let nAdd := total (·.add)
     let byModule (f : Shake.Verdict → Array Import) := Json.mkObj <| verdicts.toList.filterMap
       fun (i, v) => let is := authored f i v
-        if is.isEmpty then none else some (vnames[i]!.toString, toJson (is.map toString))
+        let render (imp : Import) := if view.header.moduleData[i]!.isModule then toString imp
+          else s!"import {imp.module}"
+        if is.isEmpty then none else some (vnames[i]!.toString, toJson (is.map render))
     -- the same count, from constants alone
     let closure := transitiveImports env
     let required := requiredModules env own

LeanMetrics/Metrics/Tactics.lean

@@ -123,7 +123,7 @@ def decideUsage : Metric where
       nodesOfKind ``Tactic.simpAll c ++ nodesOfKind ``Tactic.simpa c ++
       nodesOfKind ``Tactic.dsimp c) #[]
     let termRfl := ctx.declarations.filter fun d =>
-      (bodyOf? d).any fun b => b.isIdent && b.getId == `rfl
+      (bodyOf? d).any fun b => let b := unwrapProof b; b.isIdent && b.getId == `rfl
     let nNativeDecide := cmds.foldl (· + countKind ``Tactic.nativeDecide ·) 0
     return { columns := #[
       ("n_dec_decide", toJson (decides.size - nKernel - nNative)), ("n_dec_kernel", toJson nKernel),

LeanMetrics/Syntax.lean

@@ -120,7 +120,15 @@ def bodyOf? (decl : Syntax) : Option Syntax :=
     | some e => some e[0][0]
     | none => none
 
-/-- Whether a body is a tactic block (`:= by …`). -/
+/-- Remove wrappers that do not change a proof's tactic/term mode. Keep the original syntax
+for source size and `by` depth: treating a wrapper as a `by` node would count it twice. -/
+partial def unwrapProof (body : Syntax) : Syntax :=
+  if body.isOfKind ``Term.paren || body.isOfKind ``Term.typeAscription then unwrapProof body[1]
+  else if body.isOfKind ``Term.set_option then unwrapProof body[5]
+  else if body.isOfKind ``Term.open then unwrapProof body[3]
+  else body
+
+/-- Whether this syntax node itself is a tactic block. -/
 def isTacticBody (body : Syntax) : Bool :=
   body.isOfKind ``Term.byTactic || body.isOfKind ``Term.byTactic'
 

Main.lean

@@ -45,7 +45,7 @@ def runCmd (p : Parsed) : IO UInt32 := do
 
 /-- The command line of `lean-metrics`. -/
 def cmd : Cmd := `[Cli|
-  "lean-metrics" VIA runCmd; ["0.1.0"]
+  "lean-metrics" VIA runCmd; ["0.2.0"]
   "Measure a built Lake project: size, declarations, proofs, tactics, imports, dependency \
   structure, documentation and build warnings. Run `lake build` in the project first."
 

README.md

@@ -36,7 +36,9 @@ every module they import from the project itself. Dependencies such as Mathlib a
 measured.
 
 Alternatively, `lean-metrics.sh` does both steps: run from the root of a project, it builds the
-project, builds `lean-metrics` with the same toolchain, and runs it.
+project, builds `lean-metrics` with the same toolchain, and runs it. This checkout supports Lean
+`v4.34.0`; the wrapper changes the selected toolchain but does not port Lean API usage or dependency
+versions to other releases.
 ```sh
 ../lean-metrics/lean-metrics.sh > metrics.json
 ```
@@ -55,7 +57,7 @@ monorepo, for example `--module MyMonorepo.ProjectA`, and loads only what those
 `--metric M,N` runs only these metrics; `--list` lists all of them with a one-line description.
 
 `--details` adds structured detail to the document, such as the tactic histogram, the dependency
-graph's edges, and the imports `lake shake` would remove and add in each module.
+graph's nodes and edges, and the imports `lake shake` would remove and add in each module.
 
 `--main A,B` names the project's main results, as they are written in the source. The dependency
 graph (`dep_graph`) is measured from the largest of them; by default, from the largest declaration