From bff14687186f5ebed756809a67e2c981bcf248c7 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 11 Nov 2024 09:32:53 +0000
Subject: [PATCH 1/5] feat: No docs script

---
 HepLean/AnomalyCancellation/Basic.lean        |   1 +
 HepLean/AnomalyCancellation/GroupActions.lean |   1 +
 .../MSSMNu/OrthogY3B3/ToSols.lean             |   3 +
 lakefile.toml                                 |   4 +
 scripts/MetaPrograms/no_docs.lean             | 105 ++++++++++++++++++
 5 files changed, 114 insertions(+)
 create mode 100644 scripts/MetaPrograms/no_docs.lean

diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
index f54ad884..5c796215 100644
--- a/HepLean/AnomalyCancellation/Basic.lean
+++ b/HepLean/AnomalyCancellation/Basic.lean
@@ -57,6 +57,7 @@ instance chargesModule (χ : ACCSystemCharges) : Module ℚ χ.Charges :=
 instance ChargesAddCommGroup (χ : ACCSystemCharges) : AddCommGroup χ.Charges :=
   Module.addCommMonoidToAddCommGroup ℚ
 
+/-- The module `χ.Charges` over `ℚ` is finite. -/
 instance (χ : ACCSystemCharges) : Module.Finite ℚ χ.Charges :=
   FiniteDimensional.finiteDimensional_pi ℚ
 
diff --git a/HepLean/AnomalyCancellation/GroupActions.lean b/HepLean/AnomalyCancellation/GroupActions.lean
index 4639d5a7..e8fae423 100644
--- a/HepLean/AnomalyCancellation/GroupActions.lean
+++ b/HepLean/AnomalyCancellation/GroupActions.lean
@@ -37,6 +37,7 @@ structure ACCSystemGroupAction (χ : ACCSystem) where
 
 namespace ACCSystemGroupAction
 
+/-- The given instance of a group on the `group` field of a `ACCSystemGroupAction`. -/
 instance {χ : ACCSystem} (G : ACCSystemGroupAction χ) : Group G.group := G.groupInst
 
 /-- The action of a group element on the vector space of linear solutions. -/
diff --git a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
index cb0fd39b..7dc20505 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/OrthogY3B3/ToSols.lean
@@ -39,6 +39,7 @@ namespace AnomalyFreePerp
 and for the cube line to sit in the quad. -/
 def LineEqProp (R : MSSMACC.AnomalyFreePerp) : Prop := α₁ R = 0 ∧ α₂ R = 0 ∧ α₃ R = 0
 
+/-- The proposition `LineEqProp` is decidable. -/
 instance (R : MSSMACC.AnomalyFreePerp) : Decidable (LineEqProp R) := instDecidableAnd
 
 /-- A condition on `Sols` which we will show in `linEqPropSol_iff_proj_linEqProp` that is equivalent
@@ -79,6 +80,7 @@ entirely in the quadratic surface. -/
 def InQuadProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
     quadBiLin R.val R.val = 0 ∧ quadBiLin Y₃.val R.val = 0 ∧ quadBiLin B₃.val R.val = 0
 
+/-- The proposition `InQuadProp` is decidable. -/
 instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InQuadProp R) := instDecidableAnd
 
 /-- A condition which is satisfied if the plane spanned by the solutions `R`, `Y₃` and `B₃`
@@ -124,6 +126,7 @@ def InCubeProp (R : MSSMACC.AnomalyFreePerp) : Prop :=
     cubeTriLin R.val R.val R.val = 0 ∧ cubeTriLin R.val R.val B₃.val = 0 ∧
     cubeTriLin R.val R.val Y₃.val = 0
 
+/-- The proposition `InCubeProp` is decidable. -/
 instance (R : MSSMACC.AnomalyFreePerp) : Decidable (InCubeProp R) := instDecidableAnd
 
 /-- A condition which is satisfied if the plane spanned by the solutions `R`, `Y₃` and `B₃`
diff --git a/lakefile.toml b/lakefile.toml
index 2a30a12a..ac3eea9e 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -64,6 +64,10 @@ srcDir = "scripts"
 name = "free_simps"
 srcDir = "scripts/MetaPrograms"
 
+[[lean_exe]]
+name = "no_docs"
+srcDir = "scripts/MetaPrograms"
+
 [[lean_exe]]
 name = "informal"
 supportInterpreter = true
