Skip to content

docs(lean,#16034): datation precise des 9 jonctions 520045ab sur po-2027 (share-state.json 14/09 00:18) #16969

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 1 commit into from
Sep 22, 2026
Merged

docs(lean,#16034): datation precise des 9 jonctions 520045ab sur po-2027 (share-state.json 14/09 00:18) #16969

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
82 changes: 82 additions & 0 deletions docs/lean/junctions-scan-po-2027-CoursIA2.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -192,3 +192,85 @@ Prochaine etape conditionnelle :
- MEMORY `lean-warm-mathlib-junction-build.md` (po-2027 junctions warm-Mathlib pattern ; junction vers warm Mathlib d'un lake frere ; `count_sorry --repo` requis)
- MEMORY `lean_kernel_broken.md` (REPL cassé en lean4-wsl mais `lake build` natif OK)
- c.1203 (premier scan po-2027 manuel — 9 jonctions verifiees) ; c.1205 (rapport Scan present, ce document)

## V3 — Datation precise des 9 jonctions 520045ab (c.724)

C.724 — investigation `share-state.json` du store `.mathlib-cache/` pour reconcilier
l'etat V2 (9 jonctions actives, datation inconnue) avec le narratif c.1059 (V1 narrow
annoncait 0 jonction le 10/09) et l'absence de poses hors-Apply documentees sur
po-2027 (contrairement a po-2024 ou PR #15972 a date 4 poses manuelles).

### Source de verite

`D:\dev\CoursIA-2\.mathlib-cache\share-state.json` — fichier unique de l'outillage
`setup_shared_mathlib.ps1` (seule ecriture de fichier du script, l.337).
`LastWriteTime` filesystem = **2026-09-14T00:22:37+02:00**, soit **3 minutes 45
secondes apres** `createdAt` declare. Les 9 membres ont ete poses **simultanement**
par un seul `Invoke-Apply` (logique du script : enregistrement post-Apply).

### Champs autoritatifs

```json
{
"groupId": "leanprover_lean4_v4.32.1-520045ab",
"toolchain": "leanprover/lean4:v4.32.1",
"mathlibRev": "520045ab14e26149ee970e2e617ca04b09bde5d6",
"createdAt": "2026-09-14T00:18:52.9763479+02:00",
"members": [
...
{"relPath": "MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean",
"isDonor": true},
...
]
}
```

`isDonor: true` est sur `conway_lean` uniquement — c'est le **membre donneur**,
celui dont le checkout Mathlib pre-existant a ete **promu** cible du store
(et non jonctionne). Les 8 autres ont ete **jonctionnes** vers cette cible.
`hadBackup: false` partout — pas de `.bak-2611` residuel, Apply mene a terme
sans rollback.

### Reconciliation avec les narratifs anterieurs

| Source | Date | Lecture | Reel |
|---|---|---|---|
| Rapport V1 narrow c.1059 | 2026-09-10 | 0 jonction sur worktree CoursIA | OK (worktree CoursIA != clone principal CoursIA-2) |
| Rapport V2 c.1205 | 2026-09-16 | 9 jonctions actives sur po-2027 CoursIA-2 | OK (mesure post-Apply, cf ci-dessous) |
| Claim initial #16034 | 2026-09-13 | "Apply jonctions NTFS po-2027" — non livre | **Apply execute 14/09 00:18 par une autre lane (auteur non identifie ici)** |
| Scan c.724 (ce cycle) | 2026-09-20 | 9 jonctions (5 dans cluster principal + 4 v4.33.0 manifest-vers-v4.32.1) | OK, identique a V2 |

L'Apply 14/09 a donc ete realise **entre** le claim du 13/09 et le scan du 16/09.
Le claim initial #16034 est **OBSOLETE** au sens strict : la livraison est faite,
mais **par une autre lane** que `myia-po-2027:CoursIA-2`. L'acceptance §1 (Scan
manifest-identique) etait deja livree (PR #16375 c.629) ; l'acceptance §2 (Apply
jonctions) a ete livree par tierce partie ; l'acceptance §3 (anti-regression
HARD) et §4 (mesure espace) restent dues — pas de trace d'un run `lake build`
post-Apply par la lane qui a execute l'Apply.

### Recommandations

1. **Identifier l'auteur de l'Apply 14/09** : `git reflog` du store, logs
d'execution du script, ou recherche PR mergée entre 13/09 et 14/09 touchant
`setup_shared_mathlib.ps1` ou `share-state.json`. Sans cela, l'attribution
reste floue.

2. **Verifier l'anti-regression §3** : pour chacune des 9 lanes jonctionnees,
`lake build SUCCESS` post-Apply et `count_code_sorry.py --json` →
`distinct_code_sorry` inchange. C'est un test qui n'a pas ete documente
comme execute.

3. **Clore le claim #16034** : la livraison a ete faite par tierce partie,
la valeur ajout de cette lane est desormais la **documentation** (ce
rapport) et le **suivi** de l'anti-regression §3.

4. **Delta restant** : seul `search_lean` reste candidat Apply (6.9 Go, risque
faible). Le rapport V2 §Conclusion search_lean documente la faisabilite.

### Datation alternative (si `share-state.json` n'etait pas autoritatif)

Les sources secondaires (toutes rapportees par V2) ne permettent pas de dater
precisement : la jonction elle-meme n'ecrit pas de log (cf c.1059 V1 narrow
note Portee). L'absence de poses manuelles documentees sur po-2027 (vs 4
documentees sur po-2024 par PR #15972) accroit la probabilite que toutes les 9
aient ete posees par l'Apply 14/09 — `share-state.json` est la source de verite.
Loading