From 5ab53ca3143ea0ae7044d8445174a0730be3dce3 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 26 Jun 2024 08:33:54 -0400
Subject: [PATCH 1/9] chore: Add lean version of check_file_import

---
 .github/workflows/build.yml                   | 16 ++--
 HepLean.lean                                  |  3 +-
 .../BeyondTheStandardModel/TwoHDM/Basic.lean  |  1 -
 lakefile.toml                                 |  4 +
 scripts/check_file_imports.lean               | 95 +++++++++++++++++++
 5 files changed, 109 insertions(+), 10 deletions(-)
 create mode 100644 scripts/check_file_imports.lean

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 4f36fcc..a1b67f7 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -24,12 +24,7 @@ jobs:
         run: |
           lean --version
           lake --version
-      
-      - name: check ls 
-        run: |
-          ls -a
-          
-      
+
       - name: build cache
         run: |
           lake exe cache get
@@ -41,7 +36,14 @@ jobs:
           linters: gcc
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
-      
+
+      - name: check file imports 
+        id : check_file_imports 
+        uses: liskin/gh-problem-matcher-wrap@v3
+        with : 
+          linters : gcc 
+          run : env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports
+
       - name: lint HepLean
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint
diff --git a/HepLean.lean b/HepLean.lean
index ee22052..a64b14b 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -73,7 +73,6 @@ import HepLean.SpaceTime.LorentzGroup.Proper
 import HepLean.SpaceTime.LorentzGroup.Rotations
 import HepLean.SpaceTime.Metric
 import HepLean.SpaceTime.SL2C.Basic
-import HepLean.StandardModel.Basic
 import HepLean.StandardModel.HiggsBoson.Basic
-import HepLean.StandardModel.HiggsBoson.TargetSpace
+import HepLean.StandardModel.Basic
 import HepLean.StandardModel.Representations
diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
index a9cdaa3..822e56e 100644
--- a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean
@@ -33,6 +33,5 @@ def potential (Φ1 Φ2 : higgsField)
   + (lam₆ * Φ1.normSq x * (Φ1.innerProd Φ2) x + conj lam₆ * Φ1.normSq x * (Φ2.innerProd Φ1) x).re
   + (lam₇ * Φ2.normSq x * (Φ1.innerProd Φ2) x + conj lam₇ * Φ2.normSq x * (Φ2.innerProd Φ1) x).re
 
-
 end
 end TwoHDM
diff --git a/lakefile.toml b/lakefile.toml
index 5444a11..7a85735 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -12,3 +12,7 @@ rev = "main"
 
 [[lean_lib]]
 name = "HepLean"
+
+[[lean_exe]]
+name = "check_file_imports"
+srcDir = "scripts"
diff --git a/scripts/check_file_imports.lean b/scripts/check_file_imports.lean
new file mode 100644
index 0000000..96d4783
--- /dev/null
+++ b/scripts/check_file_imports.lean
@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Lean
+import Batteries.Lean.HashSet
+import HepLean
+/-!
+
+# Check file imports
+
+This file checks that the imports in `HepLean.lean` are sorted and complete.
+
+It can be run from the terminal using
+`lake exe check_file_imports`.
+
+## Note on adaptation
+
+The functions
+
+`addModulesIn`, `expectedHepLeanImports`, and `checkMissingImports`
+
+are adapted from `batteries.scripts.check_imports.lean` authored by Joe Hendrix.
+
+
+-/
+open Lean System Meta
+
+
+/--  Recursively finds files in directory. -/
+partial def addModulesIn (recurse : Bool) (prev : Array Name) (root : Name := .anonymous)
+    (path : FilePath) : IO (Array Name) := do
+  let mut r := prev
+  for entry in ← path.readDir do
+    if ← entry.path.isDir then
+      if recurse then
+        r ← addModulesIn recurse r (root.mkStr entry.fileName) entry.path
+    else
+      let .some mod := FilePath.fileStem entry.fileName
+        | continue
+      r := r.push (root.mkStr mod)
+  pure r
+
+
+/-- Compute imports expected by `HepLean.lean` by looking at file structure. -/
+def expectedHepLeanImports : IO (Array Name) := do
+  let mut needed := #[]
+  for top in ← FilePath.readDir "HepLean" do
+      let nm := `HepLean
+      let rootname := FilePath.withExtension top.fileName ""
+      let root :=  nm.mkStr rootname.toString
+      if ← top.path.isDir then
+        needed ← addModulesIn (recurse := true) needed (root := root) top.path
+      else
+        needed :=
+        needed.push root
+  pure needed
+
+/-- Checks whether an array `imports` is sorted after `Init` is removed.  -/
+def arrayImportSorted (imports : Array Import) : IO Bool :=  do
+  let X := (imports.map (fun x => x.module.toString)).filter (fun x => x != "Init")
+  let mut warned := false
+  if ! X = X.qsort (· < ·) then
+    IO.print s!"Import file is not sorted. \n"
+    warned := true
+  pure warned
+
+/-- Checks every file in `reqImports` is imported into `modData`
+  return true if this is NOT the case. -/
+def checkMissingImports (modData : ModuleData) (reqImports : Array Name) :
+    IO Bool := do
+  let names : HashSet Name := HashSet.ofArray (modData.imports.map (·.module))
+  let mut warned := false
+  for req in reqImports do
+    if !names.contains req then
+      IO.print s!"File {req} is not imported. \n"
+      warned := true
+  pure warned
+
+def main (_ : List String) : IO UInt32 := do
+  initSearchPath (← findSysroot)
+  let mods : Name :=  `HepLean
+  let imp :  Import := {module := mods}
+  let mFile ← findOLean imp.module
+  unless (← mFile.pathExists) do
+        throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist"
+  let (hepLeanMod, _) ← readModuleData mFile
+  let eHepLeanImports ← expectedHepLeanImports
+  let sortedWarned ← arrayImportSorted hepLeanMod.imports
+  let warned ← checkMissingImports hepLeanMod eHepLeanImports
+  if (warned ∨ sortedWarned) then
+    throw <| IO.userError s!"The HepLean module is not sorted, or has missing imports."
+  IO.println s!"Import check complete."
+  pure 0