diff --git a/scripts/MetaPrograms/no_docs.lean b/scripts/MetaPrograms/no_docs.lean
new file mode 100644
index 00000000..b4fa5b5b
--- /dev/null
+++ b/scripts/MetaPrograms/no_docs.lean
@@ -0,0 +1,105 @@
+/-
+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
+/-!
+
+# 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
+
+def Imports.NoDocStringDef (imp : Import) : MetaM UInt32 := do
+  let x := (← Imports.getUserConsts imp).filter (fun c => c.isDef)
+  let x ← x.filterM (fun c => do
+    return Bool.not (← (Name.hasDocString c.name)))
+  let y ← x.filterM (fun c => Name.hasPos c.name)
+  let loc ← y.mapM (fun c => (Name.location c.name))
+  if loc.toList.length > 0 then
+    IO.println "\n"
+    IO.println s!"Module {imp.module} has the following definitions without doc strings:"
+    IO.println (String.intercalate "\n" loc.toList)
+  pure 0
+
+def Imports.NoDocStringLemma (imp : Import) : MetaM UInt32 := do
+  let x := (← Imports.getUserConsts imp).filter (fun c => ¬ c.isDef)
+  let x ← x.filterM (fun c => do
+    return Bool.not (← (Name.hasDocString c.name)))
+  let y ← x.filterM (fun c => Name.hasPos c.name)
+  let loc ← y.mapM (fun c => (Name.location c.name))
+  if loc.toList.length > 0 then
+    IO.println "\n"
+    IO.println s!"Module {imp.module} has the following lemmas without doc strings:"
+    IO.println (String.intercalate "\n" loc.toList)
+  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 _ ← CoreM.withImportModules #[`HepLean] (imports.mapM Imports.NoDocStringDef).run'
+  if "--lemmas" ∈ args then
+    let _ ← CoreM.withImportModules #[`HepLean] (imports.mapM Imports.NoDocStringLemma).run'
+  pure 0

From ad5c329e265cb0a09a4d6e2646ae4bdafadb1d96 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 11 Nov 2024 10:07:25 +0000
Subject: [PATCH 2/5] chore: Test stats workflow

---
 .github/workflows/stats.yml                   | 32 +++++++++++++++++++
 .../MSSMNu/Permutations.lean                  |  1 +
 .../PureU1/BasisLinear.lean                   |  1 +
 .../PureU1/Permutations.lean                  |  1 +
 .../AnomalyCancellation/SM/Permutations.lean  |  2 ++
 HepLean/FlavorPhysics/CKMMatrix/Basic.lean    |  1 +
 HepLean/Lorentz/ComplexTensor/Basic.lean      |  1 +
 7 files changed, 39 insertions(+)
 create mode 100644 .github/workflows/stats.yml

diff --git a/.github/workflows/stats.yml b/.github/workflows/stats.yml
new file mode 100644
index 00000000..d4c5d9df
--- /dev/null
+++ b/.github/workflows/stats.yml
@@ -0,0 +1,32 @@
+on:
+  pull_request:
+
+name: Create and Commit File on Pull Request
+
+jobs:
+  create-and-commit:
+    runs-on: ubuntu-latest
+
+    steps:
+      # Step 1: Checkout the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v3
+
+      # Step 2: Create a file
+      - name: Create a New File
+        run: echo "This is a new file created by the GitHub Actions workflow." > newfile.txt
+
+      # Step 3: Configure Git
+      - name: Set up Git user
+        run: |
+          git config --global user.name "github-actions"
+          git config --global user.email "github-actions@github.com"
+
+      # Step 4: Stage and commit the file
+      - name: Commit and Push Changes
+        run: |
+          git add newfile.txt
+          git commit -m "Automated commit: added newfile.txt"
+          git push origin HEAD:${{ github.head_ref }}
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
diff --git a/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean b/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
index 4a6d218f..078c3bd8 100644
--- a/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
+++ b/HepLean/AnomalyCancellation/MSSMNu/Permutations.lean
@@ -29,6 +29,7 @@ open BigOperators
 @[simp]
 def PermGroup := Fin 6 → Equiv.Perm (Fin 3)
 
+/-- The type `PermGroup` has a group instances derived from the group instance of it's target. -/
 @[simp]
 instance : Group PermGroup := Pi.group
 
diff --git a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
index 22fdc523..ae306e54 100644
--- a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
@@ -120,6 +120,7 @@ noncomputable
 def asBasis : Basis (Fin n) ℚ ((PureU1 n.succ).LinSols) where
   repr := coordinateMap
 
