refactor: Lint

HepLean.lean

@@ -107,6 +107,9 @@ import HepLean.Mathematics.SuperAlgebra.Basic
 import HepLean.Meta.AllFilePaths
 import HepLean.Meta.Basic
 import HepLean.Meta.Informal
+import HepLean.Meta.Notes.Basic
+import HepLean.Meta.Notes.HTMLNote
+import HepLean.Meta.Notes.ToHTML
 import HepLean.Meta.TransverseTactics
 import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
 import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar

HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean

@@ -3,11 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FlavorPhysics.CKMMatrix.Basic
-import HepLean.FlavorPhysics.CKMMatrix.Rows
 import HepLean.FlavorPhysics.CKMMatrix.Relations
-import Mathlib.Analysis.SpecialFunctions.Complex.Arg
-import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
 /-!
 # Phase freedom of the CKM Matrix
 

HepLean/Meta/Basic.lean

@@ -117,7 +117,6 @@ def Name.hasDocString (c : Name) : MetaM Bool := do
   | some _ => pure true
   | none => pure false
 
-
 /-- Given a name, returns the source code defining that name. -/
 def Name.getDeclString (name : Name) : MetaM String := do
   let env ← getEnv
@@ -128,7 +127,7 @@ def Name.getDeclString (name : Name) : MetaM String := do
     let endLine := decl.range.endPos
     let fileName? := env.getModuleFor? name
     match fileName? with
-    | some fileName  =>
+    | some fileName =>
       let fileContent ← IO.FS.readFile { toString := (← Name.toFile fileName)}
       let fileMap := fileContent.toFileMap
       let startPos := fileMap.ofPosition startLine

HepLean/Meta/Informal.lean

@@ -105,7 +105,15 @@ def $name : InformalDefinition := {
 syntax (name := informal_definition_note) "informal_definition_note " ident
   " where " (colGt informalAssignment)* : command
 
-macro "informal_definition_note " name:ident " where " assignments:informalAssignment* : command => do
+/-- An informal definition is a definition which is not type checked, and is written
+  as a string literal. It can be used to plan out sections for future formalization, or to
+  include results which the formalization is not immediately known.
+  Each informal definition must included a
+  `math :≈ "..."`
+  entry, but can also include the following entries
+  `physics :≈ "..."`, `ref :≈ "..."`, and `deps :≈ [...]`. -/
+macro "informal_definition_note " name:ident " where " assignments:informalAssignment* :
+    command => do
   let mut math_def? : Option (TSyntax `term) := none
   let mut physics_def? : Option (TSyntax `term) := none
   let mut ref_def? : Option (TSyntax `term) := none
@@ -184,7 +192,6 @@ def $name : InformalLemma := {
   dependencies := $(dep_def?.getD (← `([])))
     })
 
-
 /-- The syntax for the command `informal_lemma`. -/
 syntax (name := informal_lemma_note) "informal_lemma_note " ident " where "
   (colGt informalAssignment)* : command

HepLean/Meta/Notes/Basic.lean

@@ -17,30 +17,31 @@ import ImportGraph.RequiredModules
 namespace HepLean
 open Lean System Meta
 
--- Define the structure to hold note information, including module name
+/-- The information from a `note ...` command. To be used in a note file-/
 structure NoteInfo 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
-  deriving Inhabited
 
--- Define the environment extension to store notes
+/-- Enviroment extention to store `note ...`. -/
 initialize noteExtension : SimplePersistentEnvExtension NoteInfo (Array NoteInfo) ←
   registerSimplePersistentEnvExtension {
-    name          := `noteExtension
-    addEntryFn    := fun arr nodeInfor => arr.push nodeInfor
-    addImportedFn := fun es => es.foldl (· ++ ·) #[]  -- Merge imported notes
+    name := `noteExtension
+    addEntryFn := fun arr nodeInfor => arr.push nodeInfor
+    addImportedFn := fun es => es.foldl (· ++ ·) #[]
   }
 
--- Define the syntax for the `note` command
+/-- Syntax for the `note ...` command -/
 syntax (name := note_comment) "note " str : command
 
