From 1c303f87414825b1a24945830bdee0d3ba09e781 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Mon, 11 Nov 2024 11:23:27 +0000 Subject: [PATCH] feat: Stats page --- .github/workflows/docs.yml | 3 + HepLean.lean | 1 + HepLean/Meta/Basic.lean | 178 ++++++++++++++++++++++++++++++ scripts/MetaPrograms/no_docs.lean | 67 +---------- scripts/stats.lean | 152 ++++++++++++++----------- 5 files changed, 272 insertions(+), 129 deletions(-) create mode 100644 HepLean/Meta/Basic.lean diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 7edaaa3..5d496ae 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -47,6 +47,9 @@ jobs: - name: make list of informal proofs and lemmas run : lake exe informal mkFile mkDot mkHTML + - name: make stats page + run : lake exe stats mkHTML + - name: Generate svg from dot run : dot -Tsvg -o ./docs/graph.svg ./docs/InformalDot.dot diff --git a/HepLean.lean b/HepLean.lean index a8aaa9c..f91f739 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -108,6 +108,7 @@ import HepLean.Mathematics.LinearMaps import HepLean.Mathematics.PiTensorProduct import HepLean.Mathematics.SO3.Basic import HepLean.Meta.AllFilePaths +import HepLean.Meta.Basic import HepLean.Meta.Informal import HepLean.Meta.TransverseTactics import HepLean.SpaceTime.Basic diff --git a/HepLean/Meta/Basic.lean b/HepLean/Meta/Basic.lean new file mode 100644 index 0000000..bfb5a27 --- /dev/null +++ b/HepLean/Meta/Basic.lean @@ -0,0 +1,178 @@ +/- +Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license. +Authors: Joseph Tooby-Smith +-/ +import Batteries.Lean.HashSet +import Lean +import Mathlib.Lean.Expr.Basic +import Mathlib.Lean.CoreM +import ImportGraph.RequiredModules +import HepLean.Meta.Informal +/-! + +## Basic Lean meta programming commands + +-/ + +namespace HepLean +open Lean System Meta + +/-! + +## Imports + +-/ + +/-- Gets all imports within HepLean. -/ +def allImports : IO (Array Import) := do + initSearchPath (← findSysroot) + let mods : Name := `HepLean + let imp : Import := {module := mods} + let mFile ← findOLean imp.module + unless (← mFile.pathExists) do + throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist" + let (hepLeanMod, _) ← readModuleData mFile + let imports := hepLeanMod.imports.filter (fun c => c.module ≠ `Init) + return imports + +/-- Number of files within HepLean. -/ +def noImports : IO Nat := do + let imports ← allImports + pure imports.size + +/-- Gets all constants from an import. -/ +def Imports.getConsts (imp : Import) : IO (Array ConstantInfo) := do + let mFile ← findOLean imp.module + let (modData, _) ← readModuleData mFile + pure modData.constants + +/-- Gets all user defined constants from an import. -/ +def Imports.getUserConsts (imp : Import) : MetaM (Array ConstantInfo) := do + let env ← getEnv + let x := (← Imports.getConsts imp).filter (fun c => ¬ c.name.isInternal) + let x := x.filter (fun c => ¬ Lean.isCasesOnRecursor env c.name) + let x := x.filter (fun c => ¬ Lean.isRecOnRecursor env c.name) + let x := x.filter (fun c => ¬ Lean.isNoConfusion env c.name) + let x := x.filter (fun c => ¬ Lean.isBRecOnRecursor env c.name) + let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.binductionOnSuffix) + let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.belowSuffix) + let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.ibelowSuffix) + /- Removing syntax category declarations. -/ + let x := x.filter (fun c => ¬ c.name.toString = "Informal.informalAssignment.quot" ) + let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.indexExpr.quot" ) + let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.tensorExpr.quot" ) + pure x + +/-- Lines from import. -/ +def Imports.getLines (imp : Import) : IO (Array String) := do + let filePath := (mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean" + let lines ← IO.FS.lines filePath + return lines + +/-! + +## Name + +-/ + + +/-- Turns a name into a Lean file. -/ +def Name.toFile (c : Name) : MetaM String := do + return s!"./{c.toString.replace "." "/" ++ ".lean"}" + +/-- Given a name, returns the line number. -/ +def Name.lineNumber (c : Name) : MetaM Nat := do + match ← findDeclarationRanges? c with + | some decl => pure decl.range.pos.line + | none => panic! s!"{c} is a declaration without position" + +/-- Returns the location of a name. -/ +def Name.location (c : Name) : MetaM String := do + let env ← getEnv + let x := env.getModuleFor? c + match x with + | some decl => pure ((← Name.toFile decl) ++ ":" ++ toString (← Name.lineNumber c) ++ " " + ++ c.toString) + | none => panic! s!"{c} is a declaration without position" + +/-- Determines if a name has a location. -/ +def Name.hasPos (c : Name) : MetaM Bool := do + match ← findDeclarationRanges? c with + | some _ => pure true + | none => pure false + +/-- Determines if a name has a doc string. -/ +def Name.hasDocString (c : Name) : MetaM Bool := do + let env ← getEnv + let doc ← Lean.findDocString? env c + match doc with + | some _ => pure true + | none => pure false + +/-- Number of definitions. -/ +def noDefs : MetaM Nat := do + let imports ← allImports + let x ← imports.mapM Imports.getUserConsts + let x := x.flatten + let x := x.filter (fun c => c.isDef) + let x ← x.filterM (fun c => (Name.hasPos c.name)) + pure x.toList.length + +/-- Number of definitions. -/ +def noLemmas : MetaM Nat := do + let imports ← allImports + let x ← imports.mapM Imports.getUserConsts + let x := x.flatten + let x := x.filter (fun c => ¬ c.isDef) + let x ← x.filterM (fun c => (Name.hasPos c.name)) + pure x.toList.length + +/-- Number of definitions without a doc-string. -/ +def noDefsNoDocString : MetaM Nat := do + let imports ← allImports + let x ← imports.mapM Imports.getUserConsts + let x := x.flatten + let x := x.filter (fun c => c.isDef) + let x ← x.filterM (fun c => (Name.hasPos c.name)) + let x ← x.filterM (fun c => do + return Bool.not (← (Name.hasDocString c.name))) + pure x.toList.length + +/-- Number of definitions without a doc-string. -/ +def noLemmasNoDocString : MetaM Nat := do + let imports ← allImports + let x ← imports.mapM Imports.getUserConsts + let x := x.flatten + let x := x.filter (fun c => ¬ c.isDef) + let x ← x.filterM (fun c => (Name.hasPos c.name)) + let x ← x.filterM (fun c => do + return Bool.not (← (Name.hasDocString c.name))) + pure x.toList.length + +/-- The number of lines in HepLean. -/ +def noLines : IO Nat := do + let imports ← HepLean.allImports + let x ← imports.mapM HepLean.Imports.getLines + let x := x.flatten + pure x.toList.length + +/-- The number of informal lemmas in HepLean. -/ +def noInformalLemmas : MetaM Nat := do + let imports ← allImports + let x ← imports.mapM Imports.getUserConsts + let x := x.flatten + let x := x.filter (Informal.isInformal) + let x := x.filter (Informal.isInformalLemma) + pure x.toList.length + +/-- The number of informal definitions in HepLean. -/ +def noInformalDefs : MetaM Nat := do + let imports ← allImports + let x ← imports.mapM Imports.getUserConsts + let x := x.flatten + let x := x.filter (Informal.isInformal) + let x := x.filter (Informal.isInformalDef) + pure x.toList.length + +end HepLean diff --git a/scripts/MetaPrograms/no_docs.lean b/scripts/MetaPrograms/no_docs.lean index b4fa5b5..4f6800d 100644 --- a/scripts/MetaPrograms/no_docs.lean +++ b/scripts/MetaPrograms/no_docs.lean @@ -3,68 +3,14 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import Batteries.Lean.HashSet -import Lean -import Mathlib.Lean.Expr.Basic -import Mathlib.Lean.CoreM -import HepLean.Meta.Informal -import ImportGraph.RequiredModules +import HepLean.Meta.Basic /-! # Extracting commands with no doc strings. -/ -open Lean System Meta - -def Imports.getConsts (imp : Import) : IO (Array ConstantInfo) := do - let mFile ← findOLean imp.module - let (modData, _) ← readModuleData mFile - pure modData.constants - -def Imports.getUserConsts (imp : Import) : MetaM (Array ConstantInfo) := do - let env ← getEnv - let x := (← Imports.getConsts imp).filter (fun c => ¬ c.name.isInternal) - let x := x.filter (fun c => ¬ Lean.isCasesOnRecursor env c.name) - let x := x.filter (fun c => ¬ Lean.isRecOnRecursor env c.name) - let x := x.filter (fun c => ¬ Lean.isNoConfusion env c.name) - let x := x.filter (fun c => ¬ Lean.isBRecOnRecursor env c.name) - let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.binductionOnSuffix) - let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.belowSuffix) - let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.ibelowSuffix) - /- Removing syntax category declarations. -/ - let x := x.filter (fun c => ¬ c.name.toString = "Informal.informalAssignment.quot" ) - let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.indexExpr.quot" ) - let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.tensorExpr.quot" ) - pure x - -def Name.lineNumber (c : Name) : MetaM Nat := do - match ← findDeclarationRanges? c with - | some decl => pure decl.range.pos.line - | none => panic! s!"{c} is a declaration without position" - -def Name.toFile (c : Name) : MetaM String := do - return s!"./{c.toString.replace "." "/" ++ ".lean"}" - -def Name.location (c : Name) : MetaM String := do - let env ← getEnv - let x := env.getModuleFor? c - match x with - | some decl => pure ((← Name.toFile decl) ++ ":" ++ toString (← Name.lineNumber c) ++ " " - ++ c.toString) - | none => panic! s!"{c} is a declaration without position" - -def Name.hasPos (c : Name) : MetaM Bool := do - match ← findDeclarationRanges? c with - | some _ => pure true - | none => pure false - -def Name.hasDocString (c : Name) : MetaM Bool := do - let env ← getEnv - let doc ← Lean.findDocString? env c - match doc with - | some _ => pure true - | none => pure false +open Lean System Meta HepLean def Imports.NoDocStringDef (imp : Import) : MetaM UInt32 := do let x := (← Imports.getUserConsts imp).filter (fun c => c.isDef) @@ -91,14 +37,7 @@ def Imports.NoDocStringLemma (imp : Import) : MetaM UInt32 := do pure 0 unsafe def main (args : List String) : IO UInt32 := do - initSearchPath (← findSysroot) - let mods : Name := `HepLean - let imp : Import := {module := mods} - let mFile ← findOLean imp.module - unless (← mFile.pathExists) do - throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist" - let (hepLeanMod, _) ← readModuleData mFile - let imports := hepLeanMod.imports.filter (fun c => c.module ≠ `Init) + let imports ← allImports let _ ← CoreM.withImportModules #[`HepLean] (imports.mapM Imports.NoDocStringDef).run' if "--lemmas" ∈ args then let _ ← CoreM.withImportModules #[`HepLean] (imports.mapM Imports.NoDocStringLemma).run' diff --git a/scripts/stats.lean b/scripts/stats.lean index 3a14bca..f823e7d 100644 --- a/scripts/stats.lean +++ b/scripts/stats.lean @@ -3,11 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ -import Batteries.Lean.HashSet -import Lean -import Mathlib.Lean.Expr.Basic -import Mathlib.Lean.CoreM -import HepLean +import HepLean.Meta.Basic /-! # HepLean Stats @@ -17,72 +13,98 @@ This file concerns with statistics of HepLean. -/ -open Lean System Meta +open Lean System Meta HepLean -structure FileStats where - numDefs : Nat - numLemsWithoutDocString : Nat - numLemsWithDocString : Nat -def FileStats.add (a b : FileStats) : FileStats where - numDefs := a.numDefs + b.numDefs - numLemsWithoutDocString := a.numLemsWithoutDocString + b.numLemsWithoutDocString - numLemsWithDocString := a.numLemsWithDocString + b.numLemsWithDocString +def getStats : MetaM String := do + let noDefsVal ← noDefs + let noLemmasVal ← noLemmas + let noImportsVal ← noImports + let noDefsNoDocVal ← noDefsNoDocString + let noLemmasNoDocVal ← noLemmasNoDocString + let noLinesVal ← noLines + let s := s!" + Number of Imports: {noImportsVal} + Number of Definitions: {noDefsVal} + Number of Lemmas: {noLemmasVal} + Number of Definitions without doc strings: {noDefsNoDocVal} (out of {noDefsVal}) + Number of Lemmas without doc strings: {noLemmasNoDocVal} (out of {noLemmasVal}) + Number of Lines: {noLinesVal}" + pure s -def FileStats.zero : FileStats where - numDefs := 0 - numLemsWithoutDocString := 0 - numLemsWithDocString := 0 +unsafe def Stats.toHtml : MetaM String := do + let noDefsVal ← noDefs + let noLemmasVal ← noLemmas + let noImportsVal ← noImports + let noDefsNoDocVal ← noDefsNoDocString + let noLemmasNoDocVal ← noLemmasNoDocString + let noLinesVal ← noLines + let noInformalDefsVal ← noInformalDefs + let noInformalLemmasVal ← noInformalLemmas + let header := "--- +layout: default +--- + + + + Stats for HepLean + + + +" + let body := s!" +

