Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 6 additions & 2 deletions scripts/check_dag.py
Original file line number Diff line number Diff line change
Expand Up @@ -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*$"
)
Expand Down
34 changes: 33 additions & 1 deletion scripts/test_check_dag.py
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
Loading