refactor: some docs

lake-manifest.json

@@ -131,5 +131,5 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"}],
- "name": "HepLean",
+ "name": "PhysLean",
  "lakeDir": ".lake"}

scripts/MetaPrograms/TODO_to_yml.lean

@@ -3,8 +3,8 @@ 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.TODO.Basic
+import PhysLean.Meta.Basic
+import PhysLean.Meta.TODO.Basic
 import Mathlib.Lean.CoreM
 /-!
 
@@ -12,7 +12,7 @@ import Mathlib.Lean.CoreM
 
 -/
 
-open Lean System Meta HepLean
+open Lean System Meta PhysLean
 
 
 unsafe def getTodoInfo : MetaM (List todoInfo) := do
@@ -34,7 +34,7 @@ unsafe def todosToYAML : MetaM String := do
 
 unsafe def main (args : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)
-  let ymlString ← CoreM.withImportModules #[`HepLean] (todosToYAML).run'
+  let ymlString ← CoreM.withImportModules #[`PhysLean] (todosToYAML).run'
   println! ymlString
   let fileOut : System.FilePath := {toString := "./docs/_data/TODO.yml"}
   if "mkFile" ∈ args then

scripts/MetaPrograms/check_rfl.lean

@@ -5,8 +5,8 @@ Authors: Joseph Tooby-Smith
 -/
 import Batteries.Lean.HashSet
 import Lean
-import HepLean.Meta.AllFilePaths
-import HepLean.Meta.TransverseTactics
+import PhysLean.Meta.AllFilePaths
+import PhysLean.Meta.TransverseTactics
 /-!
 
 This file produces a list of places where `rfl` will complete the goal.

scripts/MetaPrograms/free_simps.lean

@@ -6,8 +6,8 @@ Authors: Joseph Tooby-Smith
 import Batteries.Lean.HashSet
 import Batteries.Data.String.Matcher
 import Lean
-import HepLean.Meta.AllFilePaths
-import HepLean.Meta.TransverseTactics
+import PhysLean.Meta.AllFilePaths
+import PhysLean.Meta.TransverseTactics
 /-!
 
 This file checks for non-terminating `simp` tactics which do not appear as `simp only`.

scripts/MetaPrograms/informal.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.Informal.Post
+import PhysLean.Meta.Informal.Post
 import Mathlib.Lean.CoreM
 /-!
 

scripts/MetaPrograms/notes.lean

@@ -3,18 +3,18 @@ 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.Remark.Properties
-import HepLean.Meta.Notes.ToHTML
+import PhysLean.Meta.Basic
+import PhysLean.Meta.Remark.Properties
+import PhysLean.Meta.Notes.ToHTML
 import Mathlib.Lean.CoreM
-import HepLean
+import PhysLean
 /-!
 
 # Extracting notes from Lean files
 
 -/
 
-open Lean System Meta HepLean
+open Lean System Meta PhysLean
 
 inductive NameStatus
   | complete : NameStatus
@@ -149,7 +149,7 @@ def perturbationTheory : Note where
     .name `FieldSpecification.wicks_theorem_context .incomplete,
     .p "In this note we walk through the important parts of the proof of the three versions of
       Wick's theorem for field operators containing carrying both fermionic and bosonic statitics,
-      as it appears in HepLean. Not every lemma or definition is covered here.
+      as it appears in PhysLean. Not every lemma or definition is covered here.
       The aim is to give just enough that the story can be understood.",
     .p "
      Before proceeding with the steps in the proof, we review some basic terminology
@@ -292,7 +292,7 @@ def perturbationTheory : Note where
 
 unsafe def main (_ : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)
-  let ymlString ← CoreM.withImportModules #[`HepLean] (perturbationTheory.toYML).run'
+  let ymlString ← CoreM.withImportModules #[`PhysLean] (perturbationTheory.toYML).run'
   let fileOut : System.FilePath := {toString := "./docs/_data/perturbationTheory.yml"}
   IO.println (s!"YML file made.")
   IO.FS.writeFile fileOut ymlString

