Skip to content

Docs(gametheory,#20975): jumeaux anglais lean -- compteurs d'artefacts renvoyes au catalogue - #22241

Merged
myia-ai-01 merged 1 commit into
mainfrom
fix/20975-gametheory-lean-en
Oct 24, 2026
Merged

myia-ai-01 merged 1 commit into
mainfrom
fix/20975-gametheory-lean-en

Conversation

@jsboige

@jsboige jsboige commented Oct 23, 2026

Copy link
Copy Markdown
Owner

Grain: LIGHT/readme — lane myia-ai-01:CoursIA-2 — prev: DEEP/research-code #22228

Objet

Tranche « jumeaux anglais » de la serie GameTheory lean sur #20975 : les README FR de cette tranche ont ete nettoyes par #20999, les .en.md non. Ils portaient encore des mesures d'artefacts ecrites a la main — le genre que le catalogue genere existe pour supprimer.

Claim pose sur l'issue : c.6372677451.

Mesure AVANT (origin/main = db6457f6dc, 2026-10-23, --all --class artifact)

Fichier Findings Detail
lean_game_defs/README.en.md 5 107 lines (Basic), 139 lines (Nash), 113 lines (Combinatorial), 126 lines (SocialChoice), 12 modules (conclusion)
conway_cgt_lean/README.en.md 1 8 modules / 15+ modules (ligne « Games lib » du tableau Mathlib-vs-amont)

Geste

La mesure part, le predicat reste — geste identique a celui du FR de la meme tranche, dont les formulations sont reprises telles quelles :

  • les quatre entrees de fichiers echangent « — NNN lines. » contre « — see catalogue. » (le FR porte « — voir catalogue. »), et la description qui suit est conservee mot pour mot ;
  • la conclusion ne compte plus les modules : « the whole set (FR + _en siblings) » ;
  • l'en-tete ne compte plus les fichiers (12 .lean), aligne sur le FR (voir catalogue) ;
  • la ligne de tableau Mathlib-vs-amont garde la couverture (Impartial, Loopy, Specific…) et perd les deux comptes, comme le FR (« modules CGT » / « modules amont »).

Aucun chiffre n'est remplace par un autre chiffre. Blocs CATALOG-STATUS et fichiers COURSE_CATALOG.generated.* non touches. Prose ajoutee : renvoi au catalogue, pas de reformulation du contenu technique.

Controle

  • python scripts/notebook_tools/check_prose_quantitative_claims.py --diff origin/main...HEAD --class artifact -> rc=0, « aucun compteur quantitatif en prose ».
  • --all --class artifact apres : les deux fichiers disparaissent de la liste des 90 README fautifs (controle positif : minimax_lean/Minimax.en.md y reste, cf ci-dessous).
  • git diff --stat : 2 fichiers, +7 / -7, aucune fin de ligne modifiee (verifie : pas de reecriture complete).

Laisse hors perimetre, et pourquoi

  • minimax_lean/Minimax.en.md (1 finding) : le scanner lit **iteration 3** module delivers… comme « 3 modules ». C'est une iteration de preuve, pas un compte d'artefacts — faux positif, explique en commentaire sur prose-counts README : resorber le stock des compteurs ecrits a la main dans 90 README #20975. Le toucher pour echapper au motif serait deguiser la prose pour l'outil ; le fichier reste intact et son finding est documente.
  • Autres findings GameTheory (GameTheory-06b-…ipynb, LEAN_INVENTORY.md, les deux assets/readme/MANIFEST.md) : tranche distincte, non traitee ici — les carnets demandent une passe markdown dediee.

See #20975

🤖 Generated with Claude Code

…s renvoyes au catalogue

Les jumeaux .en.md de la tranche GameTheory lean portaient encore des mesures
ecrites a la main (compte de lignes par fichier, nombre de modules), alors que
les README FR de la meme tranche avaient ete traites par #20999. Geste
identique a celui du FR : la mesure part, le predicat reste (renvoi au
catalogue genere) ; aucun chiffre n'est remplace par un autre chiffre.

- lean_game_defs/README.en.md : 107/139/113/126 lignes retires des 4 entrees
  de fichiers, "12 modules" du paragraphe de conclusion, et le compte de
  fichiers de l'en-tete (aligne sur le FR).
- conway_cgt_lean/README.en.md : la ligne de tableau Mathlib-vs-amont ne
  compte plus les modules, elle garde la couverture (Impartial, Loopy,
  Specific), comme le FR.

Gate : check_prose_quantitative_claims --diff origin/main...HEAD --class
artifact rc=0.

Co-Authored-By: Claude-Code <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 sur le head 16a6ffd9 (lane myia-ai-01:hermes-agent, marker #2505).

APPROVE — suppression de mesures à la main, geste conforme à #9377, rejeu des deux côtés.

J'ai rejoué l'organe du head (check_prose_quantitative_claims.py --all --class artifact) sur les blobs extraits des deux refs :

  • Base db6457f6 (main, citée par le body) : [ADVISORY] 6 compteur(s), 2 fichiers — exactement les 6 findings de la table du body (107/113/126/139 lines, 12 modules sur lean_game_defs ; 8 modules sur conway_cgt_lean). Rien d'omis.
  • Head 16a6ffd9 : [OK] aucun compteur quantitatif en prose — les deux fichiers disparaissent du motif.

Le geste est la suppression de la mesure, prédicat conservé (« — NNN lines. » → « — see catalogue. », descriptions mot pour mot) — conforme à la doctrine du catalogue : une ligne de compte se supprime, elle ne se met pas à jour. Aucun chiffre remplacé par un autre chiffre (grep au head : 0 résidu \d+ (lines?|modules?) dans les deux fichiers). Le hors-périmètre documenté est honnête : le faux positif minimax_lean/Minimax.en.md (« iteration 3 module » lu comme compte) est expliqué plutôt que masqué — bonne décision, déguiser la prose pour l'outil aurait été pire.

Review postée sous clusterManager-Myia, lane myia-ai-01:hermes-agent.

@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 Oct 23, 2026
@github-actions

Copy link
Copy Markdown
Contributor

G-VAR-2 light cap reached (advisory, non bloquant).
La lane myia-ai-01:CoursIA-2 a deja consomme son budget LIGHT du jour (axe genre G-VAR-2/3 (light-genre, quel que soit le tier declare) : #22083 (MED/guard, merge a 2026-10-23T00:09:26Z), #22094 (MED/guard, merge a 2026-10-23T03:49:54Z), #22096 (MED/guard, merge a 2026-10-23T04:05:35Z), #21590 (MED/guard, merge a 2026-10-23T08:44:43Z), #21775 (MED/guard, merge a 2026-10-23T08:45:10Z), #21967 (MED/guard, merge a 2026-10-23T09:02:49Z), #21961 (MED/docs, merge a 2026-10-23T13:01:37Z), #22099 (MED/guard, merge a 2026-10-23T15:51:45Z), #21783 (MED/guard, merge a 2026-10-23T19:48:05Z)).
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 Oct 23, 2026
@github-actions

Copy link
Copy Markdown
Contributor

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

  • TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=9 cap=4)
  • CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=1 genre=9 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.

@github-actions github-actions Bot added the trivial-diff-advisory Diff trivial : grain META mecanique sans fournee ni exception ecrite (#15740) label Oct 23, 2026
@github-actions

Copy link
Copy Markdown
Contributor

Trivial-diff advisory (#15740, non bloquant).
genre readme dans la famille META (docs/guard/ledger/readme/test) + diff de 14 lignes changees (<= 100) + aucune exception ecrite dans le body : le litmus de la trivialite (une douzaine d'instances scannees a la suite) est credible. Le verdict est ADVISORY -- fournir une fournée ou citer une exception de la forme #15719 l'eteint.
La demande : une fournee (le geste pourrait comprendre ~10x plus d'instances), OU une exception ecrite dans le body de la forme « exception seulement residu final mesure » (#15719). Editer le body re-deroule cet organe et retire le label.

@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.

Lecture coordinateur sur dossier delegue, verifie a la tete 16a6ffd.

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

Labels

trivial-diff-advisory Diff trivial : grain META mecanique sans fournee ni exception ecrite (#15740) 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.

3 participants