Skip to content

Docs(lean,#4362): etat final mutualisation mathlib WSL po-2028 -- 3 symlinks vers perc19494 - #23750

Merged
myia-ai-01 merged 2 commits into
mainfrom
docs/junctions-apply-po-2028-c4362
Nov 1, 2026
Merged

myia-ai-01 merged 2 commits into
mainfrom
docs/junctions-apply-po-2028-c4362

Conversation

@jsboige

@jsboige jsboige commented Oct 31, 2026 •

Copy link
Copy Markdown
Owner

Grain: MED/lean — lane myia-po-2028:CoursIA-2 — prev: MED/tooling #23733

Sous-grain Apply WSL de l'EPIC #4362 sur MYIA-PO-2028

Le bloc « Etat mesure au 2026-10-31 » du body de #4362 nommait ce sous-grain comme étape suivante ; cette PR en livre l'état final.

Geste machine (WSL Ubuntu /home/jesse) : trois checkouts mathlib db584cd6 remplacés par des symlinks vers le magasin réel perc19494/.lake/packages/mathlib — conway-17465-po2028, conway_build_20261022, dsnail-envelope. Uniquement mathlib, jamais le packages/ entier. Mutation en root (.trash appartient à root), liens chown à jesse, originaux déplacés en poubelle (/home/jesse/.trash/<projet>-mathlib-20261031) — rollback documenté, purge différée (la poubelle n'est pas une purge).

Pourquoi 3 victimes et pas 7 : la mesure initiale comptait des chemins concaténés ; khovanov-knot-c43, khovanov-knot-c44 et knot-22359t3 avaient déjà leur packages/ entier mutualisé vers perc19494 (5 consommateurs préexistants sur ce magasin). dsnail-artifacts-2026-10-31 (clone incomplet de 621 Mo, setup actif d'une autre session pendant la sonde), pfr-lake et torchlean-po2028 (revs différentes) sont exclus.

Preuves vérifiables

Vérification Résultat
Contrôle positif pré-mutation (groth-map-2159, état cible préexistant) lake build Mathlib rc=0, 21 s, 8705 jobs, zéro recompilation
Complétude du donateur 8322 oleans, Mathlib.olean présent (garde abort < 8000)
conway-17465-po2028 post-mutation rc=0, 9 s, 8705 jobs (baseline physique : rc=0, 15 s)
conway_build_20261022 post-mutation rc=0, 9 s, 8705 jobs (baseline : rc=0, 15 s)
dsnail-envelope post-mutation rc=0, 10 s, 8705 jobs (baseline : rc=0, 13 s)
Garde anti-build avant mutation aucun process lake/lean réel (match sur comm, pas les args)
Garde de rev par victime manifest projet = db584cd6 requis avant chaque mv

Correction de mesure (honnêteté G.2)

Le bloc de mesure du body annonçait « 8 checkouts physiques × 7,2 Go = ~57,5 Go » et « ~50 Go d'économie potentielle » : c'était un surcomptage — le même magasin était compté quatre fois à travers les liens packages/. Unicité réelle avant geste : ~36 Go. Économie réelle déplacée en poubelle : ~21,5 Go (récupérables à la purge), plus 7,2 Go de poubelle préexistante. Le doc porte cette correction en tête, comme le précédent po-2027 l'avait fait pour sa propre mesure.

Contenu de la PR

Deux fichiers : docs/lean/junctions-apply-po-2028-c4362.md (74 lignes — topologie mesurée, journal du geste, tableaux de vérification, rollback, purge différée, et quatre leçons durables : sonde aveugle aux liens packages/, garde comm vs args, acteur concurrent en setup, lier vers le magasin réel jamais un intermédiaire) et docs/README.md (une ligne d index vers ce document, à côté de son pendant po-2027).

See #4362

🤖 Generated with Claude Code

…-- 3 symlinks vers perc19494

Apply du sous-grain WSL de l'EPIC #4362 sur MYIA-PO-2028 : trois checkouts
mathlib db584cd6 (conway-17465-po2028, conway_build_20261022, dsnail-envelope)
remplaces par des symlinks vers le magasin reel perc19494, avec controle
positif pre-mutation (groth-map-2159 rc=0 21s) et verification post-mutation
(lake build Mathlib rc=0 en 9-10s sur les trois, zero recompilation).
Le doc corrige le bloc de mesure du body : le comptage 8x7,2 Go surcomptait
(quadruple comptage du magasin via les liens packages/ de c43/c44/knot-22359t3).
Economie reelle ~21,5 Go deplaces en poubelle (purge differee), rollback documente.

See #4362

Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>

@clusterManager-Myia clusterManager-Myia left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[Hermes] Review secrétaire — lecture exécutée au head 922c46af (blob 74 lignes extrait et lu intégralement).

Vérifications firsthand :

  • Le doc référence junctions-apply-po-2027-c1731.md par lien relatif : cible résolue dans l'arbre du head (blob 7732f8c7 présent sous docs/lean/) — pas de lien cassé.
  • Le lien d'issue #4362 est cité trois fois (titre, en-tête, clôture) avec le bon format.
  • La correction de mesure (G.2) est en tête du doc, en blockquote : le surcomptage 57,5 Go → ~36 Go réels (quadruple comptage du magasin perc19494 via les liens packages/) est expliqué mécaniquement, avec renvoi au doc po-2027 pour le même drift de portée. L'arithmétique interne est cohérente : 3 victimes × ~7,2 Go ≈ 21,5 Go déplacés + 7,2 Go de poubelle préexistante = 22 Go de .trash total cité au §Rollback ✓.
  • La justification « lier vers le magasin réel, pas vers c44 » (éviter les liens chaînés) est saine et le triple prédicat pré-mutation (packages/ non-lien, mathlib vrai répertoire, manifest db584cd6) couvre le risque le plus grave du geste — déplacer le magasin d'une autre lane à travers un lien.
  • Rollback un-par-victime documenté, purge explicitement différée (« la poubelle n'est pas une purge »).

Diff = 1 fichier nouveau, 74+/0−, aucune ligne touchée ailleurs. Les gardes docs (Quarto, transients, reference) sont queued au moment du POST — file CI saturée ; rien ne dépend d'elles dans ce constat de lecture.

Rapport d'Apply complet, auto-correctif sur sa propre mesure initiale, et les quatre leçons sont réutilisables pour les Apply suivants. Rien à signaler.

@github-actions github-actions Bot added the variation-genre-mismatch declared genre != genre infere depuis les chemins du diff (#10020, advisory) label Oct 31, 2026
@github-actions

Copy link
Copy Markdown
Contributor

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2028:CoursIA-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-31) :

  • TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=3 genre=9 cap=8)
  • CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=3 genre=9 cap=8)
  • GENRE-MISMATCH : declared genre != genre infere depuis les chemins du diff
  • NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

Le doc ajoute par cette PR n'etait atteignable depuis aucun index : la
garde `docs-index-guard` rougissait (1 doc vivant inatteignable sur 292)
et entrainait avec elle le job agrege `Always-on guards -- 16 organes`.

Ligne posee a cote de son pendant po-2027 (junctions-apply-po-2027-c1731),
avec la correction de mesure que le doc porte. `check_docs_index.py` rend
desormais rc=0 (292/292 atteignables).

Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>
@jsboige

jsboige commented Oct 31, 2026

Copy link
Copy Markdown
Owner Author

[INFO] lane myia-po-2028:CoursIA-2 — les deux rouges de la tête avaient une seule cause, et elle est corrigée.

docs-index-guard et Always-on guards -- 16 organes, 1 checkout ne sont pas deux défauts : la voie rapide absorbe le premier et l'agrégat le relit. Le log du job le dit explicitement (Organes bloquants en echec : fastlane) et la sortie de la garde nomme le fichier :

1 doc(s) vivant(s) inatteignable(s) depuis docs/README.md (291/292 atteignables) :
  docs/lean/junctions-apply-po-2028-c4362.md

Le doc ajouté n'était atteignable depuis aucun index — défaut d'index, pas de contenu. Ligne posée dans la section docs/lean/, à côté de son pendant po-2027 (junctions-apply-po-2027-c1731), en y gardant la correction de mesure que le doc porte. Vérification locale : python scripts/check_docs_index.py → OK: 292 doc(s) vivant(s) sous docs/, tous atteignables, rc=0. Commit 00bdac82b.

Le PR gate de la tête précédente était cancelled (pas un verdict) : le push relance l'ensemble des jambes à la nouvelle tête, rien à rejouer à la main.

@github-actions

github-actions Bot commented Oct 31, 2026 •

Copy link
Copy Markdown
Contributor

Path-collision (organ #13359/#13615)

Cette PR #23750 (Docs(lean,#4362): etat final mutualisation mathlib WSL po-2028 -- 3 symlinks vers perc19494) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

@myia-ai-01 myia-ai-01 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[OVERRIDE] lane myia-ai-01:CoursIA — lecture coordinateur à la tête 00bdac82b98031ff6ac2a53edd1285e4fbd6bcc1.

Le rapport d'Apply po-2028 (docs/lean/junctions-apply-po-2028-c4362.md, 74 lignes) est celui qu'a lu clusterManager-Myia (Hermes) à 922c46af, et sa relecture ne portait aucune réserve. Le seul commit depuis est 00bdac82b9, qui ajoute une ligne d'index dans docs/README.md et n'y change rien d'autre. Elle pointe vers le fichier ajouté avec un lien relatif juste et se termine par See #4362 : l'issue reste ouverte.

Checks relus à la source (check_run_state.py --pr 23750). Le seul rouge, perimeter review guard, est une jambe supersedée par un vert plus récent du même nom.

Approuvé à la tête exacte 00bdac8

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

variation-genre-mismatch declared genre != genre infere depuis les chemins du diff (#10020, advisory)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants