From eccede0a7d166abba5ce47e4f1b1e488e394a723 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Wed, 20 May 2026 13:36:18 +0900 Subject: [PATCH] Flag truncated files in partial-port audit --- python/lean_pool/partial_port_audit.py | 48 +++++++++++++++++++++++-- python/tests/test_partial_port_audit.py | 39 ++++++++++++++++++-- 2 files changed, 81 insertions(+), 6 deletions(-) diff --git a/python/lean_pool/partial_port_audit.py b/python/lean_pool/partial_port_audit.py index 4634e032b4..428fa8f0cb 100644 --- a/python/lean_pool/partial_port_audit.py +++ b/python/lean_pool/partial_port_audit.py @@ -70,15 +70,17 @@ class AuditFinding: file_ratio: float loc_ratio: float missing_files: tuple[str, ...] + truncated_files: tuple[str, ...] = () def format(self) -> str: """Format the finding as a concise human-readable paragraph.""" missing = ", ".join(self.missing_files) if self.missing_files else "none" + truncated = ", ".join(self.truncated_files) if self.truncated_files else "none" return ( f"{self.project}: imported {self.imported_files}/{self.upstream_files} " f"Lean files and {self.imported_loc}/{self.upstream_loc} non-comment " f"LOC from {self.upstream_repo}; largest unmatched upstream filenames: " - f"{missing}" + f"{missing}; matched files with large LOC gaps: {truncated}" ) @@ -160,9 +162,29 @@ def has_forbidden_upstream_construct(text: str) -> bool: ) +def normalize_name(name: str) -> str: + """Normalize a file or directory name for rough source/import matching.""" + return re.sub(r"[^a-z0-9]", "", name.lower()) + + def normalize_stem(path: str | Path) -> str: """Normalize a Lean filename stem for rough source/import matching.""" - return re.sub(r"[^a-z0-9]", "", Path(path).stem.lower()) + return normalize_name(Path(path).stem) + + +def normalize_relative_path(path: str | Path) -> str: + """Normalize a project-relative Lean path for same-file comparisons. + + Imported files live under ``LeanPool//...`` while upstream files + usually live under the upstream root module. Dropping those leading project + components lets ``LeanPool/Foo/Bar/Baz.lean`` match ``Foo/Bar/Baz.lean``. + """ + parts = Path(path).with_suffix("").parts + if len(parts) >= 3 and parts[0] == "LeanPool": + parts = parts[2:] + elif len(parts) >= 2 and parts[0] != "LeanPool": + parts = parts[1:] + return "/".join(normalize_name(part) for part in parts) def module_name(path: Path) -> str: @@ -307,8 +329,27 @@ def evaluate_stats( missing_files = tuple( file.path for file in missing_upstream_files if file.loc >= large_file_cutoff )[:MAX_MISSING_FILES] + imported_by_path: dict[str, list[LeanFile]] = {} + for file in imported.files: + imported_by_path.setdefault(normalize_relative_path(file.path), []).append(file) + truncated_files = [] + for file in sorted(upstream.files, key=lambda item: item.loc, reverse=True): + matching_imports = imported_by_path.get(normalize_relative_path(file.path), []) + if not matching_imports: + continue + imported_file = max(matching_imports, key=lambda item: item.loc) + if imported_file.loc / file.loc < cutoff: + truncated_files.append(f"{file.path} ({imported_file.loc}/{file.loc} LOC)") + if len(truncated_files) >= MAX_MISSING_FILES: + break + truncated_files_tuple = tuple(truncated_files) file_count_suspicious = upstream.file_count >= 3 and file_ratio < cutoff - if loc_ratio >= cutoff and not file_count_suspicious and not missing_files: + if ( + loc_ratio >= cutoff + and not file_count_suspicious + and not missing_files + and not truncated_files_tuple + ): return None if not missing_files: missing_files = tuple(file.path for file in missing_upstream_files)[ @@ -324,6 +365,7 @@ def evaluate_stats( file_ratio=file_ratio, loc_ratio=loc_ratio, missing_files=missing_files, + truncated_files=truncated_files_tuple, ) diff --git a/python/tests/test_partial_port_audit.py b/python/tests/test_partial_port_audit.py index 8b0819fecc..b209a0517b 100644 --- a/python/tests/test_partial_port_audit.py +++ b/python/tests/test_partial_port_audit.py @@ -10,6 +10,7 @@ has_forbidden_upstream_construct, imported_modules, module_name, + normalize_relative_path, normalize_stem, stats_from_worktree, ) @@ -60,9 +61,7 @@ def test_stats_from_worktree_skips_dependents_of_unimportable_files( (tmp_path / "Bad.lean").write_text( "theorem missing : True := by sorry\n", encoding="utf-8" ) - (tmp_path / "UsesBad.lean").write_text( - "import Bad\ndef y := 1\n", encoding="utf-8" - ) + (tmp_path / "UsesBad.lean").write_text("import Bad\ndef y := 1\n", encoding="utf-8") (tmp_path / "UsesUsesBad.lean").write_text( "import UsesBad\ndef z := 1\n", encoding="utf-8" ) @@ -95,6 +94,13 @@ def test_normalize_stem_matches_renamed_camel_case_file() -> None: ) +def test_normalize_relative_path_drops_project_prefix() -> None: + """Upstream and LeanPool project roots are ignored for same-file checks.""" + assert normalize_relative_path( + "Monlib/LinearAlgebra/QuantumSet/Basic.lean" + ) == normalize_relative_path("LeanPool/Monlib4/LinearAlgebra/QuantumSet/Basic.lean") + + def test_evaluate_stats_flags_large_loc_gap() -> None: """A small imported slice of a larger upstream project is suspicious.""" imported = LeanStats((LeanFile("LeanPool/Fineqs/Main.lean", 90, "main"),)) @@ -151,6 +157,33 @@ def test_evaluate_stats_lists_largest_missing_files_for_ratio_gap() -> None: ) +def test_evaluate_stats_flags_truncated_matched_file() -> None: + """A same-path file with too little LOC is still suspicious.""" + imported = LeanStats( + ( + LeanFile( + "LeanPool/Monlib4/LinearAlgebra/QuantumSet/Basic.lean", + 120, + "basic", + ), + LeanFile("LeanPool/Monlib4/Other.lean", 900, "other"), + ) + ) + upstream = LeanStats( + ( + LeanFile("Monlib/LinearAlgebra/QuantumSet/Basic.lean", 1000, "basic"), + LeanFile("Monlib/Other.lean", 900, "other"), + ) + ) + + finding = evaluate_stats("LeanPool.Monlib4", "owner/monlib4", imported, upstream) + + assert finding is not None + assert finding.truncated_files == ( + "Monlib/LinearAlgebra/QuantumSet/Basic.lean (120/1000 LOC)", + ) + + def test_evaluate_stats_accepts_close_import() -> None: """A near-complete import passes the tolerance check.""" imported = LeanStats((LeanFile("LeanPool/Foo/Main.lean", 920, "main"),))