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] 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