Merge pull request #260 from HEPLean/Notes

feat: Infrastructure for notes

.github/workflows/docs.yml

@@ -50,6 +50,9 @@ jobs:
       - name: make stats page
         run : lake exe stats mkHTML
 
+      - name: make notes
+        run : lake exe notes
+
       - name: Generate svg from dot
         run : dot -Tsvg -o ./docs/graph.svg ./docs/InformalDot.dot
 

HepLean.lean

@@ -106,7 +106,12 @@ import HepLean.Mathematics.SO3.Basic
 import HepLean.Mathematics.SuperAlgebra.Basic
 import HepLean.Meta.AllFilePaths
 import HepLean.Meta.Basic
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
+import HepLean.Meta.Informal.Post
+import HepLean.Meta.Notes.Basic
+import HepLean.Meta.Notes.HTMLNote
+import HepLean.Meta.Notes.NoteFile
+import HepLean.Meta.Notes.ToHTML
 import HepLean.Meta.TransverseTactics
 import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
 import HepLean.PerturbationTheory.FeynmanDiagrams.Instances.ComplexScalar

HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.StandardModel.Basic
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 
 # The Georgi-Glashow Model

HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.StandardModel.Basic
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 
 # The Pati-Salam Model

HepLean/BeyondTheStandardModel/Spin10/Basic.lean

@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.BeyondTheStandardModel.PatiSalam.Basic
 import HepLean.BeyondTheStandardModel.GeorgiGlashow.Basic
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 
 # The Spin(10) Model

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/Lorentz/ComplexVector/Basic.lean

@@ -7,7 +7,7 @@ import Mathlib.Data.Complex.Exponential
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import HepLean.Lorentz.SL2C.Basic
 import HepLean.Lorentz.ComplexVector.Modules
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 import Mathlib.RepresentationTheory.Rep
 import HepLean.Lorentz.PauliMatrices.SelfAdjoint
 /-!

HepLean/Lorentz/ComplexVector/Modules.lean

@@ -3,7 +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.Meta.Informal
+import HepLean.Meta.Informal.Basic
 import HepLean.Lorentz.SL2C.Basic
 import Mathlib.RepresentationTheory.Rep
 import Mathlib.Logic.Equiv.TransferInstance

HepLean/Lorentz/Group/Restricted.lean

@@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
 import HepLean.Lorentz.Group.Basic
 import HepLean.Lorentz.Group.Proper
 import HepLean.Lorentz.Group.Orthochronous
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 # The Restricted Lorentz Group
 

HepLean/Lorentz/RealVector/Basic.lean

@@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
 import Mathlib.Data.Complex.Exponential
 import Mathlib.Analysis.InnerProductSpace.PiL2
 import HepLean.Lorentz.Group.Basic
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 import Mathlib.RepresentationTheory.Rep
 import HepLean.Lorentz.RealVector.Modules
 /-!

HepLean/Lorentz/RealVector/Modules.lean

@@ -3,7 +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.Meta.Informal
+import HepLean.Meta.Informal.Basic
 import HepLean.Lorentz.Group.Basic
 import Mathlib.RepresentationTheory.Rep
 import Mathlib.Logic.Equiv.TransferInstance

HepLean/Lorentz/SL2C/Basic.lean

@@ -8,7 +8,7 @@ import HepLean.Lorentz.RealVector.Basic
 import Mathlib.RepresentationTheory.Basic
 import HepLean.Lorentz.Group.Restricted
 import HepLean.Lorentz.PauliMatrices.SelfAdjoint
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 # The group SL(2, ℂ) and it's relation to the Lorentz group
 

HepLean/Lorentz/Weyl/Basic.lean

@@ -3,7 +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.Meta.Informal
+import HepLean.Meta.Informal.Basic
 import HepLean.Lorentz.SL2C.Basic
 import Mathlib.RepresentationTheory.Rep
 import HepLean.Lorentz.Weyl.Modules

HepLean/Lorentz/Weyl/Modules.lean

@@ -3,7 +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.Meta.Informal
+import HepLean.Meta.Informal.Basic
 import HepLean.Lorentz.SL2C.Basic
 import Mathlib.RepresentationTheory.Rep
 import Mathlib.Logic.Equiv.TransferInstance

HepLean/Mathematics/SuperAlgebra/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import Mathlib.RingTheory.GradedAlgebra.Basic
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 
 # Super Algebras

HepLean/Meta/Basic.lean