+/-- The module over `ℚ` defined by linear solutions to the pure `U(1)` ACCs is finite. -/
 instance : Module.Finite ℚ ((PureU1 n.succ).LinSols) :=
   Module.Finite.of_basis asBasis
 
diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
index 584a61e5..8f97c655 100644
--- a/HepLean/AnomalyCancellation/PureU1/Permutations.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
@@ -26,6 +26,7 @@ namespace PureU1
 @[simp]
 def PermGroup (n : ℕ) := Equiv.Perm (Fin n)
 
+/-- The type `PermGroup n` inherits the instance of a group from `Equiv.Perm`. -/
 instance {n : ℕ} : Group (PermGroup n) := Equiv.Perm.permGroup
 
 section Charges
diff --git a/HepLean/AnomalyCancellation/SM/Permutations.lean b/HepLean/AnomalyCancellation/SM/Permutations.lean
index 3f3f9f41..8fbc13fb 100644
--- a/HepLean/AnomalyCancellation/SM/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SM/Permutations.lean
@@ -30,6 +30,8 @@ def PermGroup (n : ℕ) := ∀ (_ : Fin 5), Equiv.Perm (Fin n)
 
 variable {n : ℕ}
 
+/-- The type `PermGroup n` inherits the instance of a group from it's
+  target space `Equiv.Perm`.  -/
 @[simp]
 instance : Group (PermGroup n) := Pi.group
 
diff --git a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
index b46cbfe5..2eecfda9 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Basic.lean
@@ -155,6 +155,7 @@ scoped[CKMMatrix] notation (name := ts_element) "[" V "]ts" => V.1 2 1
 /-- The `tb`th element of the CKM matrix. -/
 scoped[CKMMatrix] notation (name := tb_element) "[" V "]tb" => V.1 2 2
 
+/-- The setoid of CKM matrices defined by phase shifts of fermions. -/
 instance CKMMatrixSetoid : Setoid CKMMatrix := ⟨PhaseShiftRelation, phaseShiftRelation_equiv⟩
 
 /-- The matrix obtained from `V` by shifting the phases of the fermions. -/
diff --git a/HepLean/Lorentz/ComplexTensor/Basic.lean b/HepLean/Lorentz/ComplexTensor/Basic.lean
index f65bd7f7..f458838f 100644
--- a/HepLean/Lorentz/ComplexTensor/Basic.lean
+++ b/HepLean/Lorentz/ComplexTensor/Basic.lean
@@ -215,6 +215,7 @@ instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
 instance {n : ℕ} {c : Fin n → complexLorentzTensor.C} :
     Fintype (OverColor.mk c).left := Fin.fintype n
 