Stats for HepLean

+

Number of Files 📄: {noImportsVal}

+

Number of lines 💻: {noLinesVal}

+

Number of Definitions (incl. instances): {noDefsVal - noInformalLemmasVal}

+

- Of which {noDefsVal - noDefsNoDocVal- noInformalLemmasVal} have doc-strings:

+ +

- Of which {noDefsVal - noInformalLemmasVal - noInformalDefsVal} are not informal definitions:

+ -def getStatsArray (a : Array Import) : MetaM (Array FileStats) := do - return ← a.mapM getStats +

Number of Lemmas: {noLemmasVal + noInformalLemmasVal}

+

- Of which {noLemmasVal - noLemmasNoDocVal + noInformalLemmasVal} have doc-strings:

+ +

- Of which {noLemmasVal} are not informal lemmas:

+ + " + let footer := " + + +" + pure (header ++ "\n" ++ body ++ "\n" ++ footer) -def main (_ : List String) : IO UInt32 := do - initSearchPath (← findSysroot) - let mods : Name := `HepLean - let imp : Import := {module := mods} - let mFile ← findOLean imp.module - unless (← mFile.pathExists) do - throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist" - let (hepLeanMod, _) ← readModuleData mFile - let noFiles := hepLeanMod.imports.size - 1 - let fileStats ← CoreM.withImportModules #[`HepLean] (getStatsArray hepLeanMod.imports).run' - let totalStats := Array.foldl FileStats.add FileStats.zero fileStats - IO.println s!"Total number of files: {noFiles}" - IO.println totalStats +unsafe def main (args : List String) : IO UInt32 := do + let _ ← noImports + let statString ← CoreM.withImportModules #[`HepLean] (getStats).run' + println! statString + if "mkHTML" ∈ args then + let html ← CoreM.withImportModules #[`HepLean] (Stats.toHtml).run' + let htmlFile : System.FilePath := {toString := "./docs/Stats.html"} + IO.FS.writeFile htmlFile html + IO.println (s!"HTML file made.") pure 0