@@ -8,7 +8,7 @@ import Lean
 import Mathlib.Lean.Expr.Basic
 import Mathlib.Lean.CoreM
 import ImportGraph.RequiredModules
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 
 ## Basic Lean meta programming commands
@@ -80,12 +80,27 @@ def Imports.getLines (imp : Import) : IO (Array String) := do
 def Name.toFile (c : Name) : MetaM String := do
   return s!"./{c.toString.replace "." "/" ++ ".lean"}"
 
+/-- Turns a name, which represents a module, into a link to github. -/
+def Name.toGitHubLink (c : Name) (l : Nat := 0) : MetaM String := do
+  let headerLink := "https://github.com/HEPLean/HepLean/blob/master/"
+  let filePart := (c.toString.replace "." "/") ++ ".lean"
+  let linePart := "#L" ++ toString l
+  return headerLink ++ filePart ++ linePart
+
 /-- 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"
 
+/-- Given a name, returns the file name corresponding to that declaration. -/
+def Name.fileName (c : Name) : MetaM Name := do
+  let env ← getEnv
+  let x := env.getModuleFor? c
+  match x with
+  | some c => pure c
+  | 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
@@ -109,6 +124,27 @@ 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
+  let decl ← findDeclarationRanges? name
+  match decl with
+  | some decl =>
+    let startLine := decl.range.pos
+    let endLine := decl.range.endPos
+    let fileName? := env.getModuleFor? name
+    match fileName? with
+    | some fileName =>
+      let fileContent ← IO.FS.readFile { toString := (← Name.toFile fileName)}
+      let fileMap := fileContent.toFileMap
+      let startPos := fileMap.ofPosition startLine
+      let endPos := fileMap.ofPosition endLine
+      let text := fileMap.source.extract startPos endPos
+      pure text
+    | none =>
+        pure ""
+  | none => pure ""
+
 /-- Number of definitions. -/
 def noDefs : MetaM Nat := do
   let imports ← allImports
@@ -156,24 +192,6 @@ def noLines : IO Nat := do
   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
-
 /-- The number of TODO items. -/
 def noTODOs : IO Nat := do
   let imports ← HepLean.allImports

HepLean/Meta/Informal/Basic.lean

@@ -8,11 +8,14 @@ import Lean
 
 ## Informal definitions and lemmas
 
+This file contains the necessary structures that must be imported into a file
+for it to contain informal definitions and lemmas.
+
+Everything else about informal definitions and lemmas are in the `Informal.Post` module.
+
 -/
 open Lean Elab System
 
-/-! TODO: Derive a means to extract informal definitions and informal lemmas. -/
-
 /-! TODO: Can likely make this a bona-fide command. -/
 
 /-- The structure representating an informal definition. -/
@@ -54,6 +57,11 @@ syntax (name := informalAssignment) ident ":≈" str : informalAssignment
 /-- The syntax describing an informal assignment of `ident` to a list. -/
 syntax (name := informalAssignmentDeps) ident ":≈" "[" sepBy(term, ",") "]" : informalAssignment
 
+/-!
+
+## Syntax
+
+-/
 /-- The syntax for the command informal_definition. -/
 syntax (name := informal_definition) "informal_definition " ident
   " where " (colGt informalAssignment)* : command
@@ -96,6 +104,50 @@ def $name : InformalDefinition := {
   dependencies := $(dep_def?.getD (← `([])))
     })
 
+/-- The syntax for the command informal_definition. -/
+syntax (name := informal_definition_note) "informal_definition_note " ident
+  " where " (colGt informalAssignment)* : command
+
+/-- 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
+  let mut dep_def? : Option (TSyntax `term) := none
+  for assignment in assignments do
+    match assignment with
+    | `(informalAssignment| physics :≈ $val:str) =>
+      let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for physics"
+      physics_def? := some (← `($(Lean.quote strVal)))
+    | `(informalAssignment| math :≈ $val:str) =>
+      let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math"
+      math_def? := some (← `($(Lean.quote strVal)))
+    | `(informalAssignment| ref :≈ $val:str) =>
+      let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
+      ref_def? := some (← `($(Lean.quote strVal)))
+    | `(informalAssignmentDeps| deps :≈ [$deps,*]) =>
+      dep_def? := some (← `([$deps,*]))
+    | _ => Macro.throwError "invalid assignment syntax in informal_definition"
+  unless math_def?.isSome do
+    Macro.throwError "A 'math' assignments is required"
+  `(
+/-- An informal definition. -/
+@[note_attr_informal]
+def $name : InformalDefinition := {
+  name := $(Lean.quote name.getId),
+  physics := $(physics_def?.getD (← `("No physics description provided"))),
+  math := $(math_def?.getD (panic! "math not assigned")),
+  ref := $(ref_def?.getD (← `("No references provided"))),
+  dependencies := $(dep_def?.getD (← `([])))
+    })
+
 /-- The syntax for the command `informal_lemma`. -/
 syntax (name := informal_lemma) "informal_lemma " ident " where "
   (colGt informalAssignment)* : command