scripts/MetaPrograms/redundent_imports.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 PhysLean.Meta.Basic
 import ImportGraph.Imports
 /-!
 
@@ -11,7 +11,7 @@ import ImportGraph.Imports
 
 -/
 
-open Lean System Meta HepLean
+open Lean System Meta PhysLean
 
 
 def Imports.RedundentImports (imp : Import) : MetaM UInt32 := do
@@ -25,5 +25,5 @@ def Imports.RedundentImports (imp : Import) : MetaM UInt32 := do
 unsafe def main (_ : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)
   let imports ← allImports
-  let _ ← CoreM.withImportModules #[`HepLean] (imports.mapM Imports.RedundentImports).run'
+  let _ ← CoreM.withImportModules #[`PhysLean] (imports.mapM Imports.RedundentImports).run'
   return 0

scripts/README.md

@@ -1,5 +1,5 @@
 
-# Scripts associated with HepLean
+# Scripts associated with PhysLean
 
 ## lint-style.py and lint-style.sh
 
@@ -9,7 +9,7 @@ These are to be slowly replaced with code written in Lean.
 
 ## hepLean_style_lint
 
-Checks the following in HepLean
+Checks the following in PhysLean
 - There are no double empty lines.
 - There are no non-initial double spaces.
 Passing this linter is currently not required to pass CI on github.
@@ -21,7 +21,7 @@ lake exe hepLean_style_lint
 
 ## check_file_imports.lean
 
-Checks all files are correctly imported into `HepLean.lean`.
+Checks all files are correctly imported into `PhysLean.lean`.
 
 Run using
 ```
@@ -39,7 +39,7 @@ lake exe type_former_lint
 
 ## stats.sh
 
-Outputs statistics for HepLean.
+Outputs statistics for PhysLean.
 
 Run using
 ```
@@ -61,7 +61,7 @@ Run on a specific file using
 ```
 lake exe openAI_doc_check <module_name>
 ```
-where `<module_name>` is e.g. `HepLean.SpaceTime.Basic`.
+where `<module_name>` is e.g. `PhysLean.SpaceTime.Basic`.
 
 Run on a random file using
 ```
@@ -70,7 +70,7 @@ lake exe openAI_doc_check random
 
 ## lint-all.sh
 
-Performs all linting checks on HepLean.
+Performs all linting checks on PhysLean.
 
 Run using
 ```
@@ -79,13 +79,13 @@ Run using
 
 ## Other useful commands
 
-- To build HepLean use
+- To build PhysLean use
 ```
 lake exe cache get
 lake build
 ```
 
-- To update HepLean's dependencies use
+- To update PhysLean's dependencies use
 ```
 lake update
 ```

scripts/lint-all.sh

@@ -5,14 +5,14 @@ echo "Running linter for Lean files"
 
 ./scripts/lint-style.sh
 
-echo "Building HepLean"
+echo "Building PhysLean"
 
-lake build HepLean
+lake build PhysLean
 
 echo "Run linter"
 
-lake exe runLinter HepLean
+lake exe runLinter PhysLean
 
 echo "Run shake"
 
-lake exe shake HepLean
+lake exe shake PhysLean

scripts/lint-style.sh

@@ -10,7 +10,7 @@ set -exo pipefail
 
 touch scripts/style-exceptions.txt
 
-git ls-files 'HepLean/*.lean' | xargs ./scripts/lint-style.py "$@"
+git ls-files 'PhysLean/*.lean' | xargs ./scripts/lint-style.py "$@"
 
 # 2. Global checks on the mathlib repository
 

scripts/mathlib_textLint_on_hepLean.lean

@@ -10,7 +10,7 @@ import Cli.Basic
 # Text based style linters from Mathlib
 
 This file is a copy of the `./scripts/lint_style.lean` executable from mathlib, adapted
