diff --git a/docs/lean/junctions-scan-po-2027.md b/docs/lean/junctions-scan-po-2027.md index 70dc3e9d95..2a102ab9aa 100644 --- a/docs/lean/junctions-scan-po-2027.md +++ b/docs/lean/junctions-scan-po-2027.md @@ -27,7 +27,9 @@ Voir aussi : | Empreinte totale Mathlib | **0 Go** | | Économie jonction-cluster potentielle | **0 GB** | -**Verdict** : **machine po-2027 = réservoir identifié, pas amorcé**. Aucun checkout Mathlib réel n'existe sur cette machine ; les `.lake/packages/` sont soit absents, soit restreints à `config/` (lake jamais exécuté localement). C'est le cas prédit par l'acceptance de #13962 : « Une lane qui trouve 0 checkout réel n'a rien à faire et le dit ». +**Verdict** : **worktree scanné de po-2027 = réservoir identifié, pas amorcé**. Dans le seul worktree couvert par ce Scan, aucun checkout Mathlib réel n'existe ; les `.lake/packages/` y sont soit absents, soit restreints à `config/` (lake jamais exécuté localement). C'est le cas prédit par l'acceptance de #13962 : « Une lane qui trouve 0 checkout réel n'a rien à faire et le dit ». + +> **Portée (#15568)** — le Scan opère depuis le repo-root courant et ne voit donc que **ce worktree-là**. Un checkout Mathlib logé dans un autre worktree de po-2027 échappe à la mesure : c'est le faux négatif déjà observé au c.857 (#14296, un checkout dans un autre worktree que le scanné). Ce rapport ne consigne pas le `git worktree list` de po-2027, donc rien ici ne soutient une formulation au niveau **machine**. Les énoncés de portée machine de ce document ont été bornés au worktree scanné ; pour une mesure réellement machine-wide, il faudrait rejouer le Scan dans chaque worktree listé et publier le total. ## Sortie verbatim du Scan @@ -81,23 +83,27 @@ Note : l'alignement des manifests (#2611 etape 2) peut elargir les groupes. ## Comparaison multi-machine -| Mesure | ai-01 (#13962) | po-2026 (#14038) | po-2027 (c.1059) | -|---|---:|---:|---:| -| Checkouts Mathlib réels | **17** | 0 | **0** | -| Jonctions actives | 0 | 0 | **0** | -| Empreinte totale | ~110 Go | 0 Go | **0 Go** | -| Groupes mutualisables | 1 (15 lacs) | 1 (19 lacs) | **2 (13 + 9 lacs)** | -| Économie jonction-cluster | ~90 Go | 0 Go | **0 GB** | +| Mesure | ai-01 (#13962) | po-2023 (#15070) | po-2024 (#14296) | po-2026 (#14038) | po-2027 (c.1059) | +|---|---:|---:|---:|---:|---:| +| Checkouts Mathlib réels | **17** | **3** | 0 | 0 | **0** | +| Jonctions actives | 0 | 0 | 0 | 0 | **0** | +| Empreinte totale | ~110 Go | **1,28 Go** | 0 Go | 0 Go | **0 Go** | +| Groupes mutualisables | 1 (15 lacs) | **2 (13 + 9 lacs)** | 1 (19 lacs) | 1 (19 lacs) | **2 (13 + 9 lacs)** | +| Économie jonction-cluster | ~90 Go | **0,64 Go** | 0 Go | 0 Go | **0 GB** | + +> **Provenance des colonnes (#15568)** — po-2023 vient de #15070 (Scan du 2026-09-07, PR fermée) et po-2024 de `docs/lean/cluster-junctions-c857.md` (#14296, c.857, Scan du 2026-09-02). Ces deux mesures ont été produites par leurs lanes avec le même instrument ; leurs chiffres sont repris **tels quels**, sans re-mesure (acceptance 3 de #15568). Elles partagent la borne de portée décrite plus haut : chacune est une mesure **de worktree**, pas de machine. -Le réservoir identifié sur po-2027 (22 lacs mutualisables) **excède en nombre** celui de po-2026 (19), mais reste à **0 Go** faute de checkout donneur. La conclusion est homogène sur les 3 machines scannées : le réservoir est large, l'amorçage est nul. +Le réservoir identifié sur po-2027 (22 lacs mutualisables) **excède en nombre** celui de po-2026 (19), mais reste à **0 Go** faute de checkout donneur. Les **cinq** machines mesurées à ce jour — ai-01, po-2023, po-2024, po-2026, po-2027 — partagent le même profil : **le réservoir est large, l'amorçage est quasi nul**. La seule valeur non nulle du plateau est po-2023, dont les 3 checkouts physiques (1,28 Go cumulés) rendent **0,64 Go** récupérables ; sa lane a conclu que cette économie marginale ne justifiait pas un Apply. ## Cause -**Aucun des 27 lacs n'a exécuté `lake update` localement sur po-2027** : les `.lake/packages/mathlib` n'existent pas ou se limitent à `config/`. La machine porte les **manifests** (qui définissent la dépendance transitive) mais pas les **build artifacts**. C'est cohérent avec le profil po-2027 = worker CPU non Lean dédié (kernel `lean4-wsl` invoqué pour les preuves Lean mais sans cache Mathlib local — exécution sur runners `coursia-lean` self-hosted). +**Aucun des 27 lacs n'a exécuté `lake update` localement dans le worktree scanné de po-2027** : les `.lake/packages/mathlib` n'y existent pas ou se limitent à `config/`. Ce worktree porte les **manifests** (qui définissent la dépendance transitive) mais pas les **build artifacts**. C'est cohérent avec le profil po-2027 = worker CPU non Lean dédié (kernel `lean4-wsl` invoqué pour les preuves Lean mais sans cache Mathlib local — exécution sur runners `coursia-lean` self-hosted). ## Conclusion opérationnelle -Le périmètre po-2027 du grain #13962 est **vide**. C'est exactement le cas que l'acceptance prédit : « Une lane qui trouve 0 checkout réel n'a rien à faire et le dit ». +Le périmètre de po-2027 **dans le worktree scanné** est **vide**. C'est exactement le cas que l'acceptance prédit : « Une lane qui trouve 0 checkout réel n'a rien à faire et le dit ». + +Nuance de portée (#15568) : « vide » qualifie le worktree mesuré, pas la machine. Un checkout présent dans un autre worktree de po-2027 resterait invisible ici, et un Apply y aurait alors une cible. La recommandation ci-dessous (« aucune action sur po-2027 ») porte donc sur ce seul worktree. **Recommandation pour coordinateur** :