From 61d3a0eda4ba67258c7012bebf0a9abdd6a101d7 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Mon, 31 Aug 2026 06:23:54 +0000
Subject: [PATCH] fix: include meta imports in DAG checks

---
 scripts/check_dag.py      |  8 ++++++--
 scripts/test_check_dag.py | 34 +++++++++++++++++++++++++++++++++-
 2 files changed, 39 insertions(+), 3 deletions(-)

diff --git a/scripts/check_dag.py b/scripts/check_dag.py
index 5d14c0a90..f3f2862a1 100644
--- a/scripts/check_dag.py
+++ b/scripts/check_dag.py
@@ -19,12 +19,16 @@
 )
 
 
-IMPORT_RE = re.compile(r"^\s*(?:public\s+|private\s+)?import\s+(.+?)\s*$")
+IMPORT_RE = re.compile(
+    r"^\s*(?:(?:public|private)\s+)?(?:meta\s+)?import\s+(.+?)\s*$"
+)
 LEAN_EXE_ROOT_RE = re.compile(r"^\s*root\s*:=\s*`([A-Za-z0-9_.]+)\s*$")
 LEAN_GLOB_MODULE_RE = re.compile(r"`([A-Z][A-Za-z0-9_.]+)")
 LEAN_LIB_RE = re.compile(r"^lean_lib\s+([A-Za-z0-9_]+)\b")
 LEAN_EXE_RE = re.compile(r"^lean_exe\s+([A-Za-z0-9_]+)\b")
-QUALIFIED_IMPORT_RE = re.compile(r"^\s*(?:public\s+|private\s+)?import\s+([A-Za-z0-9_.]+)\s*$")
+QUALIFIED_IMPORT_RE = re.compile(
+    r"^\s*(?:(?:public|private)\s+)?(?:meta\s+)?import\s+([A-Za-z0-9_.]+)\s*$"
+)
 IMPORT_ALL_RE = re.compile(
     r"^\s*(?:(?:public|private|meta)\s+)*import\s+all\s+([A-Za-z0-9_.]+)\s*$"
 )
diff --git a/scripts/test_check_dag.py b/scripts/test_check_dag.py
index 631c16407..195eb5046 100644
--- a/scripts/test_check_dag.py
+++ b/scripts/test_check_dag.py
@@ -8,11 +8,43 @@
 
 sys.path.insert(0, str(Path(__file__).resolve().parent))
 
-from check_dag import check_correspondence_only, check_sealed_import_all
+from check_dag import (
+    check_correspondence_only,
+    check_sealed_import_all,
+    import_roots,
+    parse_imports,
+)
 from check_phase4 import check_headline_reports
 from libgraph import LibraryInfo, load_libraries
 
 
+class MetaImportTest(unittest.TestCase):
+    def test_meta_imports_are_edges(self) -> None:
+        with tempfile.TemporaryDirectory() as directory:
+            path = Path(directory) / "HexOwner.lean"
+            path.write_text(
+                "public meta import HexDependency.Tactic\n"
+                "meta import HexDependency.Runtime\n",
+                encoding="utf-8",
+            )
+
+            self.assertEqual(
+                parse_imports(path),
+                ["HexDependency.Tactic", "HexDependency.Runtime"],
+            )
+            self.assertEqual(
+                import_roots("public meta import HexDependency.Tactic"),
+                ["HexDependency"],
+            )
+            self.assertEqual(
+                import_roots("meta import HexDependency.Runtime"),
+                ["HexDependency"],
+            )
+            self.assertEqual(
+                import_roots("meta public import HexDependency.Invalid"), []
+            )
+
+
 class SealedImportAllTest(unittest.TestCase):
     def test_ownerless_roots_are_checked(self) -> None:
         with tempfile.TemporaryDirectory() as directory: