fix(lean-ci,#17336): lost_gate soustrait la couverture reprise — deplacer le gate n'est pas le perdre

scripts/lean/check_axiom_gate_coverage.py

@@ -254,10 +254,31 @@ def deleted_dispatchers(ref: str) -> list[dict]:
             continue  # the parent did not have it (add/delete in one commit)
         out.append({"dispatcher": Path(path).name,
                     "deleted_by": sha[:10],
-                    "had_gate": calls_gate(last)})
+                    "had_gate": calls_gate(last),
+                    "gated_paths": gate_project_paths(last)})
     return out
 
 
+def classify_deleted(deleted: list[dict], gated_now: set[str]) -> dict:
+    """Partition deleted dispatchers into lost / relocated / never.
+
+    "Perdu" means lost COVERAGE, not lost FILE: a dispatcher that had the
+    gate and whose every former project-path is gated by a live caller
+    today moved its coverage rather than dropping it. Fail-closed on the
+    unreadable cases: a dispatcher that called the gate without passing a
+    project-path cannot prove its coverage moved, so it stays "lost".
+    """
+    lost, relocated, never = [], [], []
+    for d in deleted:
+        if not d["had_gate"]:
+            never.append(d)
+        elif d["gated_paths"] and set(d["gated_paths"]) <= gated_now:
+            relocated.append(d)
+        else:
+            lost.append(d)
+    return {"lost": lost, "relocated": relocated, "never": never}
+
+
 def measure(ref: str) -> dict:
     """Full coverage report at ``ref``."""
     covered = covered_lakes(ref)
@@ -269,8 +290,9 @@ def measure(ref: str) -> dict:
     manifest_paths = {lk.get("project-path") for lk in lakes}
     ungated = sorted(p for p in manifest_paths
                      if p and p not in set(gated_paths))
-    lost = [d for d in deleted if d["had_gate"]]
-    never = [d for d in deleted if not d["had_gate"]]
+    parts = classify_deleted(deleted, set(gated_paths))
+    lost, relocated = parts["lost"], parts["relocated"]
+    never = parts["never"]
 
     # What the file-wide scan would have credited *beyond* the job-scoped one:
     # the measure of the defect the scoping closes. Empty is the good news, not
@@ -290,12 +312,14 @@ def measure(ref: str) -> dict:
         "matrix_lakes_without_gate": ungated,
         "deleted_dispatchers": len(deleted),
         "lost_gate": sorted(lost, key=lambda d: d["dispatcher"]),
+        "gate_relocated": sorted(relocated, key=lambda d: d["dispatcher"]),
         "never_had_gate": sorted(never, key=lambda d: d["dispatcher"]),
         "not_an_acceptance_criterion": (
             "Cette couverture est une MESURE, pas un verdict de surete : un lake "
             "sans gate d'axiomes n'est pas illicite, il doit seulement etre CONNU "
-            "comme tel (#17097 critere 3). Aucun lake n'a perdu le gate en entrant "
-            "dans la matrice : le trou est preexistant."
+            "comme tel (#17097 critere 3). La perte ne se declare que si aucun "
+            "appel vivant ne reprend les project-paths de l'ancien dispatcher : "
+            "deplacer le gate n'est pas le perdre."
         ),
     }
 
@@ -321,6 +345,9 @@ def _print_human(r: dict) -> None:
     print(f"   AVAIENT le gate -> PERDU : {len(r['lost_gate'])}")
     for d in r["lost_gate"]:
         print(f"      PERDU  {d['dispatcher']:42} (supprime par {d['deleted_by']})")
+    print(f"   gate DEPLACE (couverture reprise ailleurs) : {len(r['gate_relocated'])}")
+    for d in r["gate_relocated"]:
+        print(f"      deplace {d['dispatcher']:42} (supprime par {d['deleted_by']})")
     print(f"   n'avaient pas le gate   : {len(r['never_had_gate'])}")
     for d in r["never_had_gate"]:
         print(f"      jamais {d['dispatcher']:42} (supprime par {d['deleted_by']})")

