refactor: Lint

HepLean.lean

@@ -60,6 +60,8 @@ import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.Basic
 import HepLean.FlavorPhysics.CKMMatrix.StandardParameterization.StandardParameters
 import HepLean.Mathematics.LinearMaps
 import HepLean.Mathematics.SO3.Basic
+import HepLean.Meta.AllFilePaths
+import HepLean.Meta.TransverseTactics
 import HepLean.SpaceTime.Basic
 import HepLean.SpaceTime.CliffordAlgebra
 import HepLean.SpaceTime.LorentzAlgebra.Basic

HepLean/Meta/AllFilePaths.lean

@@ -3,7 +3,6 @@ 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
 /-!
 
@@ -15,10 +14,9 @@ open Lean Elab System
 
 /-! TODO: Make this definition more functional in style. -/
 
-/-- Gets an array of all file paths in `HepLean`. -/
-partial def allFilePaths : IO (Array FilePath) := do
-  go (#[] : Array FilePath) `HepLean ("./HepLean" : FilePath)
-where go prev root path := do
+/-- The recursive function underlying `allFilePaths`. -/
+partial def allFilePaths.go (prev : Array FilePath)
+  (root : Name) (path : FilePath) : IO (Array FilePath) := do
   let mut r := prev
   for entry in ← path.readDir do
     if ← entry.path.isDir then
@@ -26,3 +24,7 @@ where go prev root path := do
     else
       r := r.push (root.toString.replace "." "/" ++ "/" ++ entry.fileName)
   pure r
+
+/-- Gets an array of all file paths in `HepLean`. -/
+partial def allFilePaths : IO (Array FilePath) := do
+  allFilePaths.go (#[] : Array FilePath) `HepLean ("./HepLean" : FilePath)

HepLean/Meta/TransverseTactics.lean

@@ -3,15 +3,13 @@ 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 HepLean.Meta.AllFilePaths
 /-!
 
 This file enables us to transverse tactics and test for conditions.
 
 ## References
-The content of this file is based on the following sources (released under the Apache 2.0 license):
+The content of this file is based on the following sources (released under the Apache 2.0 license).
 
 - https://github.com/dwrensha/tryAtEachStep/blob/main/tryAtEachStep.lean
 - https://github.com/lean-dojo/LeanDojo/blob/main/src/lean_dojo/data_extraction/ExtractData.lean
@@ -26,7 +24,8 @@ open Lean Elab System
 
 namespace transverseTactics
 
-
+/-- Takes in a file and returns the infostates of commands and the corresponding
+  enviroment before the command is processed. -/
 partial def processCommands : Frontend.FrontendM (List (Environment × InfoState)) := do
   /- Very roughly, `Frontend.FrontendM (List (Environment × InfoState))` is equivalent
     to `Frontend.Context → Frontend.state → List (Environment × InfoState)`.
@@ -34,14 +33,14 @@ partial def processCommands : Frontend.FrontendM (List (Environment × InfoState
     The `←get` here is returning the inputted value of `Frontend.state`,
     from which we get the enviroment.
     -/
-  let env := (←get).commandState.env
+  let env := (← get).commandState.env
   /- Processes a single command, adding it to `env`. This is done using
     `modify fun s => { s with commands := s.commands.push cmd }` as part of
     `Frontend.processCommand`. -/
   let done ← Frontend.processCommand
   /- Gets the updated `Frontend.state`. -/
   let st := ← get
-  /- Gets the infostate associated with the single command.  -/
+  /- Gets the infostate associated with the single command. -/
   let infoState := st.commandState.infoState
   set {st with commandState := {st.commandState with infoState := {}}}
   if done
@@ -49,20 +48,22 @@ partial def processCommands : Frontend.FrontendM (List (Environment × InfoState
   else
     /- For each command, we return the enviroment before the command is processed,
       and the `infoState` associated with that command. -/
-    return (env, infoState) :: (←processCommands)
+    return (env, infoState) :: (← processCommands)
 
+/-- Tests if a given `info` is `ofTacticInfo` and if so runs `visitTacticInfo`. -/
 def visitInfo (file : FilePath) (env : Environment)
     (visitTacticInfo : FilePath → ContextInfo → TacticInfo → MetaM Unit) (ci : ContextInfo)
     (info : Info) (acc : List (IO Unit)) : List (IO Unit) :=
   match info with
   | .ofTacticInfo ti =>
-     (ci.runMetaM default
-     (do setEnv env
-         try visitTacticInfo file ci ti
-         catch e =>
-            println! "caught: {←e.toMessageData.toString}")) :: acc
-  | _ =>   acc
+    (ci.runMetaM default
+    (do setEnv env
+        try visitTacticInfo file ci ti
+        catch e =>
+          println! "caught: {←e.toMessageData.toString}")) :: acc
+  | _ => acc
 
+/-- Applies `visitInfo` to each node of the info trees. -/
 def traverseForest (file : FilePath)
     (visitTacticInfo : FilePath → ContextInfo → TacticInfo → MetaM Unit)
     (steps : List (Environment × InfoState)) : List (IO Unit) :=
@@ -73,11 +74,14 @@ def traverseForest (file : FilePath)
 
 end transverseTactics
 
+/-! TODO: Find a way to free the enviroment `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)
   (visitTacticInfo : FilePath → ContextInfo → TacticInfo → MetaM Unit) : IO Unit := do
   searchPathRef.set compile_time_search_path%
-  /- This is equivalent to `(IO.FS.readFile file).bind (fun fileContent => do ...)`.  -/
+  /- This is equivalent to `(IO.FS.readFile file).bind (fun fileContent => do ...)`. -/
   let fileContent ← IO.FS.readFile file
   enableInitializersExecution
   /- Get `Parser.InputContext` from file. -/
@@ -87,7 +91,7 @@ unsafe def transverseTactics (file : FilePath)
   let (header, parserState, messages) ← Parser.parseHeader inputCtx
   /- Recall that the elborator turns a Lean syntax object into a Lean Expr object.
     In the below, we process the header, creating an enviroment with the relevent imports.
-    This can be thought of as creating an import only file.  -/
+    This can be thought of as creating an import only file. -/
   if messages.hasErrors then
     for msg in messages.toList do
       if msg.severity == .error then
@@ -110,7 +114,7 @@ unsafe def transverseTactics (file : FilePath)
   /- Runs the `processCommands` function on the context defined by `inputCtx`, and the
   state defined by `frontendState`. -/
   let (steps, _frontendState) ← (processCommands.run { inputCtx := inputCtx }).run
-     { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
+    { commandState := commandState, parserState := parserState, cmdPos := parserState.pos }
   /- Note that for us, each `infoState.trees` is actually of length 1. -/
   for t in traverseForest file visitTacticInfo steps do
     try t