Merge pull request #290 from HEPLean/Docs

feat: Update TODO list mechanism
HEPLean · Jan 22, 2025 · f8722d2 · f8722d2
2 parents 36d3be1 + 793a67b
commit f8722d2
Show file tree

Hide file tree

Showing 37 changed files with 183 additions and 42 deletions.
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -42,7 +42,7 @@ jobs:
         run: lake -Kenv=dev build HepLean
 
       - name: make TODO list
-        run : lake exe find_TODOs mkFile
+        run : lake exe TODO_to_yml mkFile
 
       - name: make list of informal proofs and lemmas
         run : lake exe informal mkFile mkDot mkHTML

diff --git a/HepLean.lean b/HepLean.lean
@@ -117,6 +117,7 @@ import HepLean.Meta.Notes.Basic
 import HepLean.Meta.Notes.HTMLNote
 import HepLean.Meta.Notes.NoteFile
 import HepLean.Meta.Notes.ToHTML
+import HepLean.Meta.TODO.Basic
 import HepLean.Meta.TransverseTactics
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.NormalOrder

diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Mathematics.LinearMaps
+import HepLean.Meta.TODO.Basic
 import Mathlib.LinearAlgebra.FiniteDimensional.Defs
 /-!
 # Basic set up for anomaly cancellation conditions
@@ -13,9 +14,9 @@ This file defines the basic structures for the anomaly cancellation conditions.
 It defines a module structure on the charges, and the solutions to the linear ACCs.
 
 -/
-/-! TODO: Derive an ACC system from a guage algebra and fermionic representations. -/
-/-! TODO: Relate ACC Systems to algebraic varieties. -/
-/-! TODO: Refactor whole file, and dependent files. -/
+TODO "Derive an ACC system from a guage algebra and fermionic representations."
+TODO "Relate ACC Systems to algebraic varieties."
+TODO "Refactor whole file, and dependent files."
 
 /-- A system of charges, specified by the number of charges. -/
 structure ACCSystemCharges where

diff --git a/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/BasisLinear.lean
@@ -75,7 +75,7 @@ lemma sum_of_vectors {n : ℕ} (f : Fin k → (PureU1 n).LinSols) (j : Fin n) :
     (∑ i : Fin k, (f i)).1 j = (∑ i : Fin k, (f i).1 j) :=
   sum_of_anomaly_free_linear (fun i => f i) j
 
-/-! TODO: replace `Finsupp.equivFunOnFinite` here with `Finsupp.linearEquivFunOnFinite`. -/
+TODO "replace `Finsupp.equivFunOnFinite` here with `Finsupp.linearEquivFunOnFinite`."
 /-- The coordinate map for the basis. -/
 noncomputable
 def coordinateMap : (PureU1 n.succ).LinSols ≃ₗ[ℚ] Fin n →₀ ℚ where

diff --git a/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
@@ -616,7 +616,7 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n) → ℚ) : Pa' f = Pa' f' ↔ f =
     linarith
   · rw [h]
 
-/-! TODO: Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`. -/
+TODO "Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`."
 /-- A helper function for what follows. -/
 def join (g : Fin n.succ → ℚ) (f : Fin n → ℚ) : (Fin n.succ) ⊕ (Fin n) → ℚ := fun i =>
   match i with

diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@@ -623,7 +623,7 @@ lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ) : Pa' f = Pa' f' ↔
     linarith
   · rw [h]
 
-/-! TODO: Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`. -/
+TODO "Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`."
 /-- A helper function for what follows. -/
 def join (g f : Fin n → ℚ) : Fin n ⊕ Fin n → ℚ := fun i =>
   match i with

diff --git a/HepLean/AnomalyCancellation/PureU1/Permutations.lean b/HepLean/AnomalyCancellation/PureU1/Permutations.lean
@@ -89,7 +89,7 @@ lemma FamilyPermutations_anomalyFreeLinear_apply (S : (PureU1 n).LinSols)
     ((FamilyPermutations n).linSolRep f S).val i = S.val (f.invFun i) := by
   rfl
 
-/-! TODO: Replace the definition of `pairSwap` with `Equiv.swap`. -/
+TODO "Replace the definition of `pairSwap` with `Equiv.swap`."
 /-- The permutation which swaps i and j. -/
 def pairSwap {n : ℕ} (i j : Fin n) : (FamilyPermutations n).group where
   toFun s :=

diff --git a/HepLean/AnomalyCancellation/PureU1/VectorLike.lean b/HepLean/AnomalyCancellation/PureU1/VectorLike.lean
@@ -10,7 +10,7 @@ import HepLean.AnomalyCancellation.PureU1.Sorts
 For the `n`-even case we define the property of a charge assignment being vector like.
 
 -/
-/-! TODO: Define vector like ACC in the `n`-odd case. -/
+TODO "Define vector like ACC in the `n`-odd case."
 universe v u
 
 open Nat

diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.StandardModel.HiggsBoson.Potential
+import HepLean.Meta.TODO.Basic
 /-!
 
 # The Two Higgs Doublet Model
@@ -144,9 +145,9 @@ lemma left_eq_neg_right : P.toFun Φ1 (- Φ1) =
 
 -/
 
-/-! TODO: Prove bounded properties of the 2HDM potential.
+TODO "Prove bounded properties of the 2HDM potential.
   See e.g. https://inspirehep.net/literature/201299 and
-  https://arxiv.org/pdf/hep-ph/0605184. -/
+  https://arxiv.org/pdf/hep-ph/0605184."
 
 /-- The proposition on the coefficients for a potential to be bounded. -/
 def IsBounded : Prop :=

diff --git a/HepLean/Lorentz/Algebra/Basis.lean b/HepLean/Lorentz/Algebra/Basis.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Lorentz.Algebra.Basic
+import HepLean.Meta.TODO.Basic
 /-!
 # Basis of the Lorentz Algebra
 
@@ -15,4 +16,4 @@ This file is waiting for Lorentz Tensors to be done formally, before
 it can be completed.
 
 -/
-/-! TODO: Define the standard basis of the Lorentz algebra. -/
+TODO "Define the standard basis of the Lorentz algebra."
diff --git a/HepLean/Lorentz/ComplexTensor/Basis.lean b/HepLean/Lorentz/ComplexTensor/Basis.lean
@@ -8,6 +8,7 @@ import HepLean.Tensors.Tree.NodeIdentities.PermContr
 import HepLean.Tensors.Tree.NodeIdentities.ProdComm
 import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
 import HepLean.Tensors.Tree.NodeIdentities.ContrContr
+import HepLean.Meta.TODO.Basic
 /-!
 
 ## Basis vectors associated with complex Lorentz tensors
@@ -47,7 +48,7 @@ lemma perm_basisVector_cast {n m : ℕ} {c : Fin n → complexLorentzTensor.C}
   simp only [Functor.const_obj_obj, OverColor.mk_hom] at h1
   rw [h1]
 
-/-! TODO: Generalize `basis_eq_FD`. -/
+TODO "Generalize `basis_eq_FD`."
 lemma basis_eq_FD {n : ℕ} (c : Fin n → complexLorentzTensor.C)
     (b : Π j, Fin (complexLorentzTensor.repDim (c j))) (i : Fin n)
     (h : { as := c i } = { as := c1 }) :

diff --git a/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean b/HepLean/Lorentz/ComplexTensor/PauliMatrices/CoContractContr.lean
@@ -388,7 +388,7 @@ lemma pauliMatrix_contr_lower_3_1_1 :
   · congr 2
     decide
 
-/-! TODO: Work out why `pauliCo_prod_basis_expand'` is needed. -/
+TODO "Work out why `pauliCo_prod_basis_expand'` is needed."
 /-- This lemma is exactly the same as `pauliCo_prod_basis_expand`.
   It is needed here for `pauliMatrix_contract_pauliMatrix_aux`. It is unclear why
   `pauliMatrix_lower_basis_expand_prod` does not work. -/

diff --git a/HepLean/Lorentz/ComplexVector/Basic.lean b/HepLean/Lorentz/ComplexVector/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Lorentz.ComplexVector.Modules
+import HepLean.Meta.TODO.Basic
 /-!
 
 # Complex Lorentz vectors
@@ -128,7 +129,7 @@ lemma inclCongrRealLorentz_ρ (M : SL(2, ℂ)) (v : ContrMod 3) :
   rw [LorentzGroup.toComplex_mulVec_ofReal]
   rfl
 
-/-! TODO: Rename. -/
+TODO "Rename."
 lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
     (complexContr.ρ M) (complexContrBasis i) =
     ∑ j, (SL2C.toLorentzGroup M).1 j i •
@@ -140,6 +141,6 @@ lemma SL2CRep_ρ_basis (M : SL(2, ℂ)) (i : Fin 1 ⊕ Fin 3) :
   simp only [LinearMap.map_smulₛₗ, ofRealHom_eq_coe, coe_smul]
   rw [complexContrBasis_of_real]
 
