Fix(#13962): check_mathlib_cache -- une jonction pendante n'est plus classee absent/reel

scripts/lean/check_mathlib_cache.py

@@ -10,8 +10,13 @@
   `find` ne traverse pas les junctions.
 * `os.path.islink(chemin)` renvoie **False** : rien ne signale que le repertoire
   est un lien, donc le « 0 » passe pour une mesure de repertoire vide.
+* `os.path.exists(chemin)` **suit** le lien : il rend **False** des que la CIBLE a
+  disparu. Teste avant la detection du lien, il classe une jonction **pendante**
+  en « pas de checkout » — et l'affichage la rend `reel`, c'est-a-dire l'exact
+  contraire de la verite. Mesure po-2025 (2026-10-08) : 14 jonctions pendantes
+  lues `absent`/`reel`. Detail : `docs/lean/junctions-scan-po-2025.md`.
 
-Ensemble, les deux fabriquent un verdict « cache purge, cold-build 30 min requis »
+Ensemble, les trois fabriquent un verdict « cache purge, cold-build 30 min requis »
 a partir d'un cache parfaitement sain. Cette confusion a immobilise une lane Lean
 pendant 5 cycles (DM `msg-20260729T055956-n3f4ap`).
 
@@ -85,15 +90,31 @@ def analyse_lake(lake: Path, cache: dict[str, int]) -> dict:
     mathlib = lake / ".lake" / "packages" / "mathlib"
     result: dict = {"lake": str(lake), "declares_mathlib": declares_mathlib(lake)}
 
+    # La detection du lien precede le test d'existence : `exists()` SUIT le lien et
+    # rend False des que la CIBLE a disparu. Teste en premier, il classait une
+    # jonction pendante en `absent`, et l'affichage ligne ~158 la rendait `reel` --
+    # l'inverse de la verite (14 jonctions po-2025, cf junctions-scan-po-2025.md).
+    # `islink()` est False sur une junction Windows : c'est la divergence de chemin
+    # qui la revele, pas l'API dediee (`is_junction()` n'existe qu'a partir de 3.12).
+    real = Path(os.path.realpath(mathlib))
+    result["junction"] = str(real) != str(mathlib.resolve(strict=False)) or real != mathlib
+    if result["junction"]:
+        # Cible du lien, meme morte : elle sert au diagnostic. Cle distincte de
+        # `realpath`, qui designe un cache PHYSIQUE et alimente le dedoublonnage --
+        # une cible disparue n'est pas un cache physique et ne doit pas y entrer.
+        result["junction_target"] = str(real)
+
     if not mathlib.exists():
-        result["status"] = "absent" if result["declares_mathlib"] else "no_mathlib_dep"
+        if result["junction"]:
+            # Le lien existe, sa cible a disparu : etat distinct de « aucun checkout »
+            # et strictement pire que `cold` -- le chemin se presente comme un paquet
+            # installe, mais rien n'est atteignable a travers.
+            result["status"] = "dangling"
+        else:
+            result["status"] = "absent" if result["declares_mathlib"] else "no_mathlib_dep"
         result["oleans"] = 0
         return result
 
-    real = Path(os.path.realpath(mathlib))
-    # `islink()` est False sur une junction Windows : c'est la divergence de
-    # chemin qui la revele, pas l'API dediee.
-    result["junction"] = str(real) != str(mathlib.resolve(strict=False)) or real != mathlib
     result["realpath"] = str(real)
 
     key = str(real)
@@ -162,13 +183,22 @@ def main(argv: list[str] | None = None) -> int:
     partial = [r for r in results if r["status"] == "partial"]
     ok = [r for r in results if r["status"] == "ok"]
     absent = [r for r in results if r["status"] == "absent"]
+    dangling = [r for r in results if r["status"] == "dangling"]
 
     print()
     print(f"Lakes: {len(lakes)} | mathlib ok: {len(ok)} | froid: {len(cold)} | "
           f"partiel: {len(partial)} | non installe: {len(absent)} | "
+          f"jonctions pendantes: {len(dangling)} | "
           f"caches physiques distincts: {len(by_real)}")
 
-    if cold or partial:
+    if dangling:
+        print("\nJonctions PENDANTES -- le lien existe, sa cible a disparu :")
+        print(f"  {len(dangling)} lake(s) portent un chemin `.lake/packages/mathlib`")
+        print("  qui se presente comme un paquet installe, mais rien n'est atteignable")
+        print("  a travers. Distinct de `froid` (cible presente, store vide) et de")
+        print("  `non installe` (aucun lien).")
+
+    if cold or partial or dangling:
         print("\nAvant de conclure 'cache purge', relancer un `lake build` reel :")
         print("  un comptage a 0 via `find` ou `islink` ne prouve rien sur une junction.")
 
@@ -178,7 +208,13 @@ def main(argv: list[str] | None = None) -> int:
         Path(args.json_out).write_text(json.dumps(payload, indent=2), encoding="utf-8")
         print(f"\nJSON: {args.json_out}")
 
-    return 1 if (args.strict and (cold or partial)) else 0
+    # `dangling` est compte par `--strict` alors que `absent` ne l'est pas : un lake
+    # sans checkout est l'etat NORMAL d'un lac jamais construit localement (lake le
+    # recuperera), tandis qu'une jonction pendante se presente comme un paquet
+    # installe et n'atteint rien -- un `lake build` peut tenter de repeupler le
+    # store partage a travers elle (incident fondateur #13962, docstring de
+    # setup_shared_mathlib.ps1).
+    return 1 if (args.strict and (cold or partial or dangling)) else 0
 
 
 if __name__ == "__main__":

scripts/lean/tests/test_check_mathlib_cache.py

@@ -11,6 +11,9 @@
 junctions, no network). Zero source churn.
 """
 
+import os
+import shutil
+import subprocess
 import sys
 from pathlib import Path
 
@@ -43,6 +46,37 @@ def _make_lake(root: Path, name: str, lakefile: str = "lakefile.lean",
     return lake
 
 
+def _link_dir(link: Path, target: Path) -> None:
+    """Cree un lien de repertoire vers ``target``.
+
+    Sous Windows on passe par une **junction** NTFS (`mklink /J`), qui n'exige pas
+    d'elevation la ou `symlink_to` en exige une ; ailleurs, un symlink ordinaire.
+    Le test se skip si aucun des deux n'est disponible.
+    """
+    link.parent.mkdir(parents=True, exist_ok=True)
+    if os.name == "nt":
+        proc = subprocess.run(["cmd", "/c", "mklink", "/J", str(link), str(target)],
+                              capture_output=True, text=True)
+        if proc.returncode != 0:
+            pytest.skip(f"mklink /J indisponible : {proc.stderr.strip() or proc.stdout.strip()}")
+        return
+    try:
+        link.symlink_to(target, target_is_directory=True)
+    except (OSError, NotImplementedError):
+        pytest.skip("symlinks not supported on this platform")
+
+
+def _make_lake_with_mathlib_link(root: Path, name: str, store: Path,
+                                 populate: bool = True) -> Path:
+    """Lac declarant mathlib, dont `.lake/packages/mathlib` est un LIEN vers ``store``."""
+    lake = _make_lake(root, name, body="require mathlib from git")
+    store.mkdir(parents=True, exist_ok=True)
+    if populate:
+        _write(store / "Mathlib" / "Init.olean")
+    _link_dir(lake / ".lake" / "packages" / "mathlib", store)
+    return lake
+
+
 # ---------------------------------------------------------------------------
 # constants
 # ---------------------------------------------------------------------------
@@ -209,12 +243,13 @@ def test_cache_dedups_by_realpath(self, tmp_path):
         for name in ("L1", "L2"):
             lake = _make_lake(tmp_path, name, body='require mathlib from git')
             mlib = lake / ".lake" / "packages" / "mathlib"
-            mlib.parent.mkdir(parents=True, exist_ok=True)
-            # symlink so realpath converges on the shared store
-            try:
-                mlib.symlink_to(shared, target_is_directory=True)
-            except (OSError, NotImplementedError):
-                pytest.skip("symlinks not supported on this platform")
+            # Lien vers le store partage, pour que le realpath converge dessus.
+            # `_link_dir` (mklink /J sous Windows) la ou `symlink_to` exige une
+            # elevation : ce test se SKIPPAIT donc en permanence sur Windows, et
+            # le dedoublonnage par realpath -- precisement la propriete qu'il
+            # epingle -- n'etait verifie nulle part sur la machine qui porte les
+            # 18 junctions.
+            _link_dir(mlib, shared)
             r = analyse_lake(lake, cache)
             assert r["oleans"] == 1
         # cache holds exactly one entry for the shared realpath
@@ -226,6 +261,73 @@ def test_result_carries_lake_path(self, tmp_path):
         assert str(lake) == r["lake"]
 
 
+# ---------------------------------------------------------------------------
+# analyse_lake -- jonctions
+#
+# Trois etats distincts, mesures sur po-2025 le 2026-10-08 (18 jonctions,
+# aucune utilisable) et documentes dans docs/lean/junctions-scan-po-2025.md :
+#   - `ok`      : lien vers un store peuple
+#   - `cold`    : lien vers un store VIDE (cible presente)
+#   - `dangling`: lien dont la CIBLE A DISPARU -- etat nouveau, il etait rendu
+#                 `absent` + `reel` avant ce fix
+# ---------------------------------------------------------------------------
+
+class TestJunctionStates:
+    def test_live_junction_is_detected_and_counted(self, tmp_path):
+        """Controle positif : un lien vers un store peuple reste `ok`."""
+        lake = _make_lake_with_mathlib_link(
+            tmp_path, "L", tmp_path / "store", populate=True)
+        r = analyse_lake(lake, {})
+        assert r["junction"] is True
+        assert r["status"] == "partial"  # 1 olean, sous le plancher
+        assert r["oleans"] == 1
+        assert r["realpath"]  # un cache PHYSIQUE alimente le dedoublonnage
+
+    def test_junction_to_empty_store_stays_cold(self, tmp_path):
+        """Non-regression : cible presente mais vide -> `cold`, pas `dangling`."""
+        lake = _make_lake_with_mathlib_link(
+            tmp_path, "L", tmp_path / "store", populate=False)
+        r = analyse_lake(lake, {})
+        assert r["junction"] is True
+        assert r["status"] == "cold"
+        assert r["oleans"] == 0
+
+    def test_dangling_junction_is_not_absent(self, tmp_path):
+        """Le lien survit a la disparition de sa cible : etat `dangling`."""
+        store = tmp_path / "store"
+        lake = _make_lake_with_mathlib_link(tmp_path, "L", store, populate=True)
+        shutil.rmtree(store)  # la cible disparait, le lien reste
+
+        r = analyse_lake(lake, {})
+        assert r["status"] == "dangling", r
+        assert r["junction"] is True
+        assert r["oleans"] == 0
+        assert r["junction_target"] == str(store)
+
+    def test_dangling_junction_does_not_enter_physical_cache_count(self, tmp_path):
+        """Une cible disparue n'est pas un cache physique (cle `realpath` absente)."""
+        store = tmp_path / "store"
+        lake = _make_lake_with_mathlib_link(tmp_path, "L", store, populate=True)
+        shutil.rmtree(store)
+
+        r = analyse_lake(lake, {})
+        assert "realpath" not in r
+        assert r["junction_target"] == str(store)
+
+    def test_control_real_dir_is_not_a_junction(self, tmp_path):
+        """Controle negatif : un repertoire REEL n'est jamais vu comme un lien.
+
+        Sans lui, une detection qui rendrait `junction=True` partout passerait les
+        quatre tests precedents sans rien prouver.
+        """
+        lake = _make_lake(tmp_path, "L", body='require mathlib from git')
+        _write(lake / ".lake" / "packages" / "mathlib" / "Mathlib" / "Init.olean")
+        r = analyse_lake(lake, {})
+        assert r["junction"] is False
+        assert r["status"] == "partial"
+        assert "junction_target" not in r
+
+
 # ---------------------------------------------------------------------------
 # main() CLI routing
 #