From 6775ae17f188c3150ac8e4e75c99cf9098428655 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 26 Jun 2024 08:42:12 -0400
Subject: [PATCH 2/9] attempt: fix workflow

---
 .github/workflows/build.yml     |  7 ++-----
 HepLean.lean                    |  3 ++-
 scripts/add-copilot.sh          | 18 ------------------
 scripts/check_file_imports.lean |  2 --
 scripts/copilot_lakefile.txt    | 23 -----------------------
 5 files changed, 4 insertions(+), 49 deletions(-)
 delete mode 100755 scripts/add-copilot.sh
 delete mode 100644 scripts/copilot_lakefile.txt

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index a1b67f7..cc876e8 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -38,11 +38,8 @@ jobs:
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
       - name: check file imports 
-        id : check_file_imports 
-        uses: liskin/gh-problem-matcher-wrap@v3
-        with : 
-          linters : gcc 
-          run : env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports
+        run: | 
+          env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports
 
       - name: lint HepLean
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
diff --git a/HepLean.lean b/HepLean.lean
index a64b14b..ee22052 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -73,6 +73,7 @@ import HepLean.SpaceTime.LorentzGroup.Proper
 import HepLean.SpaceTime.LorentzGroup.Rotations
 import HepLean.SpaceTime.Metric
 import HepLean.SpaceTime.SL2C.Basic
-import HepLean.StandardModel.HiggsBoson.Basic
 import HepLean.StandardModel.Basic
+import HepLean.StandardModel.HiggsBoson.Basic
+import HepLean.StandardModel.HiggsBoson.TargetSpace
 import HepLean.StandardModel.Representations
diff --git a/scripts/add-copilot.sh b/scripts/add-copilot.sh
deleted file mode 100755
index d0cb37e..0000000
--- a/scripts/add-copilot.sh
+++ /dev/null
@@ -1,18 +0,0 @@
-#!/usr/bin/env bash
-
-
-cp ./scripts/copilot_lakefile.txt lakefile.lean
-
-lake update LeanCopilot 
-
-lake exe LeanCopilot/download
-
-lake build 
-
-echo ".........................................................................."
-echo "Please do not push changes to the following files: 
-     - lakefile.lean
-     - .lake/lakefile.olean
-     - .lake/lakefile.olean.trace
-     - lake-manifest.json
-Please ensure that there are no 'import LeanCopilot' statements in the lean files."
diff --git a/scripts/check_file_imports.lean b/scripts/check_file_imports.lean
index 96d4783..bbc552c 100644
--- a/scripts/check_file_imports.lean
+++ b/scripts/check_file_imports.lean
@@ -3,8 +3,6 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import Lean
-import Batteries.Lean.HashSet
 import HepLean
 /-!
 
diff --git a/scripts/copilot_lakefile.txt b/scripts/copilot_lakefile.txt
deleted file mode 100644
index 1c73ce2..0000000
--- a/scripts/copilot_lakefile.txt
+++ /dev/null
@@ -1,23 +0,0 @@
-import Lake
-open Lake DSL
-
-package «hep_lean» {
-  -- add any package configuration options here
-}
-
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
-
-@[default_target]
-lean_lib «HepLean» {
-  -- add any library configuration options here
-  moreLinkArgs := #[
-    "-L./.lake/packages/LeanCopilot/.lake/build/lib",
-    "-lctranslate2"
-  ]
-}
-
-meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
-require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
-
-require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.2.1"
\ No newline at end of file