@@ -133,7 +185,6 @@ macro "informal_lemma " name:ident " where " assignments:informalAssignment* : c
   unless math_def?.isSome do
     Macro.throwError "A 'math' assignments is required"
   `(
-
 /-- An informal lemma. -/
 def $name : InformalLemma := {
   name := $(Lean.quote name.getId),
@@ -144,26 +195,52 @@ def $name : InformalLemma := {
   dependencies := $(dep_def?.getD (← `([])))
     })
 
-/-- Is true if and only if a `ConstantInfo` corresponds to an `InformalLemma` or a
-  `InformalDefinition`. -/
-def isInformal (c : ConstantInfo) : Bool :=
-  match c with
-  | ConstantInfo.defnInfo c =>
-    if c.type.isAppOf ``InformalDefinition ∨ c.type.isAppOf ``InformalLemma then true else false
-  | _ => false
+/-- The syntax for the command `informal_lemma`. -/
+syntax (name := informal_lemma_note) "informal_lemma_note " ident " where "
+  (colGt informalAssignment)* : command
 
-/-- Is true if and only if a `ConstantInfo` corresponds to an `InformalLemma`. -/
-def isInformalLemma (c : ConstantInfo) : Bool :=
-  match c with
-  | ConstantInfo.defnInfo c =>
-    if c.type.isAppOf ``InformalLemma then true else false
-  | _ => false
-
-/-- Is true if and only if a `ConstantInfo` corresponds to an `InformalDefinition`. -/
-def isInformalDef (c : ConstantInfo) : Bool :=
-  match c with
-  | ConstantInfo.defnInfo c =>
-    if c.type.isAppOf ``InformalDefinition then true else false
-  | _ => false
+/-- An informal lemma is a lemma 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.
+  Every informal lemma must included a
+  `math :≈ "..."`
+  entry, but can also include the following entries
+  `physics :≈ "..."`, `proof :≈ "..."`, `ref :≈ "..."`, and `deps :≈ [...]`. -/
+macro "informal_lemma_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 proof_def? : Option (TSyntax `term) := none
+  let mut ref_def? : Option (TSyntax `term) := none
+  let mut dep_def? : Option (TSyntax `term) := none
+  for assignment in assignments do
+    match assignment with
+    | `(informalAssignment| physics :≈ $val:str) =>
+      let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for physics"
+      physics_def? := some (← `($(Lean.quote strVal)))
+    | `(informalAssignment| math :≈ $val:str) =>
+      let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for math"
+      math_def? := some (← `($(Lean.quote strVal)))
+    | `(informalAssignment| proof :≈ $val:str) =>
+      let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for proof"
+      proof_def? := some (← `($(Lean.quote strVal)))
+    | `(informalAssignment| ref :≈ $val:str) =>
+      let some strVal := val.raw.isStrLit? | Macro.throwError "Expected string literal for ref"
+      ref_def? := some (← `($(Lean.quote strVal)))
+    | `(informalAssignmentDeps| deps :≈ [$deps,*]) =>
+      dep_def? := some (← `([$deps,*]))
+    | _ => Macro.throwError "invalid assignment syntax"
+  unless math_def?.isSome do
+    Macro.throwError "A 'math' assignments is required"
+  `(
+/-- An informal lemma. -/
+@[note_attr_informal]
+def $name : InformalLemma := {
+  name := $(Lean.quote name.getId),
+  physics := $(physics_def?.getD (← `("No physics description provided"))),
+  math := $(math_def?.getD (panic! "math not assigned")),
+  proof := $(proof_def?.getD (← `("No proof description provided"))),
+  ref := $(ref_def?.getD (← `("No references provided"))),
+  dependencies := $(dep_def?.getD (← `([])))
+    })
 
 end Informal

HepLean/Meta/Informal/Post.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Meta.Informal.Basic
+import HepLean.Meta.Basic
+/-!
+
+## Informal definitions and lemmas
+
+-/
+open Lean Elab System
+
+namespace Informal
+
+/-- Is true if and only if a `ConstantInfo` corresponds to an `InformalLemma` or a
+  `InformalDefinition`. -/
+def isInformal (c : ConstantInfo) : Bool :=
+  match c with
+  | ConstantInfo.defnInfo c =>
+    if c.type.isAppOf ``InformalDefinition ∨ c.type.isAppOf ``InformalLemma then true else false
+  | _ => false
+
+/-- Is true if and only if a `ConstantInfo` corresponds to an `InformalLemma`. -/
+def isInformalLemma (c : ConstantInfo) : Bool :=
+  match c with
+  | ConstantInfo.defnInfo c =>
+    if c.type.isAppOf ``InformalLemma then true else false
+  | _ => false
+
+/-- Is true if and only if a `ConstantInfo` corresponds to an `InformalDefinition`. -/
+def isInformalDef (c : ConstantInfo) : Bool :=
+  match c with
+  | ConstantInfo.defnInfo c =>
+    if c.type.isAppOf ``InformalDefinition then true else false
+  | _ => false
+
+/-- Takes a `ConstantInfo` corresponding to a `InformalLemma` and returns
+  the corresponding `InformalLemma`. -/
+unsafe def constantInfoToInformalLemma (c : ConstantInfo) : MetaM InformalLemma := do
+  match c with
+  | ConstantInfo.defnInfo c =>
+      Lean.Meta.evalExpr' InformalLemma ``InformalLemma c.value
+  | _ => panic! "Passed constantInfoToInformalLemma a `ConstantInfo` that is not a `InformalLemma`"
+
+/-- Takes a `ConstantInfo` corresponding to a `InformalDefinition` and returns
+  the corresponding `InformalDefinition`. -/
+unsafe def constantInfoToInformalDefinition (c : ConstantInfo) : MetaM InformalDefinition := do
+  match c with
+  | ConstantInfo.defnInfo c =>
+      Lean.Meta.evalExpr' InformalDefinition ``InformalDefinition c.value
+  | _ => panic! "Passed constantInfoToInformalDefinition a
+    `ConstantInfo` that is not a `InformalDefinition`"
+
+end Informal
+
+namespace HepLean
+
+/-- 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

HepLean/Meta/Notes/Basic.lean

@@ -0,0 +1,112 @@
+/-
+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
+/-!
+
+## Underlying structure for notes
+
+This file contains the necessary structures that must be imported into a file
+for it to be turned into a Lean note.
+
+It allows for the
+- `note ...` command to be used to add notes to a Lean file
+- `note_attr` attribute to be used to display formally verified commands within a note.
+- `note_attr_informal` attribute to be used to display informal commands within a note.
+
+Other results relating to notes are in other files.
+
+-/
+
+namespace HepLean
+open Lean System Meta
+
+/-- 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
+
+/-- 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 (· ++ ·) #[]
+  }
+
+/-- Syntax for the `note ...` command -/
+syntax (name := note_comment) "note " str : command
+
+/-- 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
+    | some pos => do
+      let env ← getEnv
+      let fileMap ← getFileMap
+      let filePos := fileMap.toPosition pos
+      let line := filePos.line
+      let modName := env.mainModule
+      let noteInfo : NoteInfo := { content := str, fileName := modName, line := line }
+      modifyEnv fun env => noteExtension.addEntry env noteInfo
+
+    | 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 (· ++ ·) #[]
+  }
+
+/-- The `note_attr` attribute is used to display formally verified commands within a note. -/
+initialize noteAttribute : Unit ←
+  registerBuiltinAttribute {
+    name := `note_attr
+    descr := "Note attribute"
+    applicationTime := AttributeApplicationTime.afterCompilation
+    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 (· ++ ·) #[]
+  }
+
+/-- The `note_attr_informal` attribute is used to display informal commands within a note. -/
+initialize noteInformalAttribute : Unit ←
+  registerBuiltinAttribute {
+    name := `note_attr_informal
+    descr := "Informal note attribute"
+    applicationTime := AttributeApplicationTime.afterCompilation
+    add := fun declName _ _ => do
+      modifyEnv fun env => noteInformalDeclExtension.addEntry env declName
+  }
+
+end HepLean

HepLean/Meta/Notes/HTMLNote.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Meta.Notes.NoteFile
+import HepLean.Meta.Basic
+import HepLean.Meta.Informal.Post
+/-!
+
+## Turns a delaration into a html note structure.
+
+-/
+
+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
+
+/-- Converts a note infor into a HTMLNote. -/
+def HTMLNote.ofNodeInfo (ni : NoteInfo) : MetaM HTMLNote := do
+  let line := ni.line
+  let decl := ni.content
+  let fileName := ni.fileName
+  pure { content := decl, fileName := fileName, line := line }
+
+/-- 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 }
+
+/-- 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 fileName ← Name.fileName name
+  let constInfo ← getConstInfo name
+  let webAddress : String ← Name.toGitHubLink fileName line
+  let mut content := ""
+  if Informal.isInformalDef constInfo then
+    let X ← Informal.constantInfoToInformalDefinition constInfo
+    content := "<div class=\"informal-def\">"
+      ++ "<a href=\"" ++ webAddress ++ "\" class=\"button\">Improve/Formalize</a>"
+      ++"<b>Informal definition:</b> " ++ name.toString ++ "<br>"
+      ++ X.math.replace "\n" "<br>"
+      ++ "</div>"
+  else if Informal.isInformalLemma constInfo then
+    let X ← Informal.constantInfoToInformalLemma constInfo
+    content := "Informal definition: " ++ name.toString ++ "\n" ++ X.math
+    content := "Informal lemma: " ++ name.toString
+  pure { content := content, fileName := fileName, line := line }
+
+end HepLean

HepLean/Meta/Notes/NoteFile.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Meta.Notes.Basic
+/-!
+
+# Note file
+
+A note file is a structure which contains the information to go into a note.
+
+-/
+
+namespace HepLean
+open Lean System Meta
+
+/-- 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
+
+variable (N : NoteFile)
+
+/-- All imports associated to a note. -/
+def imports : Array Import := (N.files.map fun f => {module := f}).toArray
+
+end NoteFile
+
+end HepLean

HepLean/Meta/Notes/ToHTML.lean

@@ -0,0 +1,144 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Meta.Notes.HTMLNote
+import HepLean.Meta.Basic
+/-!
+
+## Turns a delaration into a html note structure.
+
+-/
+
+namespace HepLean
+open Lean System Meta
+
+namespace NoteFile
+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
+  then N.files.indexOf ni1.fileName ≤ N.files.indexOf ni2.fileName
+  else
+  ni1.line ≤ ni2.line
+
+/-- Returns a sorted list of NodeInfos for a file system. -/
+unsafe def getNodeInfo : MetaM (List HTMLNote) := do
+  let env ← getEnv
+  let allNotes := (noteExtension.getState env)
+  let allDecl := (noteDeclExtension.getState env)
+  let allInformalDecl := noteInformalDeclExtension.getState env
+  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\">
+    <!-- Include Highlight.js CSS -->
+    <link rel=\"stylesheet\" href=\"https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.8.0/styles/default.min.css\">
+    <!-- Include Highlight.js -->
+    <script src=\"https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.8.0/highlight.min.js\"></script>
+    <!-- Enable Highlight.js -->
+    <script>hljs.highlightAll();</script>
+    <script>
+      hljs.registerLanguage('lean', function(hljs) {
+          return {
+              keywords: 'def theorem axiomatic structure lemma',
+              contains: [
+                  hljs.COMMENT('--', '$'),
+                  hljs.C_NUMBER_MODE,
+                  // Operators (custom definition)
+                {
+                    className: 'operator', // Define a class for styling
+                    begin: /[:=+\\-*/<>|&!~^{}]/ // Regex for operators
+                }]
+          };
+      });
+      hljs.highlightAll();
+      </script>
+"
+
+/-- The html styles for informal definitions. -/
+def informalDefStyle : String :=
+"
+<style>
+        .informal-def {
+            position: relative; /* Establish a relative positioning context for the button */
+            background-color: #f8d7da; /* Light red background */
+            border: 2px solid #dc3545; /* Solid darker red border */
+            margin: 10px; /* Space outside the block */
+            padding: 20px; /* Space inside the block */
+        }
+
+        .informal-def .button {
+            position: absolute; /* Position relative to the parent */
+            top: 5px; /* Distance from the top of the block */
+            right: 5px; /* Distance from the right of the block */
+            background-color: rgba(220, 53, 69, 0.4);
+            color: white; /* White text */
+            border: none; /* No border for the button */
+            padding: 5px 10px; /* Padding for the button */
+            text-decoration: none; /* Remove underline from the link */
+            border-radius: 5px; /* Rounded corners for the button */
+            font-size: 12px; /* Smaller font size */
+            cursor: pointer; /* Pointer cursor on hover */
+        }
+
+        .informal-def .button:hover {
+            background-color: #0056b3; /* Darker blue on hover */
+        }
+    body {
+            color: #000000; /* Change the default text color to dark gray */
+        }
+</style>
+"
+
+/-- The header to the html code. -/
+def headerHTML : String :=
+"---
+layout: default
+---
+<!DOCTYPE html>
+<html>
+<head>" ++ codeBlockHTML ++ informalDefStyle ++ "</head>
+</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 html code corresponding to a note about Lean and its use. -/
+def leanNote : String := "
+<br>
+<div style=\"border: 1px solid black; padding: 10px;\">
+  <p>Note: These are are not ordinary notes. They are created using an automated theorem
+  prover called Lean. Lean formally checks definitions, theorems and proofs for correctness.
+  These notes are part of a much larger project called HepLean, which aims to digitalize
+  high energy physics into Lean. Please consider contributing to this project.
+  <br>
+  Please provide feedback or suggestions for improvements by creating a GitHub issue
+  <a href=\"https://github.com/HEPLean/HepLean/issues\">here</a>.
+  </p>
+</div>
+"
+/-- 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 ++ leanNote ++ 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

@@ -5,6 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.Wick.Species
 import HepLean.Mathematics.SuperAlgebra.Basic
+import HepLean.Meta.Notes.Basic
 /-!
 
 # Operator algebra
@@ -23,9 +24,13 @@ We will formally define the operator ring, in terms of the fields present in the
 - Tong, https://www.damtp.cam.ac.uk/user/tong/qft/qft.pdf
 -/
 
+note "
+  <h1>Operator algebra</h1>
+  This is a test note."
+
 namespace Wick
 
-informal_definition WickAlgebra where
+informal_definition_note WickAlgebra where
   math :≈ "
     Modifications of this may be needed.
     A structure with the following data:
@@ -50,7 +55,7 @@ informal_definition WickAlgebra where
   ref :≈ "https://physics.stackexchange.com/questions/24157/"
   deps :≈ [``SuperAlgebra, ``SuperAlgebra.superCommuator]
 
-informal_definition WickMonomial where
+informal_definition_note WickMonomial where
   math :≈ "The type of elements of the Wick algebra which is a product of fields."
   deps :≈ [``WickAlgebra]
 
@@ -126,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]

HepLean/PerturbationTheory/Wick/Contract.lean

@@ -7,6 +7,7 @@ import HepLean.PerturbationTheory.Wick.String
 import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Data.Fintype.Sum
 import Mathlib.Logic.Equiv.Fin
+import HepLean.Meta.Notes.Basic
 /-!
 
 # Wick Contract
@@ -40,6 +41,7 @@ inductive WickContract : {ni : ℕ} → {i : Fin ni → S.𝓯} → {n : ℕ}
 namespace WickContract
 
 /-- The number of nodes of a Wick contraction. -/
+@[note_attr]
 def size {ni : ℕ} {i : Fin ni → S.𝓯} {n : ℕ} {c : Fin n → S.𝓯}
     {no : ℕ} {o : Fin no → S.𝓯} {str : WickString i c o final} {k : ℕ} {b1 b2 : Fin k → Fin n} :
     WickContract str b1 b2 → ℕ := fun

HepLean/PerturbationTheory/Wick/PositionSpace.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.FeynmanDiagrams.Basic
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 
 # Wick contraction in position space

HepLean/PerturbationTheory/Wick/Species.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Logic.Function.Basic
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 
 # Wick Species

HepLean/PerturbationTheory/Wick/String.lean

@@ -3,7 +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.Meta.Informal
+import HepLean.Meta.Informal.Basic
 import HepLean.PerturbationTheory.Wick.Species
 import Mathlib.Data.Fin.Tuple.Basic
 /-!

HepLean/StandardModel/Basic.lean

@@ -7,7 +7,7 @@ import Mathlib.Data.Complex.Exponential
 import Mathlib.Geometry.Manifold.Instances.Real
 import Mathlib.LinearAlgebra.Matrix.ToLin
 import HepLean.SpaceTime.Basic
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 # The Standard Model
 

HepLean/StandardModel/HiggsBoson/Basic.lean

@@ -11,7 +11,7 @@ import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
 import Mathlib.Geometry.Manifold.Instances.Real
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Geometry.Manifold.ContMDiff.Product
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 
 # The Higgs field

HepLean/StandardModel/HiggsBoson/Potential.lean

@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Algebra.QuadraticDiscriminant
 import HepLean.StandardModel.HiggsBoson.PointwiseInnerProd
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Basic
 /-!
 # The potential of the Higgs field
 

docs/sitemap.xml

@@ -21,4 +21,10 @@
       <priority>0.8</priority>
    </url>
 
+   <!-- Pertubation Theory Notes -->
+   <url>
+      <loc>https://heplean.github.io/HepLean/PertubationTheory</loc>
+      <changefreq>daily</changefreq>
+      <priority>0.8</priority>
+   </url>
 </urlset>

lakefile.toml

@@ -61,10 +61,24 @@ name = "stats"
 supportInterpreter = true
 srcDir = "scripts"
 
+[[lean_exe]]
+name = "notes"
+supportInterpreter = true
+srcDir = "scripts/MetaPrograms"
+
+[[lean_exe]]
+name = "lint_all"
+supportInterpreter = true
+srcDir = "scripts"
+
 [[lean_exe]]
 name = "free_simps"
 srcDir = "scripts/MetaPrograms"
 
+[[lean_exe]]
+name = "check_rfl"
+srcDir = "scripts/MetaPrograms"
+
 [[lean_exe]]
 name = "no_docs"
 srcDir = "scripts/MetaPrograms"

scripts/MetaPrograms/informal.lean

@@ -7,7 +7,7 @@ import Batteries.Lean.HashSet
 import Lean
 import Mathlib.Lean.Expr.Basic
 import Mathlib.Lean.CoreM
-import HepLean.Meta.Informal
+import HepLean.Meta.Informal.Post
 import ImportGraph.RequiredModules
 /-!
 
@@ -59,36 +59,19 @@ def depToWebString (d : Name) : MetaM String := do
     (mod.toString.replace "." "/") ++ ".lean"
   pure s!"    * [{d}]({webPath}#L{lineNo})"
 
-/-- Takes a `ConstantInfo` corresponding to a `InformalLemma` and returns
-  the corresponding `InformalLemma`. -/
-unsafe def constantInfoToInformalLemma (c : ConstantInfo) : MetaM InformalLemma := do
-  match c with
-  | ConstantInfo.defnInfo c =>
-      Lean.Meta.evalExpr' InformalLemma ``InformalLemma c.value
-  | _ => panic! "Passed constantInfoToInformalLemma a `ConstantInfo` that is not a `InformalLemma`"
-
-/-- Takes a `ConstantInfo` corresponding to a `InformalDefinition` and returns
-  the corresponding `InformalDefinition`. -/
-unsafe def constantInfoToInformalDefinition (c : ConstantInfo) : MetaM InformalDefinition := do
-  match c with
-  | ConstantInfo.defnInfo c =>
-      Lean.Meta.evalExpr' InformalDefinition ``InformalDefinition c.value
-  | _ => panic! "Passed constantInfoToInformalDefinition a
-    `ConstantInfo` that is not a `InformalDefinition`"
-
 unsafe def informalDependencies (c : ConstantInfo) : MetaM (Array Name) := do
   if Informal.isInformalLemma c then
-    let informal ← constantInfoToInformalLemma c
+    let informal ← Informal.constantInfoToInformalLemma c
     pure informal.dependencies.toArray
   else if Informal.isInformalDef c then
-    let informal ← constantInfoToInformalDefinition c
+    let informal ← Informal.constantInfoToInformalDefinition c
     pure informal.dependencies.toArray
   else
     pure #[]
 
 unsafe def informalLemmaToString (c : Import × ConstantInfo) : MetaM String := do
   let lineNo ← getLineNumber c.2.name
-  let informalLemma ← constantInfoToInformalLemma c.2
+  let informalLemma ← Informal.constantInfoToInformalLemma c.2
   let dep ← informalLemma.dependencies.mapM fun d => depToString d
   pure s!"
 Informal lemma: {informalLemma.name}
@@ -101,7 +84,7 @@ Informal lemma: {informalLemma.name}
 
 unsafe def informalLemmaToWebString (c : Import × ConstantInfo) : MetaM String := do
   let lineNo ← getLineNumber c.2.name
-  let informalLemma ← constantInfoToInformalLemma c.2
+  let informalLemma ← Informal.constantInfoToInformalLemma c.2
   let dep ← informalLemma.dependencies.mapM fun d => depToWebString d
   let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
     (c.1.module.toString.replace "." "/") ++ ".lean"
@@ -115,7 +98,7 @@ unsafe def informalLemmaToWebString (c : Import × ConstantInfo) : MetaM String
 
 unsafe def informalDefToString (c : Import × ConstantInfo) : MetaM String := do
   let lineNo ← getLineNumber c.2.name
-  let informalDef ← constantInfoToInformalDefinition c.2
+  let informalDef ← Informal.constantInfoToInformalDefinition c.2
   let dep ← informalDef.dependencies.mapM fun d => depToString d
   pure s!"
 Informal def: {informalDef.name}
@@ -127,7 +110,7 @@ Informal def: {informalDef.name}
 
 unsafe def informalDefToWebString (c : Import × ConstantInfo) : MetaM String := do
   let lineNo ← getLineNumber c.2.name
-  let informalDef ← constantInfoToInformalDefinition c.2
+  let informalDef ← Informal.constantInfoToInformalDefinition c.2
   let dep ← informalDef.dependencies.mapM fun d => depToWebString d
   let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
     (c.1.module.toString.replace "." "/") ++ ".lean"
@@ -168,7 +151,7 @@ There is an implicit invitation to the reader to contribute to the formalization
  background in Lean.
 
 "
-
+open Informal
 /-- Takes an import and outputs the list of `ConstantInfo` corresponding
   to an informal definition or lemma in that import, sorted by line number. -/
 def importToInformal (i : Import) : MetaM (Array (Import × ConstantInfo)) := do
@@ -223,7 +206,7 @@ unsafe def informalLemmaToNode (nameSpaces : Array Name) (c : Import × Constant
   let lineNo ← getLineNumber c.2.name
   let webPath := "https://github.com/HEPLean/HepLean/blob/master/"++
     (c.1.module.toString.replace "." "/") ++ ".lean"
-  let informalLemma ← (constantInfoToInformalLemma c.2)
+  let informalLemma ← (Informal.constantInfoToInformalLemma c.2)
   let prefixName := if nameSpaces.contains c.2.name then c.2.name else
     c.2.name.getPrefix
   let nodeStr := s!"\"{c.2.name}\"[label=\"{c.2.name}\", shape=ellipse, style=filled, fillcolor=lightgray,

scripts/MetaPrograms/no_docs.lean

@@ -37,6 +37,7 @@ def Imports.NoDocStringLemma (imp : Import) : MetaM UInt32 := do
   pure 0
 
 unsafe def main (args : List String) : IO UInt32 := do
+  initSearchPath (← findSysroot)
   let imports ← allImports
   let _ ← CoreM.withImportModules #[`HepLean] (imports.mapM Imports.NoDocStringDef).run'
   if "--lemmas" ∈ args then

scripts/MetaPrograms/notes.lean

@@ -0,0 +1,31 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Meta.Basic
+import HepLean.Meta.Notes.ToHTML
+/-!
+
+# Extracting notes from Lean files
+
+-/
+
+open Lean System Meta HepLean
+
+def pertubationTheory : NoteFile where
+  title := "Notes on Perturbation Theory"
+  abstract := "Notes on perturbation theory in quantum field theory."
+  authors := ["Joseph Tooby-Smith"]
+  files := [
+    `HepLean.PerturbationTheory.Wick.Algebra,
+    `HepLean.PerturbationTheory.Wick.Contract
+    ]
+
+unsafe def main (_ : List String) : IO UInt32 := do
+  initSearchPath (← findSysroot)
+  let htmlString ← CoreM.withImportModules #[`HepLean] (pertubationTheory.toHTMLString).run'
+  let htmlFile : System.FilePath := {toString := "./docs/PerturbationTheory.html"}
+  IO.FS.writeFile htmlFile htmlString
+  IO.println (s!"HTML file made.")
+  pure 0

scripts/lint_all.lean

@@ -0,0 +1,26 @@
+/-
+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.Post
+import ImportGraph.RequiredModules
+
+def main (_: List String) : IO UInt32 := do
+  println! "Building ... "
+  let build ← IO.Process.output {cmd := "lake", args := #["build"]}
+  println! build.stdout
+  println! "File imports ... "
+  let importCheck ← IO.Process.output {cmd := "lake", args := #["exe", "check_file_imports"]}
+  println! importCheck.stdout
+  println! "Style lint ... "
+  let styleLint ← IO.Process.output {cmd := "lake", args := #["exe", "hepLean_style_lint"]}
+  println! styleLint.stdout
+  println! "Doc check ..."
+  let docCheck ← IO.Process.output {cmd := "lake", args := #["exe", "no_docs"]}
+  println! docCheck.stdout
+  pure 0

scripts/stats.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.Meta.Basic
+import HepLean.Meta.Informal.Post
 /-!
 
 # HepLean Stats