-/-! TODO: Include relation to real Lorentz vectors. -/
+TODO "Include relation to real Lorentz vectors."
 end Lorentz
 end
diff --git a/HepLean/Lorentz/Group/Basic.lean b/HepLean/Lorentz/Group/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Lorentz.MinkowskiMatrix
+import HepLean.Meta.TODO.Basic
 /-!
 # The Lorentz Group
 
@@ -14,7 +15,7 @@ We define the Lorentz group.
 - http://home.ku.edu.tr/~amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf
 
 -/
-/-! TODO: Show that the Lorentz is a Lie group. -/
+TODO "Show that the Lorentz group is a Lie group."
 
 noncomputable section
 

diff --git a/HepLean/Lorentz/Group/Boosts.lean b/HepLean/Lorentz/Group/Boosts.lean
@@ -21,7 +21,7 @@ A boost is the special case of a generalised boost when `u = stdBasis 0`.
   https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
 
 -/
-/-! TODO: Show that generalised boosts are in the restricted Lorentz group. -/
+TODO "Show that generalised boosts are in the restricted Lorentz group."
 noncomputable section
 
 namespace LorentzGroup

diff --git a/HepLean/Lorentz/Group/Orthochronous.lean b/HepLean/Lorentz/Group/Orthochronous.lean
@@ -12,7 +12,7 @@ We define the give a series of lemmas related to the orthochronous property of l
 matrices.
 
 -/
-/-! TODO: Prove topological properties of the Orthochronous Lorentz Group. -/
+TODO "Prove topological properties of the Orthochronous Lorentz Group."
 
 noncomputable section
 

diff --git a/HepLean/Lorentz/Group/Restricted.lean b/HepLean/Lorentz/Group/Restricted.lean
@@ -10,9 +10,9 @@ import HepLean.Lorentz.Group.Orthochronous
 This file is currently a stub.
 
 -/
-/-! TODO: Add definition of the restricted Lorentz group. -/
-/-! TODO: Prove member of the restricted Lorentz group is combo of boost and rotation. -/
-/-! TODO: Prove restricted Lorentz group equivalent to connected component of identity. -/
+TODO "Add definition of the restricted Lorentz group."
+TODO "Prove member of the restricted Lorentz group is combo of boost and rotation."
+TODO "Prove restricted Lorentz group equivalent to connected component of identity."
 
 noncomputable section
 

diff --git a/HepLean/Lorentz/Group/Rotations.lean b/HepLean/Lorentz/Group/Rotations.lean
@@ -11,7 +11,7 @@ import HepLean.Mathematics.SO3.Basic
 This file describes the embedding of `SO(3)` into `LorentzGroup 3`.
 
 -/
-/-! TODO: Generalize the inclusion of rotations into LorentzGroup to abitary dimension. -/
+TODO "Generalize the inclusion of rotations into LorentzGroup to abitary dimension."
 noncomputable section
 
 namespace LorentzGroup

diff --git a/HepLean/Lorentz/SL2C/Basic.lean b/HepLean/Lorentz/SL2C/Basic.lean
@@ -312,7 +312,7 @@ informal_lemma toRestrictedLorentzGroup where
   deps :≈ [``toLorentzGroup, ``toLorentzGroup_det_one, ``toLorentzGroup_isOrthochronous,
     ``LorentzGroup.Restricted]
 
-/-! TODO: Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group. -/
+TODO "Define homomorphism from `SL(2, ℂ)` to the restricted Lorentz group."
 end
 end SL2C
 

diff --git a/HepLean/Mathematics/LinearMaps.lean b/HepLean/Mathematics/LinearMaps.lean
@@ -6,14 +6,15 @@ Authors: Joseph Tooby-Smith
 import Mathlib.Tactic.Polyrith
 import Mathlib.Algebra.Module.LinearMap.Defs
 import Mathlib.Data.Fintype.BigOperators
+import HepLean.Meta.TODO.Basic
 /-!
 # Linear maps
 
 Some definitions and properties of linear, bilinear, and trilinear maps, along with homogeneous
 quadratic and cubic equations.
 
 -/
-/-! TODO: Replace the definitions in this file with Mathlib definitions. -/
+TODO "Replace the definitions in this file with Mathlib definitions."
 
 /-- The structure defining a homogeneous quadratic equation. -/
 @[simp]