From 07e9c6586102820bd7799369e40cd1c4d7ddd440 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 26 Jun 2024 08:49:32 -0400
Subject: [PATCH 3/9] add bash -o pipefail

---
 .github/workflows/build.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index cc876e8..9a721b1 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -39,7 +39,7 @@ jobs:
 
       - name: check file imports 
         run: | 
-          env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports
+          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports"
 
       - name: lint HepLean
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}

From e3891341225f0579e4695e2f75ac24f8f4c016b3 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 26 Jun 2024 08:54:54 -0400
Subject: [PATCH 4/9] change imports

---
 scripts/check_file_imports.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/scripts/check_file_imports.lean b/scripts/check_file_imports.lean
index bbc552c..ec21e44 100644
--- a/scripts/check_file_imports.lean
+++ b/scripts/check_file_imports.lean
@@ -3,7 +3,8 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean
+import Batteries.Lean.HashSet
+import Lean
 /-!
 
 # Check file imports

From 23e8e092ccb4273f6d18695ddf2c51628f5e8892 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 26 Jun 2024 09:01:54 -0400
Subject: [PATCH 5/9] Update build.yml

---
 .github/workflows/build.yml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 9a721b1..d9d6af3 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -28,7 +28,10 @@ jobs:
       - name: build cache
         run: |
           lake exe cache get
- 
+      - name: check file imports 
+        run: | 
+          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports"
+  
       - name: build HepLean
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3
@@ -37,10 +40,7 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
-      - name: check file imports 
-        run: | 
-          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports"
-
+   
       - name: lint HepLean
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint

From 4529ccef7dc5ae8ed531d5bba0cd18f813c083d8 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 26 Jun 2024 09:03:51 -0400
Subject: [PATCH 6/9] test: Workflows

---
 .github/workflows/build.yml | 10 +++++-----
 HepLean.lean                |  3 +--
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index d9d6af3..9a721b1 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -28,10 +28,7 @@ jobs:
       - name: build cache
         run: |
           lake exe cache get
-      - name: check file imports 
-        run: | 
-          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports"
-  
+ 
       - name: build HepLean
         id: build
         uses: liskin/gh-problem-matcher-wrap@v3
@@ -40,7 +37,10 @@ jobs:
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
 
-   
+      - name: check file imports 
+        run: | 
+          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports"
+
       - name: lint HepLean
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint
diff --git a/HepLean.lean b/HepLean.lean
index ee22052..aa68e9e 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -73,7 +73,6 @@ import HepLean.SpaceTime.LorentzGroup.Proper
 import HepLean.SpaceTime.LorentzGroup.Rotations
 import HepLean.SpaceTime.Metric
 import HepLean.SpaceTime.SL2C.Basic
-import HepLean.StandardModel.Basic
-import HepLean.StandardModel.HiggsBoson.Basic
 import HepLean.StandardModel.HiggsBoson.TargetSpace
+import HepLean.StandardModel.HiggsBoson.Basic
 import HepLean.StandardModel.Representations

From 524fccc4849e3c753d03c303533066aea88fb889 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 26 Jun 2024 09:10:56 -0400
Subject: [PATCH 7/9] doc

---
 HepLean.lean       | 3 ++-
 doc/index.markdown | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/HepLean.lean b/HepLean.lean
index aa68e9e..ee22052 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -73,6 +73,7 @@ import HepLean.SpaceTime.LorentzGroup.Proper
 import HepLean.SpaceTime.LorentzGroup.Rotations
 import HepLean.SpaceTime.Metric
 import HepLean.SpaceTime.SL2C.Basic
-import HepLean.StandardModel.HiggsBoson.TargetSpace
+import HepLean.StandardModel.Basic
 import HepLean.StandardModel.HiggsBoson.Basic
+import HepLean.StandardModel.HiggsBoson.TargetSpace
 import HepLean.StandardModel.Representations
