Migrating alpha file import to lean + adding testing

.github/workflows/alphaBuild.yml

@@ -53,6 +53,10 @@ jobs:
       - name: Check no PhyslibAlpha in Physlib and QuantumInfo
         run: env LEAN_ABORT_ON_PANIC=1 lake exe noAlphaImports
 
+      - name: Check PhyslibAlpha imports
+        run: env LEAN_ABORT_ON_PANIC=1 lake exe alphaFileImports
+
+
   style_lint:
     name: Python based linters
     runs-on: ubuntu-latest
@@ -76,12 +80,6 @@ jobs:
         with:
           python-version: 3.8
 
-      - name: Check PhyslibAlpha imports
-        run: |
-          chmod u+x scripts/PhyslibAlpha/alphaFileImports.py
-          ./scripts/PhyslibAlpha/alphaFileImports.py
-
-
       - name: Python linters for PhyslibAlpha
         run: |
           chmod u+x scripts/PhyslibAlpha/alphaPythonLinters.sh

AGENTS.md

@@ -59,7 +59,7 @@ When a long proof cannot be split, make sure it contains comments.
 - If edited a `PhyslibAlpha` file, check the following:
   - `lake exe runPhyslibAlphaLinters`
   - `lake exe noAlphaImports`
-  - `./scripts/PhyslibAlpha/alphaFileImports.py`
+  - `lake exe alphaFileImports`
   - `./scripts/PhyslibAlpha/alphaPythonLinters.sh`
 
 ## PR scope

lakefile.toml

@@ -69,6 +69,16 @@ name = "noAlphaImports"
 srcDir = "scripts/PhyslibAlpha"
 supportInterpreter = true
 
+[[lean_exe]]
+name = "alphaFileImports"
+srcDir = "scripts/PhyslibAlpha"
+supportInterpreter = true
+
+[[lean_exe]]
+name = "testImportScripts"
+srcDir = "Meta/test"
+supportInterpreter = true
+
 [[lean_exe]]
 name = "free_simps"
 srcDir = "scripts/MetaPrograms"

scripts/PhyslibAlpha/alphaFileImports.lean

@@ -0,0 +1,49 @@
+import Lean
+import Physlib.Meta.AllFilePaths
+import Std.Data.HashSet
+
+
+/-!
+Copyright (c) 2026 Fergus Munro. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Fergus Munro
+-/
+
+open Lean
+open Std
+open System
+
+def extractModuleNameFromFilePath (path : FilePath) : String := 
+  ".".intercalate ((path.withExtension "").components.drop 1)
+
+def extractModuleNameFromImport (importString : String) : String := 
+  let rec findAfterImport : List String → String
+  | "import" :: x :: _ => x
+  | _ :: xs            => findAfterImport xs
+  | []                 => ""
+
+  findAfterImport ((importString.split Char.isWhitespace).toList.map toString)
+
+def checkAllFilesImported (directory : String) (mainFilePath : String) : (IO Bool) := do
+  let modules : HashSet String := HashSet.ofArray $ (← getFilePaths directory).map extractModuleNameFromFilePath 
+  let importedModules := HashSet.ofArray $ ((← IO.FS.lines mainFilePath).filter 
+    (·.contains "import")).map extractModuleNameFromImport 
+  let diff := modules \ importedModules
+  if diff.size > 0 
+    then do 
+      IO.println s!"Error: The following .lean files are not imported in {mainFilePath}:"
+      for module_name in diff do
+        IO.println s!"  - public import {module_name}"
+      return False 
+    else do
+      IO.println s!"✓ All {modules.size} .lean files in {directory} are imported in {mainFilePath}"
+      return True
+
+unsafe def main (args : List String) : IO Unit := do
+  let (dir, file) := match args with
+    | d :: f :: [] => (d, f)
+    | _ => ("./PhyslibAlpha", "./PhyslibAlpha.lean")
+  let success ← checkAllFilesImported dir file
+  if !success then
+    IO.Process.exit 1
+

scripts/PhyslibAlpha/noAlphaImports.lean

@@ -20,10 +20,9 @@ open System
   PhyslibAlpha files, and False otherwise, printing the offending files and 
   imports to the standard output.
   -/
-def areNoAlphaImports : IO Bool := do
-  let mut violations : Array (FilePath × Name) := #[]
+def areNoAlphaImports (modules : List String) : IO Bool := do
+  let mut violations  : Array (FilePath × Name) := #[]
 
-  let modules : Array String := #["./Physlib", "./QuantumInfo"]
   for module in modules do
 
     let filePaths ← getFilePaths module
@@ -48,8 +47,12 @@ def areNoAlphaImports : IO Bool := do
     IO.println "No violations found. All files passed the check."
     return True
 
-unsafe def main (_ : List String) : IO Unit := do
-  let success ← areNoAlphaImports 
+unsafe def main (args : List String) : IO Unit := do
+  let dirs := match args with
+    | [] => ["./Physlib", "./QuantumInfo"]
+    | _ => args
+
+  let success ← areNoAlphaImports dirs
 
   if !success then
     IO.Process.exit 1

scripts/lint_all.lean

@@ -24,6 +24,14 @@ def main (args : List String) : IO UInt32 := do
   let importCheck ← IO.Process.output {cmd := "lake", args := #["exe", "check_file_imports"]}
   println! importCheck.stdout
 
+  println! "\x1b[36m(3/7) Illegal Imports\x1b[0m"
+  let noAlphaImports ← IO.Process.output {cmd := "lake", args := #["exe", "noAlphaImports"]}
+  println! noAlphaImports.stdout
+
+  println! "\x1b[36m(3/7) Ensuring all PhyslibAlpha modules imported\x1b[0m"
+  let alphaFileImports ← IO.Process.output {cmd := "lake", args := #["exe", "alphaFileImports"]}
+  println! alphaFileImports.stdout
+
   println! "\x1b[36m(4/7) TODO tag duplicates \x1b[0m"
   let todoCheck ← IO.Process.output {cmd := "lake", args := #["exe", "check_dup_tags"]}
   println! todoCheck.stdout