--- Define the elaboration behavior (do nothing)
+/-- Elaborator for the `note ...` command -/
 @[command_elab note_comment]
 def elabNote : Lean.Elab.Command.CommandElab := fun stx =>
   match stx with
   | `(note $s) => do
-
     let str : String := s.getString
     let pos := stx.getPos?
     match pos with
@@ -56,43 +57,46 @@ def elabNote : Lean.Elab.Command.CommandElab := fun stx =>
     | none => throwError "Invalid syntax for `note` command"
   | _ => throwError "Invalid syntax for `note` command"
 
-
-
 /-!
 
 ## Note attribute
 
 -/
 
+/-- Enviroment extention to store `note_attr`. -/
 initialize noteDeclExtension : SimplePersistentEnvExtension Name (Array Name) ←
   registerSimplePersistentEnvExtension {
-    name          := `noteDeclExtension
-    addEntryFn    := fun arr nodeInfor => arr.push nodeInfor
-    addImportedFn := fun es => es.foldl (· ++ ·) #[]  -- Merge imported notes
+    name := `noteDeclExtension
+    addEntryFn := fun arr nodeInfor => arr.push nodeInfor
+    addImportedFn := fun es => es.foldl (· ++ ·) #[]
   }
 
+/-- The `note_attr` attribute is used to display formally verified commands within a note. -/
 initialize noteAttribute : Unit ←
   registerBuiltinAttribute {
-    name  := `note_attr
+    name := `note_attr
     descr := "Note attribute"
     applicationTime := AttributeApplicationTime.afterCompilation
-    add   := fun declName _ _ => do
+    add := fun declName _ _ => do
       modifyEnv fun env => noteDeclExtension.addEntry env declName
   }
 
+
+/-- Enviroment extention to store `note_attr_informal`. -/
 initialize noteInformalDeclExtension : SimplePersistentEnvExtension Name (Array Name) ←
   registerSimplePersistentEnvExtension {
-    name          := `noteInformalDeclExtension
-    addEntryFn    := fun arr nodeInfor => arr.push nodeInfor
-    addImportedFn := fun es => es.foldl (· ++ ·) #[]  -- Merge imported notes
+    name := `noteInformalDeclExtension
+    addEntryFn := fun arr nodeInfor => arr.push nodeInfor
+    addImportedFn := fun es => es.foldl (· ++ ·) #[]
   }
 
+/-- The `note_attr_informal` attribute is used to display informal commands within a note. -/
 initialize noteInformalAttribute : Unit ←
   registerBuiltinAttribute {
-    name  := `note_attr_informal
+    name := `note_attr_informal
     descr := "Informal note attribute"
     applicationTime := AttributeApplicationTime.afterCompilation
-    add   := fun declName _ _ => do
+    add := fun declName _ _ => do
       modifyEnv fun env => noteInformalDeclExtension.addEntry env declName
   }
 
@@ -104,9 +108,13 @@ initialize noteInformalAttribute : Unit ←
 
 /-- A note consists of a title and a list of Lean files which make up the note. -/
 structure NoteFile where
+  /-- The overall title of the note. -/
   title : String
+  /-- The abstract of the note. -/
   abstract : String
+  /-- A list of authors. -/
   authors : List String
+  /-- The files making up the note in the order in which they should appear. -/
   files : List Name
 
 namespace NoteFile

HepLean/Meta/Notes/HTMLNote.lean

@@ -15,29 +15,34 @@ import HepLean.Meta.Informal
 namespace HepLean
 open Lean System Meta
 
+/-- A `HTMLNote` is a structure containing the html information from
+  invidual contributions (commands, informal commands, note ..) etc. to a note file. -/
 structure HTMLNote where
+  /-- The name of the file the contribution came from. -/
   fileName : Name
+  /-- The html contribution of the content. -/
   content : String
+  /-- The line in the file where the contribution came from. -/
   line : Nat
 
-
-
-def noteInfoToHTMLNote (ni : NoteInfo) : MetaM HTMLNote := do
+/-- Converts a note infor into a HTMLNote. -/
+def HTMLNote.ofNodeInfo (ni : NoteInfo) : MetaM HTMLNote := do
   let line := ni.line
-  let decl :=  ni.content
+  let decl := ni.content
   let fileName := ni.fileName
   pure { content := decl, fileName := fileName, line := line }
 
-def formalToHTMLNote (name : Name) :  MetaM HTMLNote := do
+/-- An formal definition or lemma to html for a note. -/
+def HTMLNote.ofFormal (name : Name) : MetaM HTMLNote := do
   let line ← Name.lineNumber name
   let decl ← Name.getDeclString name
   let fileName ← Name.fileName name
   let content := "<pre><code>" ++ decl ++ "</code></pre>"
   pure { content := content, fileName := fileName, line := line }
 
-unsafe def informalToHTMLNote (name : Name) :  MetaM HTMLNote := do
+/-- An informal definition or lemma to html for a note. -/
+unsafe def HTMLNote.ofInformal (name : Name) : MetaM HTMLNote := do
   let line ← Name.lineNumber name
-  let decl ← Name.getDeclString name
   let fileName ← Name.fileName name
   let constInfo ← getConstInfo name
   let mut content := ""

HepLean/Meta/Notes/ToHTML.lean

@@ -19,7 +19,7 @@ variable (N : NoteFile)
 
 /-- Sorts `NoteInfo`'s by file name then by line number. -/
 def sortLE (ni1 ni2 : HTMLNote) : Bool :=
-  if  N.files.indexOf ni1.fileName ≠  N.files.indexOf ni2.fileName
+  if N.files.indexOf ni1.fileName ≠ N.files.indexOf ni2.fileName
   then N.files.indexOf ni1.fileName ≤ N.files.indexOf ni2.fileName
   else
   ni1.line ≤ ni2.line
@@ -30,12 +30,13 @@ unsafe def getNodeInfo : MetaM (List HTMLNote) := do
   let allNotes := (noteExtension.getState env)
   let allDecl := (noteDeclExtension.getState env)
   let allInformalDecl := noteInformalDeclExtension.getState env
-  let allNoteInfo := (← allNotes.mapM noteInfoToHTMLNote) ++ (← allDecl.mapM formalToHTMLNote)
-    ++ (← allInformalDecl.mapM informalToHTMLNote)
+  let allNoteInfo := (← allNotes.mapM HTMLNote.ofNodeInfo) ++ (← allDecl.mapM HTMLNote.ofFormal)
+    ++ (← allInformalDecl.mapM HTMLNote.ofInformal)
   let noteInfo := allNoteInfo.filter (fun x => x.fileName ∈ N.files)
   let noteInfoSort := noteInfo.toList.mergeSort N.sortLE
   pure noteInfoSort
 
+/-- The HTML code needed to have syntax highlighting. -/
 def codeBlockHTML : String := "
 <meta charset=\"UTF-8\">
     <meta name=\"viewport\" content=\"width=device-width, initial-scale=1.0\">
@@ -48,7 +49,7 @@ def codeBlockHTML : String := "
     <script>
       hljs.registerLanguage('lean', function(hljs) {
           return {
-              keywords: 'def theorem axiomatic structure lemma informal_definition_note informal_lemma_note',
+              keywords: 'def theorem axiomatic structure lemma',
               contains: [
                   hljs.COMMENT('--', '$'),
                   hljs.C_NUMBER_MODE,
@@ -56,15 +57,14 @@ def codeBlockHTML : String := "
                 {
                     className: 'operator', // Define a class for styling
                     begin: /[:=+\\-*/<>|&!~^{}]/ // Regex for operators
-                }
-
-              ]
+                }]
           };
       });
       hljs.highlightAll();
       </script>
 "
 
+/-- The html styles for informal definitions. -/
 def informalDefStyle : String :=
 "
 <style>
@@ -99,7 +99,8 @@ def informalDefStyle : String :=
 </style>
 "
 
-def headerHTML : String  :=
+/-- The header to the html code. -/
+def headerHTML : String :=
 "---
 layout: default
 ---
@@ -109,18 +110,21 @@ layout: default
 </head>
 <body>"
 
+/-- The html code corresponding to the title, abstract and authors. -/
 def titleHTML : String :=
 "<center><h1 style=\"font-size: 50px;\">" ++ N.title ++ "</h1></center>
 <center><b>Authors:</b> " ++ String.intercalate ", " N.authors ++ "</center>
 <center><b>Abstract:</b> " ++ N.abstract ++ "</center>"
 
+/-- The footor of the html file. -/
 def footerHTML : String :=
 "</body>
 </html>"
 
+/-- The html file associated to a NoteFile string. -/
 unsafe def toHTMLString : MetaM String := do
   let string := String.intercalate "\n" ((← N.getNodeInfo).map (fun x => x.content))
-  pure (headerHTML ++ N.titleHTML ++  string ++ footerHTML)
+  pure (headerHTML ++ N.titleHTML ++ string ++ footerHTML)
 
 end NoteFile
 end HepLean

HepLean/PerturbationTheory/FeynmanDiagrams/Light.lean

@@ -56,7 +56,7 @@ informal_definition _root_.Wick.Contract.toFeynmanDiagram_isConnected_iff where
   deps :≈ [``Wick.WickContract.IsConnected, ``FeynmanDiagram.IsConnected]
 
 /-! TODO: Define an equivalence relation on Wick contracts related to the their underlying tensors
-  been equal after permutation. Show that two  Wick contractions are equal under this
+  been equal after permutation. Show that two Wick contractions are equal under this
   equivalence relation if and only if they have the same Feynman diagram. First step
   is to turn these statements into appropriate informal lemmas and definitions. -/
 

HepLean/PerturbationTheory/Wick/Algebra.lean

@@ -131,7 +131,7 @@ informal_lemma timeOrder_pair where
 
 informal_definition WickMap where
   math :≈ "A linear map `vev` from the Wick algebra `A` to the underlying field such that
-     `vev(...ψd(t)) = 0` and `vev(ψc(t)...) = 0`."
+    `vev(...ψd(t)) = 0` and `vev(ψc(t)...) = 0`."
   physics :≈ "An abstraction of the notion of a vacuum expectation value, containing
     the necessary properties for lots of theorems to hold."
   deps :≈ [``WickAlgebra, ``WickMonomial]