scripts/lean/tests/test_check_axiom_gate_coverage.py

@@ -17,6 +17,7 @@
 
 from check_axiom_gate_coverage import (  # noqa: E402
     calls_gate,
+    classify_deleted,
     deleted_dispatchers,
     filewide_project_paths,
     gate_project_paths,
@@ -233,10 +234,45 @@ def test_partition_is_a_partition(self):
         if not entries:
             pytest.skip(f"no deleted dispatchers visible at {_REF}")
         for e in entries:
-            assert set(e) == {"dispatcher", "deleted_by", "had_gate"}
+            assert set(e) == {"dispatcher", "deleted_by", "had_gate", "gated_paths"}
             assert isinstance(e["had_gate"], bool)
             assert e["dispatcher"].startswith("lean-")
             assert e["deleted_by"], "a deletion must carry the commit that made it"
+            assert isinstance(e["gated_paths"], list)
+
+
+class TestClassifyDeleted:
+    """Deplacer le gate n'est pas le perdre — et l'illisible reste PERDU."""
+
+    def _d(self, paths):
+        return {"dispatcher": "lean-x.yml", "deleted_by": "0123456789",
+                "had_gate": True, "gated_paths": paths}
+
+    def test_full_recoverage_is_relocation_not_loss(self):
+        d = self._d(["A/a_lean", "B/b_lean"])
+        r = classify_deleted([d], {"A/a_lean", "B/b_lean", "C/c_lean"})
+        assert r["lost"] == [] and r["never"] == []
+        assert [e["dispatcher"] for e in r["relocated"]] == ["lean-x.yml"]
+
+    def test_one_uncovered_path_keeps_it_lost(self):
+        d = self._d(["A/a_lean", "B/b_lean"])
+        r = classify_deleted([d], {"A/a_lean"})
+        assert r["relocated"] == [] and r["never"] == []
+        assert [e["dispatcher"] for e in r["lost"]] == ["lean-x.yml"]
+
+    def test_gate_without_project_path_fails_closed(self):
+        """A caller that passed no project-path cannot prove coverage moved."""
+        d = self._d([])
+        r = classify_deleted([d], {"A/a_lean"})
+        assert r["relocated"] == []
+        assert [e["dispatcher"] for e in r["lost"]] == ["lean-x.yml"]
+
+    def test_never_had_gate_stays_never(self):
+        d = {"dispatcher": "lean-y.yml", "deleted_by": "0123456789",
+             "had_gate": False, "gated_paths": []}
+        r = classify_deleted([d], set())
+        assert r["lost"] == [] and r["relocated"] == []
+        assert [e["dispatcher"] for e in r["never"]] == ["lean-y.yml"]
 
 
 class TestMeasurePartition:
@@ -262,11 +298,12 @@ def test_every_gate_caller_passes_a_project_path(self, report):
         for wf, paths in report["gate_callers"].items():
             assert paths, f"{wf} calls the gate but passes no project-path"
 
-    def test_lost_and_never_had_are_disjoint_and_exhaustive(self, report):
+    def test_lost_relocated_and_never_had_are_disjoint_and_exhaustive(self, report):
         lost = {d["dispatcher"] for d in report["lost_gate"]}
+        relocated = {d["dispatcher"] for d in report["gate_relocated"]}
         never = {d["dispatcher"] for d in report["never_had_gate"]}
-        assert not (lost & never)
-        assert len(lost) + len(never) == report["deleted_dispatchers"]
+        assert not (lost & relocated) and not (lost & never) and not (relocated & never)
+        assert len(lost) + len(relocated) + len(never) == report["deleted_dispatchers"]
 
     def test_verdict_is_not_dressed_as_an_acceptance_criterion(self, report):
         assert "not_an_acceptance_criterion" in report