diff --git a/HepLean/Meta/AllFilePaths.lean b/HepLean/Meta/AllFilePaths.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import Lean
+import HepLean.Meta.TODO.Basic
 /-!
 
 ## Getting an array of all file paths in HepLean.
@@ -12,7 +13,7 @@ import Lean
 
 open Lean Elab System
 
-/-! TODO: Make this definition more functional in style. -/
+TODO "Make this definition more functional in style."
 
 /-- The recursive function underlying `allFilePaths`. -/
 partial def allFilePaths.go (prev : Array FilePath)

diff --git a/HepLean/Meta/Basic.lean b/HepLean/Meta/Basic.lean
@@ -196,14 +196,14 @@ 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:"
+  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:")
+  let x := x.filter (fun M => M.any fun l => l.startsWith "TODO ")
   pure x.size
 
 end HepLean
diff --git a/HepLean/Meta/Informal/Basic.lean b/HepLean/Meta/Informal/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import Lean
+import HepLean.Meta.TODO.Basic
 /-!
 
 ## Informal definitions and lemmas
@@ -16,7 +17,7 @@ Everything else about informal definitions and lemmas are in the `Informal.Post`
 -/
 open Lean Elab System
 
-/-! TODO: Can likely make this a bona-fide command. -/
+TODO "Can likely make this a bona-fide command."
 
 /-- The structure representing an informal definition. -/
 structure InformalDefinition where

diff --git a/HepLean/Meta/TODO/Basic.lean b/HepLean/Meta/TODO/Basic.lean
@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Batteries.Lean.HashSet
+import Mathlib.Lean.Expr.Basic
+import Mathlib.Lean.CoreM
+import ImportGraph.RequiredModules
+/-!
+
+# Basic underlying structure for TODOs.
+
+-/
+
+namespace HepLean
+open Lean System Meta
+
+/-- The information from a `TODO ...` command. -/
+structure todoInfo where
+  /-- The content of the note. -/
+  content : String
+  /-- The file name where the note came from. -/
+  fileName : Name
+  /-- The line from where the note came from. -/
+  line : Nat
+
+/-- Environment extension to store `todo ...`. -/
+initialize todoExtension : SimplePersistentEnvExtension todoInfo (Array todoInfo) ←
+  registerSimplePersistentEnvExtension {
+    name := `todoExtension
+    addEntryFn := fun arr todoInfor => arr.push todoInfor
+    addImportedFn := fun es => es.foldl (· ++ ·) #[]
+  }
+
+/-- Syntax for the `TODO ...` command. -/
+syntax (name := todo_comment) "TODO " str : command
+
+/-- Elaborator for the `TODO ...` command -/
+@[command_elab todo_comment]
+def elabTODO : Lean.Elab.Command.CommandElab := fun stx =>
+  match stx with
+  | `(TODO $s) => do
+    let str : String := s.getString
+    let pos := stx.getPos?
+    match pos with
+    | some pos => do
+      let env ← getEnv
+      let fileMap ← getFileMap
+      let filePos := fileMap.toPosition pos
+      let line := filePos.line
+      let modName := env.mainModule
+      let todoInfo : todoInfo := { content := str, fileName := modName, line := line }
+      modifyEnv fun env => todoExtension.addEntry env todoInfo
+    | none => throwError "Invalid syntax for `TODO` command"
+  | _ => throwError "Invalid syntax for `TODO` command"
+
+end HepLean
diff --git a/HepLean/Meta/TransverseTactics.lean b/HepLean/Meta/TransverseTactics.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import Lean
+import HepLean.Meta.TODO.Basic
 /-!
 
 This file enables us to transverse tactics and test for conditions.
@@ -74,8 +75,8 @@ def traverseForest (file : FilePath)
 
 end transverseTactics
 
-/-! TODO: Find a way to free the environment `env` in `transverseTactics`.
-  This leads to memory problems when using `transverseTactics` directly in loops. -/
+TODO "Find a way to free the environment `env` in `transverseTactics`.
+  This leads to memory problems when using `transverseTactics` directly in loops."
 open transverseTactics in
 /-- Applies `visitTacticInfo` to each tactic in a file. -/
 unsafe def transverseTactics (file : FilePath)

diff --git a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
@@ -371,7 +371,7 @@ lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
 
 -/
 
-/-! TODO: Split the following two lemmas up into smaller parts. -/
+TODO "Split the following two lemmas up into smaller parts."
 
 lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
     (φc φc' : 𝓕.CrAnStates) (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)