From ba51484b1f44f2b29a4ac8a361cbc89a1318cb05 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 23 Jan 2025 06:31:11 +0000
Subject: [PATCH] feat: Curated Notes

---
 HepLean/Meta/Remark/Basic.lean                | 68 +++++++++++++++
 HepLean/Meta/Remark/Properties.lean           | 40 +++++++++
 .../FieldSpecification/Basic.lean             |  9 ++
 .../FieldStatistics/Basic.lean                |  2 +-
 docs/CuratedNotes/PerturbationTheory.html     | 42 ++++++++++
 scripts/MetaPrograms/notes.lean               | 83 ++++++++++++++++---
 6 files changed, 233 insertions(+), 11 deletions(-)
 create mode 100644 HepLean/Meta/Remark/Basic.lean
 create mode 100644 HepLean/Meta/Remark/Properties.lean
 create mode 100644 docs/CuratedNotes/PerturbationTheory.html

diff --git a/HepLean/Meta/Remark/Basic.lean b/HepLean/Meta/Remark/Basic.lean
new file mode 100644
index 0000000..56cc835
--- /dev/null
+++ b/HepLean/Meta/Remark/Basic.lean
@@ -0,0 +1,68 @@
+/-
+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
+/-!
+
+## Underlying structure for remarks
+-/
+
+namespace HepLean
+open Lean System Meta
+
+/-- The information from a `remark ...` command. To be used in a note file-/
+structure RemarkInfo where
+  /-- The content of the remark. -/
+  content : String
+  /-- The file name where the remark came from. -/
+  fileName : Name
+  /-- The line from where the remark came from. -/
+  line : Nat
+  /-- The name of the remark. -/
+  name : Name
+  /-- The namespace of the remark. -/
+  nameSpace : Name
+
+/-- Environment extension to store `remark ...`. -/
+initialize remarkExtension : SimplePersistentEnvExtension RemarkInfo (Array RemarkInfo) ←
+  registerSimplePersistentEnvExtension {
+    name := `remarkExtension
+    addEntryFn := fun arr remarkInfoT => arr.push remarkInfoT
+    addImportedFn := fun es => es.foldl (· ++ ·) #[]
+  }
+
+/-- A remark is a string used for important information. -/
+syntax (name := remark_syntax) "remark " ident  ":=" str : command
+
+/-- Elaborator for the `note ...` command -/
+@[command_elab remark_syntax]
+def elabRemark : Lean.Elab.Command.CommandElab := fun stx =>
+  match stx with
+  | `(remark $n := $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 nameSpace := (← getCurrNamespace)
+
+      let noteInfo : RemarkInfo := {
+          content := str,
+          fileName := modName,
+          line := line,
+          name := n.getId,
+          nameSpace := nameSpace}
+      modifyEnv fun env => remarkExtension.addEntry env noteInfo
+    | none => throwError "Invalid syntax for `note` command"
+  | _ => throwError "Invalid syntax for `note` command"
+
+end HepLean
diff --git a/HepLean/Meta/Remark/Properties.lean b/HepLean/Meta/Remark/Properties.lean
new file mode 100644
index 0000000..c34f197
--- /dev/null
+++ b/HepLean/Meta/Remark/Properties.lean
@@ -0,0 +1,40 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.Meta.Remark.Basic
+/-!
+
+## Underlying structure for remarks
+-/
+
+namespace HepLean
+open Lean System Meta
+
+def Name.allRemarkInfo : MetaM (List RemarkInfo) := do
+  let env ← getEnv
+  let allRemarks := (remarkExtension.getState env)
+  pure allRemarks.toList
+
+def RemarkInfo.toFullName (r : RemarkInfo) :  Name :=
+  if r.nameSpace != .anonymous then
+    (r.nameSpace.toString ++ "." ++ r.name.toString).toName
+  else
+    r.name
+
+def RemarkInfo.IsRemark (n : Name) : MetaM Bool := do
+  let allRemarks ← Name.allRemarkInfo
+  let r := allRemarks.find? (fun r => r.toFullName = n)
+  match r with
+  | some _ => pure true
+  | none => pure false
+
+def RemarkInfo.getRemarkInfo (n : Name) : MetaM RemarkInfo := do
+  let allRemarks ← Name.allRemarkInfo
+  let r := allRemarks.find? (fun r => r.toFullName = n)
+  match r with
+  | some r => pure r
+  | none => throwError s!"No remark named {n}"
+
+end HepLean
diff --git a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
index 93494c7..aff7605 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
@@ -7,6 +7,7 @@ import HepLean.Lorentz.RealVector.Basic
 import HepLean.PerturbationTheory.FieldStatistics.ExchangeSign
 import HepLean.SpaceTime.Basic
 import HepLean.PerturbationTheory.FieldStatistics.OfFinset
+import HepLean.Meta.Remark.Basic
 /-!
 
 # Field specification
@@ -24,6 +25,14 @@ These states carry the same field statistic as the field they are derived from.
 
 -/
 
+remark fieldSpecification_intro := "The raw ingredients of a field theory are:
+  - The specification of the fields.
+  - Whether each field is a boson or a fermion.
+  - Vertices present.
+  - Coefficents of each vertex.
+
+  We call the first two of these ingredients the `FieldSpecification` of the theory. "
+
 /-- A field specification is a type of fields plus a specification of the
   statistics (fermionic or bosonic) of each field. -/
 structure FieldSpecification where
diff --git a/HepLean/PerturbationTheory/FieldStatistics/Basic.lean b/HepLean/PerturbationTheory/FieldStatistics/Basic.lean
index 5526935..ae658a4 100644
--- a/HepLean/PerturbationTheory/FieldStatistics/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldStatistics/Basic.lean
@@ -27,7 +27,7 @@ namespace FieldStatistic
 
 variable {𝓕 : Type}
 
-/-- Field statistics form a commuative group equivalent to `ℤ₂`. -/
+/-- Field statistics form a commuative group isomorphic to `ℤ₂`. -/
 @[simp]
 instance : CommGroup FieldStatistic where
   one := bosonic
diff --git a/docs/CuratedNotes/PerturbationTheory.html b/docs/CuratedNotes/PerturbationTheory.html
new file mode 100644
index 0000000..8d0bc0d
--- /dev/null
+++ b/docs/CuratedNotes/PerturbationTheory.html
@@ -0,0 +1,42 @@
+---
+layout: default
+---
+<center><h1 style="font-size: 50px;">{{ site.data.perturbationTheory.title }}</h1></center>
+<br>
+<div style="border: 1px solid black; padding: 10px;">
+  <p>Note:
+  These notes are created using an interactive theorem
+  prover called <a href="https://lean-lang.org">Lean</a>.
+  Lean formally checks definitions, theorems and proofs for correctness.
+  These notes are part of a much larger project called
+  <a href="https://github.com/HEPLean/HepLean">HepLean</a>, which aims to digitalize
+  high energy physics into Lean. Please consider contributing to this project.
+  <br><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>
+<br>
+{% for entry in site.data.perturbationTheory.parts %}
+  {% if entry.type == "h1" %}
+    <h1>{{ entry.content }}</h1>
+  {% endif %}
+  {% if entry.type == "h2" %}
+    <h2>{{ entry.content }}</h2>
+  {% endif %}
+  {% if entry.type == "p" %}
+    <p>{{ entry.content }}</p>
+  {% endif %}
+  {% if entry.type == "name" %}
+    <div class="code-block-container">
+      <pre><code>
+{{ entry.content }}
+      </code></pre>
+    </div>
+  {% endif %}
+  {% if entry.type == "remark" %}
+    <p><i>Remark:</i>
+    {{ entry.content|markdownify }}
+    </p>
+  {% endif %}
+{% endfor %}
diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean
index 32fbc42..abbd4ea 100644
--- a/scripts/MetaPrograms/notes.lean
+++ b/scripts/MetaPrograms/notes.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Meta.Basic
+import HepLean.Meta.Remark.Properties
 import HepLean.Meta.Notes.ToHTML
 /-!
 
@@ -13,18 +14,80 @@ import HepLean.Meta.Notes.ToHTML
 
 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 := [
+inductive NotePart
+  | h1 : String → NotePart
+  | h2 : String → NotePart
+  | p : String → NotePart
+  | name : Name → NotePart
 
-    ]
+def formalContent (name : Name) : MetaM String := do
+  let line ← Name.lineNumber name
+  let decl ← Name.getDeclString name
+  let fileName ← Name.fileName name
+  let webAddress : String ← Name.toGitHubLink fileName line
+  pure decl
+
+
+def NotePart.toYMLM : NotePart →  MetaM String
+  | NotePart.h1 s => pure s!"
+  - type: h1
+    content: \"{s}\""
+  | NotePart.h2 s => pure s!"
+  - type: h2
+    content: \"{s}\""
+  | NotePart.p s => pure s!"
+  - type: p
+    content: \"{s}\""
+  | NotePart.name n => do
+  match (← RemarkInfo.IsRemark n) with
+  | true =>
+    let remarkInfo ← RemarkInfo.getRemarkInfo n
+    let content := remarkInfo.content
+    let contentIndent := content.replace "\n" "\n      "
+    let shortName := remarkInfo.name.toString
+    return s!"
+  - type: remark
+    name: \"{shortName}\"
+    content: |
+      {contentIndent}"
+  | false =>
+  let content ← formalContent n
+  let contentIndent := content.replace "\n" "\n      "
+  return s!"
+  - type: name
+    content: |
+      {contentIndent}"
+
+structure Note where
+  title : String
+  /-- The curators of the note are the people who put the note together.
+    This may not conicide with the original authors of the material. -/
+  curators : List String
+  parts : List NotePart
+
+def Note.toYML : Note → MetaM String
+  | ⟨title, curators, parts⟩ => return s!"
+title: \"{title}\"
+curators: {curators}
+parts:
+  {String.intercalate "\n" (← parts.mapM NotePart.toYMLM)}"
+
+def perturbationTheory : Note where
+  title := "Proof of Wick's theorem"
+  curators := ["Joseph Tooby-Smith"]
+  parts := [
+    .h1 "Field statistics",
+    .p "A quantum field can either be a bosonic or fermionic. This information is
+      contained in the inductive type `FieldStatistic`. This is defined as follows:",
+    .name `FieldStatistic,
+    .h1 "Field specifications",
+    .name `fieldSpecification_intro,
+    .name `FieldSpecification]
 
 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.")
+  let ymlString ← CoreM.withImportModules #[`HepLean] (perturbationTheory.toYML).run'
+  let fileOut : System.FilePath := {toString := "./docs/_data/perturbationTheory.yml"}
+  IO.println (s!"YML file made.")
+  IO.FS.writeFile fileOut ymlString
   pure 0