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
10 changes: 10 additions & 0 deletions docs/lean/junctions-scan-po-2024.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 :
Expand Down
4 changes: 2 additions & 2 deletions scripts/lean/check_mathlib_cache.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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))
Expand Down
5 changes: 3 additions & 2 deletions scripts/lean/tests/test_check_mathlib_cache.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
Loading