@@ -267,3 +369,36 @@ def test_bad_repo_path_exits_2(self, tmp_path):
         import check_mathlib_cache as mod
 
         assert mod.main(["--repo-path", str(tmp_path / "nope")]) == 2
+
+    def test_strict_counts_dangling_junction(self, tmp_path):
+        """``--strict`` rougit sur une jonction pendante, pas seulement sur `cold`.
+
+        Une jonction pendante se presente comme un paquet installe et n'atteint
+        rien : c'est un etat casse, la ou `absent` est l'etat normal d'un lac
+        jamais construit localement (lake recuperera le paquet lui-meme).
+        """
+        import json
+        import check_mathlib_cache as mod
+
+        (tmp_path / ".git").mkdir()
+        store = tmp_path / "store"
+        lake = _make_lake_with_mathlib_link(tmp_path, "L", store, populate=True)
+        shutil.rmtree(store)
+
+        out = tmp_path / "out.json"
+        argv = ["--repo-path", str(tmp_path), "--json-out", str(out)]
+
+        assert mod.main(argv) == 0  # advisory par defaut
+        assert mod.main(argv + ["--strict"]) == 1
+
+        payload = json.loads(out.read_text(encoding="utf-8"))
+        assert [r["status"] for r in payload["results"]] == ["dangling"], payload
+
+    def test_strict_ignores_absent(self, tmp_path):
+        """Controle negatif de la borne : `absent` (aucun lien) ne fait pas rougir."""
+        import check_mathlib_cache as mod
+
+        (tmp_path / ".git").mkdir()
+        _make_lake(tmp_path, "L", body="require mathlib from git")  # pas de .lake
+
+        assert mod.main(["--repo-path", str(tmp_path), "--strict"]) == 0