CI to check Mathlib imports: negative test

Author: javierlcontreras

.github/workflows/push_master.yml

@@ -26,6 +26,7 @@ jobs:
         run: |
           ! (find LeanCamCombi -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Mathlib$')
 
+
   build_project:
     runs-on: ubuntu-latest
     name: Build project
@@ -36,6 +37,10 @@ jobs:
       - name: Copy README.md to website/index.md
         run: cp README.md website/index.md
 
+      - name: Check LeanCamCombi.Mathlib only imports from Mathlib or LeanCamCombi.Mathlib
+        run: |
+          python3 scripts/check_mathlib_imports.py
+
       - name: Upstreaming dashboard
         run: |
           mkdir -p website/_includes

LeanCamCombi/Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean

@@ -1,6 +1,7 @@
 import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Combinatorics.Additive.ApproximateSubgroup
 import Mathlib.Tactic.Bound
+import LeanCamCombi.ExtrProbCombi.BernoulliSeq
 
 open scoped Finset Pointwise
 

scripts/check_mathlib_imports.py

@@ -0,0 +1,25 @@
+import os
+
+def list_files_by_type_recursive(folder_path, file_extension):
+    """Recursively lists all files in a folder and subfolders with the specified file extension."""
+    matching_files = []
+    for root, _, files in os.walk(folder_path):
+        matching_files.extend(os.path.join(root, f) for f in files if f.endswith(file_extension))
+    return matching_files
+
+folder = "LeanCamCombi/Mathlib"
+extension = ".lean"
+files = list_files_by_type_recursive(folder, extension)
+
+for file in files:
+    code = None
+    with open(file, "r") as reader:
+        code = reader.read()
+    lines = code.split("\n")
+    header = [line for line in lines if line.lstrip().startswith("import")]
+
+    for imp in header:
+        imp_file = imp.lstrip()[len("import"):].strip()
+        if (not imp_file.startswith("Mathlib.")) and \
+            (not imp_file.startswith("LeanCamCombi.Mathlib")):
+            raise IOError("A file in LeanCamCombi.Mathlib imports a file not in Mathlib or LeanCamCombi.Mathlib")