Skip to content

docs(lean,#15568): borner la portee du scan junctions au worktree + table 5 machines - #15577

Merged
jsboige merged 1 commit into
mainfrom
docs/15568-junctions-scan-scope
Sep 11, 2026
Merged

jsboige merged 1 commit into
mainfrom
docs/15568-junctions-scan-scope

Conversation

@jsboige

@jsboige jsboige commented Sep 11, 2026

Copy link
Copy Markdown
Owner

Grain: MED/docs — lane myia-po-2026:CoursIA — prev: MED/tooling #15557

Closes #15568

Les deux imprécisions, et ce qui a été fait

Le préflight adjoint de #15507 a relevé deux défauts de portée dans docs/lean/junctions-scan-po-2027.md. Aucun chiffre du rapport n'est en cause : les 27 lacs, les 7 groupes manifest-identity, les 0 checkouts et les 0 jonctions restent valides tels quels (acceptance 3 — aucune re-mesure).

1. Une mesure de worktree écrite comme une mesure de machine

Le Scan opère depuis le repo-root courant : il ne voit que ce worktree-là. Le document en tirait pourtant trois énoncés au niveau machine — le verdict « machine po-2027 = réservoir identifié », « aucun des 27 lacs n'a exécuté lake update sur po-2027 », « la machine porte les manifests mais pas les build artifacts ».

Le précédent c.857 (#14296) a montré qu'un checkout Mathlib logé dans un autre worktree échappe à la mesure : c'est exactement le faux négatif qu'un prédicat d'absence doit exclure avant de s'énoncer au niveau machine.

Retenu : branche 1 de l'acceptance (borner, coût nul). Le rapport ne consigne pas le git worktree list de po-2027 ; rien en lui ne soutient une formulation machine-wide, et rejouer le Scan dans chaque worktree exigerait un accès à la machine. Les formulations sont donc bornées au worktree scanné, avec un encadré « Portée » qui nomme la limite et la voie qui la lèverait.

2. Une table « multi-machine » qui choisissait son dénominateur

La table comparait trois colonnes puis concluait « la conclusion est homogène sur les 3 machines scannées ». La phrase était déclarée (« les 3 machines scannées »), donc pas fausse — mais le document cite lui-même deux mesures qu'il excluait de la table : po-2023 (#15070, 0,64 Go) et po-2024 (#14296, 24 lacs). Un lecteur qui s'arrête à la table lit une conclusion de flotte tirée d'un échantillon dont la machine la plus intéressante a été retirée.

Retenu : branche 1 de l'acceptance (compléter). po-2023 et po-2024 sont désormais des colonnes, et la phrase de conclusion nomme les cinq machines mesurées.

Colonne Source Checkouts Empreinte Économie
po-2023 #15070 (Scan 2026-09-07) 3 1,28 Go 0,64 Go
po-2024 #14296 / cluster-junctions-c857.md (Scan 2026-09-02) 0 0 Go 0 Go

Les chiffres sont repris tels quels des rapports de leurs lanes, sans re-mesure — un encadré « Provenance » le dit, et rappelle que ces deux mesures partagent la même borne de portée (mesure de worktree, pas de machine).

Effet sur la conclusion, honnêtement

Elle change de forme sans changer de fond : le réservoir reste large et l'amorçage quasi nul sur les cinq machines. Ce qui devient visible, c'est la seule valeur non nulle du plateau — po-2023, 0,64 Go — et la raison pour laquelle elle n'a pas été exploitée (l'économie marginale ne justifiait pas un Apply irréversible). Avant, cette exception était hors table ; elle y est maintenant, avec sa justification.

Périmètre

  • docs/lean/junctions-scan-po-2027.md — +17/−11, 1 fichier.
  • Aucune re-mesure, aucun lake build, aucun grep -c sorry.
  • Garde paragraphes : detect_paragraph_length.py → clean.
  • Part of #13962 (l'EPIC reste ouverte — l'Apply est à ai-01, pas ici).

Acceptance de #15568

Point État
Formulations machine-wide bornées au worktree ou Scan rejoué dans tous les worktrees bornées (branche 1), avec la limite nommée
Table porte po-2023 (#15070) et po-2024 (#14296) ou la conclusion nomme les exclusions colonnes ajoutées (branche 1) + conclusion nommant les 5 machines
Aucune re-mesure des 27 lacs respectée

…able 5 machines

Deux imprecisions de portee relevees au merge-gate de #15507. Aucun chiffre
du rapport n'est en cause : les 27 lacs, les 7 groupes manifest-identity,
les 0 checkouts et les 0 jonctions restent valides tels quels (acceptance 3).

1. Le Scan opere depuis le repo-root courant : il ne voit que ce worktree.
   Les enonces machine-wide ("Aucun des 27 lacs n'a execute lake update sur
   po-2027", "machine po-2027 = reservoir identifie") sont bornes au worktree
   scanne, avec le precedent mesure c.857 (#14296) ou un checkout loge dans un
   autre worktree echappe a la mesure. Le rapport ne consigne pas le
   git worktree list de po-2027 : rien n'y soutenait une formulation machine.

2. La table multi-machine concluait sur 3 colonnes en excluant deux mesures
   que le document cite lui-meme. Ajout de po-2023 (#15070) et po-2024
   (#14296, c.857) ; la phrase de conclusion nomme desormais les 5 machines
   mesurees et pointe la seule valeur non nulle (po-2023, 0,64 Go).

Chiffres des colonnes ajoutees repris tels quels des rapports de leurs lanes,
sans re-mesure. 1 fichier, +17/-11.

Closes #15568
Part of #13962

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@github-actions github-actions Bot added the variation-light-cap-reached Lane ayant deja merge une LIGHT aujourd'hui (cap G-VAR-2 atteint) label Sep 11, 2026
@github-actions

Copy link
Copy Markdown
Contributor

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-po-2026:CoursIA a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #15384 (MED/guard, merge a 2026-09-11T00:50:53Z), #15362 (MED/guard, merge a 2026-09-11T02:52:15Z), #15502 (LIGHT/readme, merge a 2026-09-11T04:17:52Z), #15458 (MED/docs, merge a 2026-09-11T08:36:44Z), #15459 (MED/docs, merge a 2026-09-11T08:36:52Z), #15555 (LIGHT/notebook, merge a 2026-09-11T08:40:18Z), #15550 (LIGHT/readme, merge a 2026-09-11T09:08:20Z)).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour,
toutes categories LIGHT confondues
(guard, doc, refs, ... partagent un seul budget) :
c'est un RATIO, pas un plafond plat. La decision de merge reste au coordinateur.

@github-actions github-actions Bot added variation-tier-inflation declared LIGHT << effective LIGHT-genre (#10020, advisory) variation-genre-cap-exceeded light_genre > cap partage G-VAR-2 (#10020, advisory) labels Sep 11, 2026
@github-actions

Copy link
Copy Markdown
Contributor

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

  • TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=3 genre=7 cap=4)
  • CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=3 genre=7 cap=4)

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.

@jsboige
jsboige merged commit d14b1ac into main Sep 11, 2026
20 of 21 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

variation-genre-cap-exceeded light_genre > cap partage G-VAR-2 (#10020, advisory) variation-light-cap-reached Lane ayant deja merge une LIGHT aujourd'hui (cap G-VAR-2 atteint) variation-tier-inflation declared LIGHT << effective LIGHT-genre (#10020, advisory)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

docs(lean,#13962): borner la portee du scan junctions po-2027 (worktree vs machine) et completer la table multi-machine

1 participant