Skip to content

docs(lean,#13962,c.1221): scan NTFS junctions po-2026 fresh - 15 checkouts / 4,09 GB / cluster db584cd6 #18020

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 4 commits into from
Sep 27, 2026
Merged

docs(lean,#13962,c.1221): scan NTFS junctions po-2026 fresh - 15 checkouts / 4,09 GB / cluster db584cd6 #18020

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
04efeb7
docs(lean,#13962,c.1221): scan NTFS junctions po-2026 fresh - 11 chec…
claude Sep 27, 2026
3ed19e2
docs(lean,#13962,c.1223): recount verbatim - 11 → 15 checkouts + conv…
claude Sep 27, 2026
958551c
docs(lean,#13962,c.1223): commit c1205.archive - 11 → 15 + convention…
claude Sep 27, 2026
f14739a
Merge branch 'main' into docs/13962-scan-po2026-fresh
jsboige Sep 27, 2026
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
197 changes: 114 additions & 83 deletions docs/lean/junctions-scan-po-2026.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,47 +1,53 @@
# Mathlib NTFS junctions scan — `myia-po-2026` (2026-09-01)
# Mathlib NTFS junctions scan — `myia-po-2026` (2026-09-27, c.1221)

**Issue** : #13962 (enfant de #4362)
**Machine** : `myia-po-2026` (worker Lean/QC/SymbolicLearning)
**Script** : `scripts/lean/setup_shared_mathlib.ps1 -Mode Scan` (#2611)
**Script** : `scripts/lean/setup_shared_mathlib.ps1 -Mode Scan` (#2611, ferme depuis 2026-07-03)
**Mode** : Scan (lecture seule, aucune modification)

## TL;DR

**Économie potentielle sur po-2026 : 0 GB.** Aucun des 19 lakes mutualisables
n'a de checkout local Mathlib. La machine n'a jamais fait de
`lake exe cache get` ni de `lake build` initial. L'outillage existe
(`setup_shared_mathlib.ps1` ferme depuis le 2026-07-03) mais l'application
n'a jamais eu lieu **et n'a pas de sens ici** : il n'y a rien à mutualiser.
**Économie potentielle sur po-2026 : 4,09 GB** (cluster v4.33.0-db584cd6,
23 lacs mutualisables, donneur candidat = `game_theory_lean` à 11,14 GB).
Un lac est déjà JUNCTIONED (`sensitivity_lean`), validant le principe sur cette
machine.

Ce rapport documente la **mesure po-2026** en contraste avec la mesure
ai-01 (17 checkouts réels / ~110 Go / économie ~90 Go) rapportée par
l'auteur de #13962 le 2026-09-01.
**Mise à jour majeure vs cycle 90 (2026-09-01)** : l'ancien rapport
annonçait **0 GB économie** (aucun checkout local). La situation a
fondamentalement évolué : **14 lacs du cluster `db584cd6` ont depuis acquis un checkout physique** (probablement via `lake exe cache get` durant l'exécution des notebooks en kernel `lean4-wsl` sur WSL `machine-2026`), dont **4 avec Mathlib réellement téléchargé** (GB > 0) — `game_theory_lean` 11,14, `conway_lean` 0,58, `grothendieck_lean` 2,93, `knot_lean` 0,58. Le cluster mutualisable po-2026 existe désormais et l'Apply devient actionnable.

## Sortie verbatim du Scan (2026-09-01)
> **Convention de comptage (c.1223, post-relecture Hermes #18020)** : « checkout physique » = `lake-manifest` présent dans `.lake/packages/mathlib/` (peut être 0 GB si seul le manifest est acquis, sans les oleans). « Avec Mathlib téléchargé » = checkout dont la taille dépasse 0 GB (manifest + oleans). Le verbatim liste **14 `checkout physique` dans le cluster `db584cd6`** (4 avec Mathlib téléchargé, 10 à 0 GB) + **1 `JUNCTIONED`** (`sensitivity_lean`) + **1 `checkout physique` hors cluster** (`formal_logic_lean`, 6,69 GB, isolé `v4.33.1-0df444a3`) + **8 `pas de checkout local`**. **Total acquis depuis c.90 = 15 lacs avec checkout, dont 5 avec Mathlib téléchargé.** Le compte « 11 » utilisé dans une première rédaction (cf. cid 5853418531 et version antérieure de cette page) ne dérive pas du verbatim et a été remplacé.

## Sortie verbatim du Scan (2026-09-27, c.1221)

```
=== Projets Lake avec dependance mathlib (24) ===
=== Projets Lake avec dependance mathlib (29) ===

--- Groupe leanprover_lean4_v4.32.1-520045ab [MUTUALISABLE] : toolchain=leanprover/lean4:v4.32.1 mathlib=520045ab ---
--- Groupe leanprover_lean4_v4.33.0-db584cd6 [MUTUALISABLE] : toolchain=leanprover/lean4:v4.33.0 mathlib=db584cd6 ---
MyIA.AI.Notebooks/GameTheory/assignment_lean pas de checkout local
MyIA.AI.Notebooks/GameTheory/game_theory_lean pas de checkout local
MyIA.AI.Notebooks/GameTheory/minimax_lean pas de checkout local
MyIA.AI.Notebooks/GameTheory/repeated_games_lean pas de checkout local
MyIA.AI.Notebooks/ML/learning_theory_lean pas de checkout local
MyIA.AI.Notebooks/Probas/decision_theory_lean pas de checkout local
MyIA.AI.Notebooks/QuantConnect/kelly_lean pas de checkout local
MyIA.AI.Notebooks/GameTheory/game_theory_lean checkout physique (11.14 GB)
MyIA.AI.Notebooks/GameTheory/minimax_lean checkout physique (0 GB)
MyIA.AI.Notebooks/GameTheory/repeated_games_lean checkout physique (0 GB)
MyIA.AI.Notebooks/ML/learning_theory_lean checkout physique (0 GB)
MyIA.AI.Notebooks/Probas/Applications/Percolation/percolation_lean pas de checkout local
MyIA.AI.Notebooks/Probas/decision_theory_lean checkout physique (0 GB)
MyIA.AI.Notebooks/QuantConnect/kelly_lean checkout physique (0 GB)
MyIA.AI.Notebooks/Search/search_lean pas de checkout local
MyIA.AI.Notebooks/Sudoku/sudoku_lean pas de checkout local
MyIA.AI.Notebooks/Sudoku/sudoku_lean checkout physique (0 GB)
MyIA.AI.Notebooks/SymbolicAI/Lean/Serre100/serre100_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Lean/calibration_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean checkout physique (0.58 GB)
MyIA.AI.Notebooks/SymbolicAI/Lean/formal_groups_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Lean/galois_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Planners/planning_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Tweety/argumentation_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Lean/grothendieck_lean checkout physique (2.93 GB)
MyIA.AI.Notebooks/SymbolicAI/Lean/hecke_lean pas de checkout local
MyIA.AI.Notebooks/SymbolicAI/Lean/knot_lean checkout physique (0.58 GB)
MyIA.AI.Notebooks/SymbolicAI/Lean/mathlib_examples checkout physique (0 GB)
MyIA.AI.Notebooks/SymbolicAI/Lean/sensitivity_lean JUNCTIONED
MyIA.AI.Notebooks/SymbolicAI/Planners/planning_lean checkout physique (0 GB)
MyIA.AI.Notebooks/SymbolicAI/SmartContracts/erc20_lean checkout physique (0 GB)
MyIA.AI.Notebooks/SymbolicAI/Tweety/argumentation_lean checkout physique (0 GB)
=> economie potentielle : 4.09 GB (garder le plus gros comme donneur)

--- Groupe leanprover_lean4_v4.25.0-1ccd71f8 [isole] : toolchain=leanprover/lean4:v4.25.0 mathlib=1ccd71f8 ---
MyIA.AI.Notebooks/SymbolicAI/Lean/agent_tests/prover/session_state/reference_docs/stable_marriage/upstream pas de checkout local
Expand All @@ -50,80 +56,105 @@ l'auteur de #13962 le 2026-09-01.
MyIA.AI.Notebooks/GameTheory/conway_cgt_lean pas de checkout local

--- Groupe leanprover_lean4_v4.32.1-520045ab [isole] : toolchain=leanprover/lean4:v4.32.1 mathlib=520045ab ---
MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters pas de checkout local

--- Groupe leanprover_lean4_v4.33.0-db584cd6 [isole] : toolchain=leanprover/lean4:v4.33.0 mathlib=db584cd6 ---
MyIA.AI.Notebooks/Search/discrepancy_lean pas de checkout local

--- Groupe leanprover_lean4_v4.33.0-db584cd6 [isole] : toolchain=leanprover/lean4:v4.33.0 mathlib=db584cd6 ---
MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean pas de checkout local
MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters pas de checkout local

=== Economie totale potentielle (groupes en l'etat) : 0 GB ===
--- Groupe leanprover_lean4_v4.33.1-0df444a3 [isole] : toolchain=leanprover/lean4:v4.33.1 mathlib=0df444a3 ---
MyIA.AI.Notebooks/SymbolicAI/Lean/formal_logic_lean checkout physique (6.69 GB)

=== Economie totale potentielle (groupes en l'etat) : 4.09 GB ===
Note : l'alignement des manifests (#2611 etape 2) peut elargir les groupes.
```

## Première vérification (cycle 90, po-2026)

| Mesure | ai-01 (rapport #13962) | po-2026 (mesure cycle 90) |
|---|---|---|
| Checkouts Mathlib réels | **17** | **0** |
| Jonctions NTFS actives | 0 | 0 |
| Taille échantillon checkout | 6,46 Go | N/A |
| Empreinte totale | ~110 Go | 0 Go |
| Clusters homogène rev `520045ab` | 15 | 19 manifest-only, 0 réels |
| Économie jonction-cluster | ~90 Go | **0 Go** |

## Conclusion opérationelle

Le périmètre po-2026 du grain #13962 est **vide** : aucun checkout à
mutualiser, aucun espace à récupérer. C'est exactement le cas que
l'issue mentionne (« Une lane qui trouve 0 checkout réel n'a rien à
faire et le dit »).

## Causes probables (à confirmer)

1. **po-2026 = worker QC/Lean execution, pas cluster de build**. Les
notebooks Lean s'exécutent via le kernel `lean4-wsl` (lui-même
résident sur la VM WSL `machine-2026`), pas en checkouts natifs
`lake build` sur po-2026.
2. **Le WSL est l'env de build canonique** (cf. CLAUDE.md section F +
memory `wsl-kernel-execution`). Le cycle 87 `lean4-wsl notebook exec`
recipe confirme ce pattern.
3. **ai-01 porte le cluster de jonction** : c'est la mesure mentionnée
par l'auteur #13962. po-2026 ne contribue pas au parc de checkouts
et n'a rien à mutualiser localement.
## Première vérification (c.1221, po-2026)

| Mesure | ai-01 (rapport #13962, 2026-09-01) | po-2026 cycle 90 (2026-09-01) | po-2026 c.1221 (2026-09-27) |
|---|---|---|---|
| Checkouts Mathlib réels | 17 | 0 | **15** (+ 1 JUNCTIONED préexistant) — dont 5 avec Mathlib téléchargé |
| Jonctions NTFS actives | 0 | 0 | 1 (`sensitivity_lean`) |
| Taille échantillon checkout | 6,46 Go | N/A | 11,14 GB (donneur = `game_theory_lean`) |
| Empreinte totale checkouts | ~110 Go | 0 Go | ~21,9 GB |
| Cluster homogène `db584cd6` (v4.33.0) | non listé (rev `520045ab` citée) | 19 manifest-only | **23 lacs mutualisables** |
| Économie jonction-cluster | ~90 Go | 0 Go | **4,09 GB** |

## Évolution entre c.90 et c.1221

L'écart entre les deux mesures po-2026 (0 → 15 checkouts physiques, dont 5 avec Mathlib téléchargé) reflète :

1. **Exécution de notebooks** sur po-2026 avec kernel `lean4-wsl` au cours des
cycles intermédiaires. Plusieurs notebooks Lean (notamment dans
`SymbolicAI/Lean/`) déclenchent `lake exe cache get` en arrière-plan, ce qui
popule progressivement les checkouts locaux même sans `lake build` explicite.
2. **Pinnage convergent** : la majorité des lacs se sont alignés sur
`leanprover/lean4:v4.33.0` + `mathlib=db584cd6`, qui devient le cluster
majoritaire po-2026.
3. **Premier JUNCTIONED** : `sensitivity_lean` est déjà passé en jonction (cf.
`docs/lean/junctions-scan-po-2027.md` cycle 1205 qui rapportait aussi
cette tendance côté po-2027). Le mécanisme fonctionne sur po-2026.

## Conclusion opérationnelle

**L'Apply est désormais actionnable sur po-2026** :

1. **Cluster cible** : `leanprover/lean4:v4.33.0` + `mathlib=db584cd6`,
23 lacs, donneur candidat = `game_theory_lean` (11,14 GB).
2. **Économie attendue** : 4,09 GB en posant les jonctions sur les
`checkout physique > 0` (conway_lean 0,58 + grothendieck_lean 2,93 +
knot_lean 0,58 = ~4,09 GB).
3. **Préconditions respectées** (cf. #13962 § Acceptance) :
- lake-manifest identique sur tous les membres (cluster MUTUALISABLE) ;
- toolchain identique (`v4.33.0`) ;
- `sensitivity_lean` déjà JUNCTIONED valide la procédure.
4. **8 lacs sans checkout local** (`assignment_lean`, `percolation_lean`,
`search_lean`, `serre100_lean`, `formal_groups_lean`, `galois_lean`,
`hecke_lean`, `calibration_lean`) — leur premier `lake build` ira chercher
dans le cache central une fois les jonctions posées, **plafonnant la
croissance** au lieu d'ajouter +6,46 Go chacun (cf. effet prospectif
ai-01 #13962 §Mesure).

## Recommandation pour ai-01 / coordinateur

L'auteur de #13962 est sur ai-01 (vérifié par la signature de la mesure).
**Le grain s'exécute sur ai-01, pas po-2026**. Le Apply doit être
décidé et lancé sur ai-01 :
L'auteur de #13962 est sur ai-01. **Décision Apply** :

1. **Scan ai-01** déjà mesuré (rapport #13962) : 17 checkouts, 110 Go,
cluster de 15.
2. **Apply ai-01** : `pwsh scripts/lean/setup_shared_mathlib.ps1 -Mode Apply
-Group 520045ab -Build -RemoveBackups` -- après Scan + accord
explicite (cf. #13962 §"Prudence").
3. **Vérification anti-régression** : pour chaque lake jonctionné,
`lake build SUCCESS` post-jonction + `grep -c sorry` inchangé.
4. **Aucune action sur po-2026**.
1. **Scan ai-01** (déjà mesuré #13962) : 17 checkouts / 110 Go / cluster `520045ab`.
2. **Scan po-2026** (ce rapport, c.1223) : **15 checkouts physiques** (5 avec Mathlib téléchargé, 10 à 0 GB manifest-only) / ~22 Go / cluster `db584cd6`, + 1 JUNCTIONED préexistant.
3. **Apply po-2026** : `pwsh scripts/lean/setup_shared_mathlib.ps1 -Mode Apply -Group db584cd6 -Build` (sans `-RemoveBackups` au premier essai pour conserver la sécurité anti-régression).
4. **Vérification anti-régression (HARD bloquant)** : pour chaque lake jonctionné, `lake build SUCCESS` post-jonction + `python scripts/lean/count_code_sorry.py --json` `distinct_code_sorry` inchangé avant/après.
5. **Apply ai-01** : décision séparée du coordinateur, scan distinct.

## Suivi machine-par-machine (à étendre si d'autres lanes pertinentes)
**Aucun Apply n'est lancé par ce rapport.** Le worker po-2026 documente et
rend la main. La décision Apply reste coordinateur (Tell c.1502 strict ★★
fondateur respect).

| Machine | Scan | Checkouts réels | Économie potentielle |
|---|---|---|---|
| ai-01 | ✅ (rapport #13962) | 17 | ~90 Go |
| po-2026 | ✅ (cycle 90, ce rapport) | 0 | 0 Go |
| po-2023 | à mesurer | ? | ? |
| po-2024 | à mesurer | ? | ? |
| po-2025 | à mesurer | ? | ? |
## Suivi machine-par-machine

| Machine | Scan | Checkouts réels | Jonctions | Économie potentielle |
|---|---|---|---|---|
| ai-01 | ✅ (#13962) | 17 | 0 | ~90 Go (rev `520045ab`) |
| po-2023 | ✅ (#17178) | mesuré | mesuré | mesuré |
| po-2024 | ✅ (#15938) | mesuré | mesuré | mesuré |
| po-2026 | ✅ (c.1221, ce rapport) | **15** | **1** | **4,09 Go** (rev `db584cd6`) |
| po-2027 | ✅ (#16375, c.1205) | mesuré | mesuré | mesuré |

## Fichier source de la mesure

Le rapport verbatim ci-dessus est aussi stocké dans le scratchpad du
worker po-2026 pour traçabilité : `scratchpad/junctions_scan_po2026.txt`
(cycle 90).
Rapport verbatim aussi stocké dans le scratchpad du worker po-2026 pour
traçabilité : `scratchpad/junctions_scan_po2026_c1221.out`.

## Voir aussi

- #13962 — mesure ai-01, Apply à décider par coordinateur
- #2611 — outillage `setup_shared_mathlib.ps1` (CLOSED, ferme)
- #4362 — EPIC parent (3 phases historiques CLOSED)
- #4363, #4364, #4365 — phases 1-2-3 (CLOSED sans application sur aucune machine)
- docs/lean/coordinator-workflow.md — workflow Lean PR discipline
- docs/lean/cluster-junctions-c857.md — référence cluster
- docs/lean/junctions-scan-po-2023.md — pair machine po-2023
- docs/lean/junctions-scan-po-2024.md — pair machine po-2024
- docs/lean/junctions-scan-po-2027.md — pair machine po-2027
- docs/lean/coordinator-workflow.md — workflow Lean PR discipline
- `docs/lean/junctions-scan-po-2026.md.c1205.archive` — version archive du rapport cycle 90 (preuve de préservation, Tell « Consolider != Archiver »)
Loading
Loading