diff --git a/doc/index.markdown b/doc/index.markdown
index d3837a5..19032ef 100644
--- a/doc/index.markdown
+++ b/doc/index.markdown
@@ -58,5 +58,5 @@ Any area not appearing in the below table has zero coverage in HepLean.
 | [Feynman diagrams](https://heplean.github.io/HepLean/docs/HepLean/FeynmanDiagrams/Basic.html) | ✔️ | ✘  | ✘  |  |
 | [Lorentz Group](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html) | ✔️ | ✘  | ✘  | New lemmas etc.|
 | [2HDM](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html) | ✔️ | ✘  | ✘  | New lemmas etc. |
-
+| All other areas |  ✘ | ✘  | ✘  | New lemmas etc.|
 

From a8babe70f7470396136fda70c34e6a4b850d7e69 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 26 Jun 2024 09:11:32 -0400
Subject: [PATCH 8/9] chore: Remmove check_file_import.yml

---
 .github/workflows/check_file_import.yml | 23 -----------------------
 1 file changed, 23 deletions(-)
 delete mode 100644 .github/workflows/check_file_import.yml

diff --git a/.github/workflows/check_file_import.yml b/.github/workflows/check_file_import.yml
deleted file mode 100644
index 44b99f2..0000000
--- a/.github/workflows/check_file_import.yml
+++ /dev/null
@@ -1,23 +0,0 @@
-on: 
-  push: 
-  pull_request: 
-
-name: check file import
-
-jobs: 
-  check_file_import: 
-    name: check file import 
-    runs-on: ubuntu-latest
-    steps: 
-      - name: clean up
-        run: |
-         find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-  
-      - name: update HepLean.lean 
-        run: |
-          git ls-files 'HepLean/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > HepLean.lean
-
-      - name: check that all files are imported
-        run: git diff --exit-code
\ No newline at end of file

From dc8a42bac052171475d6ecdde6d6e3952def8985 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 26 Jun 2024 09:20:19 -0400
Subject: [PATCH 9/9] chore: Update workflow and toml

---
 .github/workflows/build.yml  |  4 +--
 lakefile.toml                | 14 ++++++++
 scripts/check-file-import.py | 63 ------------------------------------
 3 files changed, 16 insertions(+), 65 deletions(-)
 delete mode 100644 scripts/check-file-import.py

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 9a721b1..2f9fb44 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -41,7 +41,7 @@ jobs:
         run: | 
           bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports"
 
-      - name: lint HepLean
+      - name: runLinter on HepLean
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint
         uses: liskin/gh-problem-matcher-wrap@v3
@@ -50,7 +50,7 @@ jobs:
           run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter HepLean
 
   style_lint: 
-    name: Lint style
+    name: Python based style linter
     runs-on: ubuntu-latest
     steps:
       - name: cleanup
diff --git a/lakefile.toml b/lakefile.toml
index 7a85735..0de577a 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,5 +1,7 @@
 name = "hep_lean"
 defaultTargets = ["HepLean"]
+# -- Optional inclusion for LeanCopilot
+#moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]
 
 [[require]]
 name = "mathlib"
@@ -13,6 +15,18 @@ rev = "main"
 [[lean_lib]]
 name = "HepLean"
 
+# -- Optional inclusion of tryAtEachStep
+#[[require]]
+#name = "tryAtEachStep" 
+#git = "https://github.com/dwrensha/tryAtEachStep"
+#rev = "main"
+
+# -- Optional inclusion of LeanCopilot
+#[[require]]
+#name = "LeanCopilot"
+#git = "https://github.com/lean-dojo/LeanCopilot.git"
+#rev = "v1.2.2"
+
 [[lean_exe]]
 name = "check_file_imports"
 srcDir = "scripts"
diff --git a/scripts/check-file-import.py b/scripts/check-file-import.py
deleted file mode 100644
index effd447..0000000
--- a/scripts/check-file-import.py
+++ /dev/null
@@ -1,63 +0,0 @@
-#!/usr/bin/env python3
-"""
-This file locally checks if all files in the HepLean directory are imported correctly in 
-the HepLean.lean file.
-"""
-import os
-import re
-
-directory = "./HepLean/"
-files = []
-for root, _, filenames in os.walk(directory):
-    for filename in filenames:
-        if filename.endswith(".lean"):
-            files.append(os.path.join(root, filename))
-
-
-with open("./HepLean.lean", 'r') as f:
-    content = f.read()
-    
-imports = []
-for line in content.split('\n'):
-    match = re.match(r'import\s+(.*)', line)
-    if match:
-        imports.append(match.group(1))
-
-files_as_imports = [] 
-for file in files:
-    file_name = file 
-    file_name = file.replace("./", "").replace("/", ".").replace(".lean", "")
-    files_as_imports.append(file_name)
-
-files_as_imports.sort()
-a = [0,3,2]
-
-def file_check(imports, files_as_imports):
-    fail = False 
-    if imports != sorted(imports):
-        print("The imports list is not sorted.")
-        fail = True
-    to_add = [] 
-    for file in files_as_imports:
-        if file not in imports:
-            fail = True
-            to_add.append(file)
-    to_delete = []
-    for file in imports:
-        if file not in files_as_imports:
-            fail = True
-            to_delete.append(file)
-    if len(to_add) != 0 : 
-        print("The following files are not imported: ")
-        for f in to_add:
-            print(f)
-    if len(to_delete) != 0 : 
-        print("The following files should be deleted from HepLean.lean: ")
-        for f in to_delete:
-            print(f)
-    if not fail:
-        print("All files are imported correctly.")
-
-print ("----- Local import check of files: ")
-file_check(imports, files_as_imports)
-print ("----- End of local import check of files ")
\ No newline at end of file