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

[jsboige]

Grain: MED/guard — lane myia-po-2025:CoursIA — prev: DEEP/notebook-python #19620

Le defaut mesure

Sur po-2025, check_mathlib_cache.py rend absent + reel pour les 14 jonctions pendantes de la machine — le premier mot dit « aucun checkout », le second dit « repertoire physique ». Les deux sont faux, et le second est l'inverse exact de la verite.

Releve verbatim, --repo-path D:/dev/CoursIA :

  absent    assignment_lean                   0 olean  reel
  cold      game_theory_lean                  0 olean  junction

La cause est un retour anticipe qui precede la detection du lien :

Ligne (avant)	Code	Effet sur une jonction pendante
88	if not mathlib.exists(): → status = "absent"; return	exists() suit le lien vers une cible disparue → False → on sort avant la l. 93-96
93-96	real = os.path.realpath(mathlib) puis junction = …	jamais atteint : la cle junction reste absente du resultat
158	flag = "junction" if r.get("junction") else "reel "	affiche reel — l'exact contraire de la verite

L'API n'est pas en cause, l'ordre des tests l'est. Mesure de la divergence, sur le meme chemin :

os.path.islink  : False      Path.is_symlink() : False
os.path.exists  : False      Path.is_junction(): True      <- la seule API qui voit juste
os.path.isdir   : False      Path.resolve()    : <la cible, correctement resolue>

Le fichier portait deja l'avertissement exact a sa derniere ligne (« un comptage a 0 via find ou islink ne prouve rien sur une junction ») : l'organe qui l'ecrit classait 14 jonctions comme des repertoires reels.

Le correctif

Detection du lien avant le test d'existence, et un troisieme etat, dangling :

• junction + junction_target sont calcules en premier (divergence de os.path.realpath) ;
• mathlib.exists() faux et lien present → dangling (et non absent) ;
• junction_target est une cle distincte de realpath : une cible disparue n'est pas un cache physique et n'entre donc pas dans le dedoublonnage ;
• --strict compte dangling alors qu'il ne compte pas absent — un lac sans checkout est l'etat normal d'un lac jamais construit localement (lake le recupere), une jonction pendante se presente comme un paquet installe et peut faire croire a un cache partage utilisable.

S'ajoutent la ligne de resume (jonctions pendantes: N), un bloc d'avertissement dedie et l'elargissement de l'avis « cache purge » a cold or partial or dangling.

Avant / apres sur l'arbre reel po-2025

avant : Lakes: 36 | mathlib ok: 0 | froid: 4 | partiel: 1 | non installe: 27 | caches physiques distincts: 2
apres : Lakes: 36 | mathlib ok: 0 | froid: 4 | partiel: 2 | non installe: 13 | jonctions pendantes: 14 | caches physiques distincts: 3

Le basculement 27 → 13 + 14 est l'effet du correctif : les 14 jonctions pendantes sortent de non installe et deviennent un etat nomme.

Le reste du delta ne vient pas de ce correctif et je ne me l'attribue pas : partiel 1→2 et caches distincts 2→3 viennent d'un lake exe cache get + lake build de differential_lean qui tournait pendant le releve et a cree son .lake/packages/mathlib (verifie : le repertoire existe, horodate en cours de mesure ; le log montre Built Cache.Lean). Le compte de checkouts physiques est donc un instantane, la ou les 18 jonctions sont stables — un lien ne se peuple pas tout seul.

Le verdict global mathlib ok: 0 / 36 est inchange : aucune des deux cecites ne fabrique un faux « ok ». Elles faussent le diagnostic (quelle classe de panne, sur quel lac), pas le verdict d'atteignabilite.

Tests

python -m pytest scripts/lean/tests/test_check_mathlib_cache.py -q → 35 passed, 0 skipped.

Cinq tests pour les trois etats de lien, chacun avec son controle :

Test	Ce qu'il epingle
test_live_junction_is_detected_and_counted	controle positif — un lien vers un store peuple reste partial/ok et alimente le cache
test_junction_to_empty_store_stays_cold	non-regression — cible presente mais vide → cold, pas dangling
test_dangling_junction_is_not_absent	le lien survit a la disparition de sa cible → dangling + junction_target
test_dangling_junction_does_not_enter_physical_cache_count	une cible disparue n'est pas un cache physique (pas de cle realpath)
test_control_real_dir_is_not_a_junction	controle negatif — sans lui, une detection qui rendrait True partout passerait les quatre autres

Plus deux tests CLI : --strict rougit sur une jonction pendante (test_strict_counts_dangling_junction) et ne rougit pas sur absent (test_strict_ignores_absent), soit les deux bornes de la decision.

Les liens de test passent par une junction (cmd /c mklink /J), qui ne demande pas d'elevation sous Windows — la ou symlink_to en exige une et fait pytest.skip.

Un test qui ne tournait pas se met a tourner. test_cache_dedups_by_realpath epingle le dedoublonnage par realpath — precisement la propriete en jeu ici — et se skippait en permanence sous Windows parce qu'il utilisait symlink_to. Il est branche sur le meme helper : il passe, et la suite n'a plus aucun skip (35 passed / 0 skipped, contre 34 passed / 1 skipped avant).

Perimetre

Deux fichiers, aucun autre :

• scripts/lean/check_mathlib_cache.py — detection, etat dangling, resume, --strict
• scripts/lean/tests/test_check_mathlib_cache.py — 5 tests de jonction, 2 tests CLI, 1 test debloque

Aucune modification de setup_shared_mathlib.ps1 ni d'un lake : le rapport de scan (#19860) a mesure que po-2025 n'a ni donneur ni sauvegarde, et un Apply serait au mieux inoperant. Le geste utile sur cette machine — retirer les 18 jonctions — est un geste disque qui attend un GO nominatif ; il n'est pas dans cette PR.

See #13962 · Part of #4362

🤖 Generated with Claude Code

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 19866
head: 6e8abe0
complete: true
body: read
comments-reviewed: 0
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: db2debca49de766c5abd1a382594250a12e7cad8ab0fc6f17a98a52547e7caa4
diff-files: 2
diff-additions: 185
diff-deletions: 14
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19866
organ-rc: 3
[/ADJOINT PREFLIGHT]

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-ai-01:CoursIA
pr: 19866
head: 6e8abe0
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 03c92cf58d75f883bb5b70d57325e7429dd716e6b7305dec9f170e9c409a4d83
diff-files: 2
diff-additions: 185
diff-deletions: 14
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
supersedes: 1
supersedes-why: le dossier BLOCKED precedent attestait un etat de jambes ou de levees depasse ; a la meme tete, la derivation live rend checks verts, B.0 clear
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19866
organ-rc: 0
[/ADJOINT PREFLIGHT]

Derivation live READY a la tete vive : le dossier BLOCKED anterieur attestait des jambes alors en cours ; jambes latest-wins vertes, B.0 clear, aucun thread non resolu.