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] 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 bfb5a27..922d1a5 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 f823e7d..ebba068 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>