-to run text-based style linters from mathlib on HepLean.
+to run text-based style linters from mathlib on PhysLean.
 
 That file is copyright Michael Rothgang, and is released under the Apache 2.0 license.
 It is authored by Michael Rothgang.
@@ -26,7 +26,7 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
     | (false, true) => OutputSetting.print ErrorFormat.github
     | (false, false) => OutputSetting.print ErrorFormat.humanReadable
   let mut allModules := #[]
-  for s in ["HepLean.lean"] do
+  for s in ["PhysLean.lean"] do
     allModules := allModules.append ((← IO.FS.lines s).filter (!·.containsSubstr "Batteries")
       |>.map (·.stripPrefix "import "))
   let numberErrorFiles ← lintModules allModules mode
@@ -36,7 +36,7 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do
 -- so far, no help options or so: perhaps that is fine?
 def heplean_lint_style : Cmd := `[Cli|
   lint_style VIA lintStyleCli; ["0.0.1"]
-  "Run text-based style linters on every Lean file in HepLean (adapted from mathlib's lint_style).
+  "Run text-based style linters on every Lean file in PhysLean (adapted from mathlib's lint_style).
   Print errors about any unexpected style errors to standard output."
 
   FLAGS:

scripts/openAI_doc_check.lean

@@ -12,7 +12,7 @@ import LLM.GPT.Json
 import LLM.GPT.API
 /-!
 
-# HepLean OpenAI doc check
+# PhysLean OpenAI doc check
 
 This file uses the openAI API to check the doc strings of definitions and theorems in a
 Lean 4 file.
@@ -53,7 +53,7 @@ def main (args : List String) : IO UInt32 := do
   | some x => do
     let mut imp : Import := Import.mk x.toName false
     if x == "random" then
-      let mods : Name :=  `HepLean
+      let mods : Name :=  `PhysLean
       let imps :  Import := {module := mods}
       let mFile ← findOLean imps.module
       unless (← mFile.pathExists) do

scripts/stats.lean

@@ -3,17 +3,17 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.Meta.Informal.Post
+import PhysLean.Meta.Informal.Post
 import Mathlib.Lean.CoreM
 /-!
 
-# HepLean Stats
+# PhysLean Stats
 
-This file concerns with statistics of HepLean.
+This file concerns with statistics of PhysLean.
 
 -/
 
-open Lean System Meta HepLean
+open Lean System Meta PhysLean
 
 def getStats : MetaM String := do
   let noDefsVal ← noDefs
@@ -49,7 +49,7 @@ layout: default
 <!DOCTYPE html>
 <html>
 <head>
-    <title>Stats for HepLean</title>
+    <title>Stats for PhysLean</title>
      <meta name=\"viewport\" content=\"width=device-width, initial-scale=1.0\">
      <style>
         /* Style the progress bar to be wider and take up more space */
@@ -79,7 +79,7 @@ layout: default
 </head>
 <body>"
   let body := s!"
-<h1>Stats for HepLean</h1>
+<h1>Stats for PhysLean</h1>
 <h3>Number of Files 📄: {noImportsVal}</h3>
 <h3>Number of lines 💻: {noLinesVal}</h3>
 <h3>Number of Definitions (incl. instances): {noDefsVal - noInformalLemmasVal}</h3>

scripts/type_former_lint.lean

@@ -11,7 +11,7 @@ import Lean
 
 This file checks that all definitions which form types start with a capital letter
 (or some non-latin character). This linter is not currently strictly enforced
-in HepLean.
+in PhysLean.
 
 
 -/
@@ -29,7 +29,7 @@ def IsUpperCamal (s : String) : Bool :=
 
 def main (_ : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)
-  let mods : Name :=  `HepLean
+  let mods : Name :=  `PhysLean
   let imp :  Import := {module := mods}
   let mFile ← findOLean imp.module
   unless (← mFile.pathExists) do