+/-- The equality of two maps in `OverColor C` from objects based on `Fin _` is decidable. -/
 instance {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
     {c1 : Fin m → complexLorentzTensor.C} (σ σ' : OverColor.mk c ⟶ OverColor.mk c1) :
     Decidable (σ = σ') :=

From 811b96cf176832794f2a69e06715af80a59d108f Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 11 Nov 2024 10:08:59 +0000
Subject: [PATCH 3/5] Delete stats.yml

---
 .github/workflows/stats.yml | 32 --------------------------------
 1 file changed, 32 deletions(-)
 delete mode 100644 .github/workflows/stats.yml

diff --git a/.github/workflows/stats.yml b/.github/workflows/stats.yml
deleted file mode 100644
index d4c5d9df..00000000
--- a/.github/workflows/stats.yml
+++ /dev/null
@@ -1,32 +0,0 @@
-on:
-  pull_request:
-
-name: Create and Commit File on Pull Request
-
-jobs:
-  create-and-commit:
-    runs-on: ubuntu-latest
-
-    steps:
-      # Step 1: Checkout the repository
-      - name: Checkout Repository
-        uses: actions/checkout@v3
-
-      # Step 2: Create a file
-      - name: Create a New File
-        run: echo "This is a new file created by the GitHub Actions workflow." > newfile.txt
-
-      # Step 3: Configure Git
-      - name: Set up Git user
-        run: |
-          git config --global user.name "github-actions"
-          git config --global user.email "github-actions@github.com"
-
-      # Step 4: Stage and commit the file
-      - name: Commit and Push Changes
-        run: |
-          git add newfile.txt
-          git commit -m "Automated commit: added newfile.txt"
-          git push origin HEAD:${{ github.head_ref }}
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}

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 4/5] 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 7edaaa3f..5d496aeb 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 a8aaa9c3..f91f7390 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 00000000..bfb5a271
--- /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 b4fa5b5b..4f6800d5 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 3a14bca9..f823e7d4 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
+---
+<!DOCTYPE html>
+<html>
+<head>
+    <title>Stats for HepLean</title>
+     <meta name=\"viewport\" content=\"width=device-width, initial-scale=1.0\">
+     <style>
+        /* Style the progress bar to be wider and take up more space */
+        progress {
+            width: 80%; /* Adjust to take up more horizontal space */
+            height: 30px; /* Increase height to make it wider */
+            appearance: none; /* Remove default browser styles */
+        }
 
-instance : ToString FileStats where
-  toString fs := s!"Number of definitions: {fs.numDefs}\n" ++
-    s!"Number of lemmas without doc string: {fs.numLemsWithoutDocString}\n" ++
-    s!"Number of lemmas with doc string: {fs.numLemsWithDocString}"
+        /* Change the color for WebKit browsers (Chrome, Safari, etc.) */
+        progress::-webkit-progress-bar {
+            background-color: #f3f3f3; /* Background color */
+            border-radius: 5px;
+            overflow: hidden;
+        }
 
-def getConstantDoc (constName : Array ConstantInfo) : MetaM (FileStats) := do
-  let env ← getEnv
-  let mut numDefs := 0
-  let mut numLemsWithoutDocString := 0
-  let mut numLemsWithDocString := 0
-  for c in constName do
-    if ¬ Lean.Name.isInternalDetail c.name then
-      if c.isDef then
-        numDefs := numDefs + 1
-      if c.isThm then
-        let doc ← Lean.findDocString? env c.name
-        if doc == none then
-          numLemsWithoutDocString := numLemsWithoutDocString + 1
-        else
-          numLemsWithDocString := numLemsWithDocString + 1
-  return {numDefs := numDefs,
-          numLemsWithoutDocString := numLemsWithoutDocString,
-          numLemsWithDocString := numLemsWithDocString}
+        progress::-webkit-progress-value {
+            background-color: #157878; /* Change this to your desired color */
+            border-radius: 5px;
+        }
 
-def getStats (imp : Import) : MetaM FileStats := do
-  if imp.module == `Init then
-    return {numDefs := 0,
-            numLemsWithoutDocString := 0,
-            numLemsWithDocString := 0}
-  let mFile ← findOLean imp.module
-  let (modData, _) ← readModuleData mFile
-  let cons := modData.constants
-  let out ← (getConstantDoc cons)
-  return out
+        /* Change the color for Firefox */
+        progress::-moz-progress-bar {
+            background-color: #157878; /* Change this to your desired color */
+        }
+    </style>
+</head>
+<body>"
+  let body := s!"
+<h1>Stats for HepLean</h1>
+<h3>Number of Files 📄: {noImportsVal}</h3>
+<h3>Number of lines 💻: {noLinesVal}</h3>
+<h3>Number of Definitions (incl. instances): {noDefsVal - noInformalLemmasVal}</h3>
+<p>- Of which {noDefsVal - noDefsNoDocVal- noInformalLemmasVal} have doc-strings:</p>
+<progress value=\"{noDefsVal - noDefsNoDocVal- noInformalLemmasVal}\" max=\"{noDefsVal- noInformalLemmasVal}\"></progress>
+<p>- Of which {noDefsVal - noInformalLemmasVal - noInformalDefsVal} are not informal definitions:</p>
+<progress value=\"{noDefsVal - noInformalLemmasVal - noInformalDefsVal}\" max=\"{noDefsVal - noInformalLemmasVal}\"></progress>
 
-def getStatsArray (a : Array Import) : MetaM (Array FileStats) := do
-  return ← a.mapM getStats
+<h3>Number of Lemmas: {noLemmasVal + noInformalLemmasVal}</h3>
+<p>- Of which {noLemmasVal - noLemmasNoDocVal + noInformalLemmasVal} have doc-strings:</p>
+<progress value=\"{noLemmasVal - noLemmasNoDocVal + noInformalLemmasVal}\" max=\"{noLemmasVal + noInformalLemmasVal}\"></progress>
+<p>- Of which {noLemmasVal} are not informal lemmas:</p>
+<progress value=\"{noLemmasVal}\" max=\"{noLemmasVal + noInformalLemmasVal}\"></progress>
+   "
+  let footer := "
+</body>
+</html>
+"
+  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

From 63fcbf3da7786c8adb122e26e6ab8e358f9375f4 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 11 Nov 2024 11:38:33 +0000
Subject: [PATCH 5/5] feat: More stats

---
 HepLean/Meta/Basic.lean | 15 +++++++++++++++
 scripts/stats.lean      |  9 +++++++--
 2 files changed, 22 insertions(+), 2 deletions(-)

diff --git a/HepLean/Meta/Basic.lean b/HepLean/Meta/Basic.lean
index bfb5a271..922d1a50 100644
--- a/HepLean/Meta/Basic.lean
+++ b/HepLean/Meta/Basic.lean
@@ -175,4 +175,19 @@ def noInformalDefs : MetaM Nat := do
   let x := x.filter (Informal.isInformalDef)
   pure x.toList.length
 
+/-- The number of TODO items. -/
+def noTODOs : IO Nat := do
+  let imports ← HepLean.allImports
+  let x ← imports.mapM HepLean.Imports.getLines
+  let x := x.flatten
+  let x := x.filter fun l => l.startsWith "/-! TODO:"
+  pure x.size
+
+/-- The number of files with a TODO item. -/
+def noFilesWithTODOs : IO Nat := do
+  let imports ← HepLean.allImports
+  let x ← imports.mapM HepLean.Imports.getLines
+  let x := x.filter (fun M => M.any fun l => l.startsWith "/-! TODO:")
+  pure x.size
+
 end HepLean
diff --git a/scripts/stats.lean b/scripts/stats.lean
index f823e7d4..ebba0684 100644
--- a/scripts/stats.lean
+++ b/scripts/stats.lean
@@ -41,6 +41,8 @@ unsafe def Stats.toHtml : MetaM String := do
   let noLinesVal ← noLines
   let noInformalDefsVal ← noInformalDefs
   let noInformalLemmasVal ← noInformalLemmas
+  let noTODOsVal ← noTODOs
+  let noFilesWithTODOsVal ← noFilesWithTODOs
   let header := "---
 layout: default
 ---
@@ -83,14 +85,17 @@ layout: default
 <h3>Number of Definitions (incl. instances): {noDefsVal - noInformalLemmasVal}</h3>
 <p>- Of which {noDefsVal - noDefsNoDocVal- noInformalLemmasVal} have doc-strings:</p>
 <progress value=\"{noDefsVal - noDefsNoDocVal- noInformalLemmasVal}\" max=\"{noDefsVal- noInformalLemmasVal}\"></progress>
-<p>- Of which {noDefsVal - noInformalLemmasVal - noInformalDefsVal} are not informal definitions:</p>
+<p>- Of which {noDefsVal - noInformalLemmasVal - noInformalDefsVal} are not <a href=\"https://heplean.github.io/HepLean/InformalGraph.html\">informal definitions</a>:</p>
 <progress value=\"{noDefsVal - noInformalLemmasVal - noInformalDefsVal}\" max=\"{noDefsVal - noInformalLemmasVal}\"></progress>
 
 <h3>Number of Lemmas: {noLemmasVal + noInformalLemmasVal}</h3>
 <p>- Of which {noLemmasVal - noLemmasNoDocVal + noInformalLemmasVal} have doc-strings:</p>
 <progress value=\"{noLemmasVal - noLemmasNoDocVal + noInformalLemmasVal}\" max=\"{noLemmasVal + noInformalLemmasVal}\"></progress>
-<p>- Of which {noLemmasVal} are not informal lemmas:</p>
+<p>- Of which {noLemmasVal} are not <a href=\"https://heplean.github.io/HepLean/InformalGraph.html\">informal lemmas</a>:</p>
 <progress value=\"{noLemmasVal}\" max=\"{noLemmasVal + noInformalLemmasVal}\"></progress>
+<h3>Number of <a href=\"https://heplean.github.io/HepLean/TODOList\">TODOs</a>: {noTODOsVal}</h3>
+<p>- There are {noImportsVal - noFilesWithTODOsVal} (of {noImportsVal}) files which are TODO free:</p>
+<progress value=\"{noImportsVal - noFilesWithTODOsVal}\" max=\"{noImportsVal}\"></progress>
    "
   let footer := "
 </body>