diff --git a/docs/lean/junctions-scan-po-2024.md b/docs/lean/junctions-scan-po-2024.md index 148a6f799a..41d4472d98 100644 --- a/docs/lean/junctions-scan-po-2024.md +++ b/docs/lean/junctions-scan-po-2024.md @@ -134,6 +134,16 @@ Deux lignes du script sont des **déplacements**, pas des purges, et ne figurent **Proposition** (hors périmètre de cette PR, grain `guard`/`tooling` à dispatcher) : donner à `Invoke-Scan` trois états au lieu d'un — `JUNCTION-OK` / `JUNCTION-COLD` / `JUNCTION-MISMATCH` — en résolvant la cible (`realpath`) et en comparant le `rev8` du manifest à celui du nom du store, plus un comptage d'oleans. `check_mathlib_cache.py` porte déjà les primitives (`MATHLIB_OLEAN_FLOOR = 1000`) ; l'y brancher éviterait de réécrire l'instrument. +### Seconde occurrence consolidée (po-2025, 2026-10-08) + +Le scan po-2025 — mesure intégrale préservée sur le dashboard RooSync `workspace-CoursIA` (post `[INFO] PRESERVATION INTEGRALE`, 08/10) — confirme les deux cécités et en mesure une **troisième, propre à l'organe dédié** : + +1. **Même cécité de cible** (`JUNCTIONED` terminal) : 18 jonctions, **0 utilisable** — dont **14 pendantes** (classe absente de po-2024, qui n'avait que des jonctions vivantes vers store vide) et 4 `MISMATCH` vers `v4.32.1-520045ab`. +2. **Même cécité de classement** : `game_theory`/`percolation`/`knot`/`argumentation` listés sous le groupe déclaré `v4.33.0-db584cd6` alors que leur cible réelle est `v4.32.1-520045ab`. +3. **`check_mathlib_cache.py` classe les pendantes en `reel`** : retour anticipé l.88 (`if not mathlib.exists(): status = "absent"; return` — `exists()` **suit** le lien vers une cible absente) avant la détection de jonction l.93-96, puis l.158 affiche `reel`. `Path.is_junction()` (Python ≥ 3.12) et `Path.resolve()` voient juste ; c'est l'**ordre des tests** qui perd l'information. Le verdict global d'atteignabilité reste exact — seule la classe de panne est faussée. + +**Méthode durable** (une jonction ne se juge pas sur son libellé) : résoudre la cible ET énumérer **à travers** le lien — `fsutil reparsepoint query` (balise `0xa0000003`), `Test-Path` sur le chemin résolu, énumération `\\?\` à travers la jonction (un `0` rendu par `find`/`islink` sur le chemin du lien ne prouve rien), `lean-toolchain` du lac vs groupe du `share-state.json`. La proposition ci-dessus s'élargit à **quatre** états : `JUNCTION-OK` / `JUNCTION-COLD` / `JUNCTION-MISMATCH` / `JUNCTION-DANGLING`. + ## 5. Correction du tableau multi-machine `docs/lean/junctions-scan-po-2027.md` porte une ligne po-2024 reprise de #14296 **sans re-mesure** (son §« Provenance des colonnes » le dit explicitement). Re-mesurée : diff --git a/scripts/lean/check_mathlib_cache.py b/scripts/lean/check_mathlib_cache.py index 03ad4ea93e..92d26cf0d2 100644 --- a/scripts/lean/check_mathlib_cache.py +++ b/scripts/lean/check_mathlib_cache.py @@ -14,7 +14,7 @@ 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`. + lues `absent`/`reel`. Detail : `docs/lean/junctions-scan-po-2024.md` §4 « Seconde occurrence consolidée (po-2025) » (mesure intégrale préservée sur le dashboard RooSync workspace-CoursIA, 08/10). 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 @@ -93,7 +93,7 @@ def analyse_lake(lake: Path, cache: dict[str, int]) -> dict: # 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). + # l'inverse de la verite (14 jonctions po-2025, cf junctions-scan-po-2024.md §4, seconde occurrence). # `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)) diff --git a/scripts/lean/tests/test_check_mathlib_cache.py b/scripts/lean/tests/test_check_mathlib_cache.py index b674be7923..8f0bf1666f 100644 --- a/scripts/lean/tests/test_check_mathlib_cache.py +++ b/scripts/lean/tests/test_check_mathlib_cache.py @@ -56,7 +56,8 @@ def _link_dir(link: Path, target: Path) -> None: 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) + capture_output=True, text=True, + encoding="utf-8", errors="replace") if proc.returncode != 0: pytest.skip(f"mklink /J indisponible : {proc.stderr.strip() or proc.stdout.strip()}") return @@ -265,7 +266,7 @@ def test_result_carries_lake_path(self, tmp_path): # 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 : +# aucune utilisable) et documentes dans docs/lean/junctions-scan-po-2024.md §4 (seconde occurrence consolidée) : # - `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