Workflow: check file imports

HEPLean · Apr 17, 2024 · 20eb535 · 20eb535
1 parent 4e9d26a
commit 20eb535
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 7 deletions.
diff --git a/.github/workflows/check_file_import.yml b/.github/workflows/check_file_import.yml
@@ -0,0 +1,22 @@
+on: 
+  push: 
+
+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
diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean
@@ -4,13 +4,6 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.AnomalyCancellation.LinearMaps
-import Mathlib.Tactic.Polyrith
-import Mathlib.Tactic.Linarith
-import Mathlib.Tactic.FieldSimp
-import Mathlib.NumberTheory.FLT.Basic
-import Mathlib.Algebra.QuadraticDiscriminant
-import Mathlib.Algebra.Module.Basic
-import Mathlib.Algebra.Module.LinearMap.Basic
 /-!
 # Basic set up for anomaly cancellation conditions
 

diff --git a/HepLean/AnomalyCancellation/LinearMaps.lean b/HepLean/AnomalyCancellation/LinearMaps.lean
@@ -14,6 +14,7 @@ quadratic and cubic equations.
 ## TODO
 
 Use definitions in `Mathlib4` for definitions where possible.
+In particular a HomogeneousQuadratic should be a map `V →ₗ[ℚ] V →ₗ[ℚ] ℚ`  etc.
 
 -/
-Original file line number
+Diff line change
@@ Expand Up / @@ -14,6 +14,7 @@ quadratic and cubic equations. @@
     ## TODO
     Use definitions in `Mathlib4` for definitions where possible.
+    In particular a HomogeneousQuadratic should be a map `V →ₗ[ℚ] V →ₗ[ℚ] ℚ`  etc.
     -/
@@ Expand Down @@