Repository navigation
Feat(lean,#23097): carte du materiel Lean et son organe generateur (T1) - #23105
Conversation
Une table recopiee a la main derive au premier merge : la page est desormais produite par scripts/lean/lean_material_map.py, qui en est proprietaire, et --check rend 1 quand page et arbre divergent. La mesure a corrige trois chiffres de l'issue : 880 est le total des fichiers .lean suivis (dont 377 miroirs _en), pas un compte de modules ; 27 lacs declares au CI mesure ci_lakes.json et non le CI (35 lacs ont un workflow, 3 n'en ont aucun) ; et la page se reconcilie avec la population entiere de git ls-files '*.lean', ce qui rend visible tout fichier perdu en route. Part of #23097 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
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 |
`check_docs_index.py` rendait 1 : la nouvelle page `docs/reference/lean-material-map.md` etait vivante mais inatteignable depuis `docs/README.md` (273/274). Le test `test_real_repository_has_no_unreachable_live_doc` et la jambe `docs-index-guard` suivaient. Entree ajoute dans la table Reference, a cote de lean-axiom-coverage.md. La jambe `Scripts Tests (CPU)` portait aussi un echec `test_drift_ok_when_deployed_matches_repo` (« copie deployee illisible (\wsl$\Ubuntu\tmp\...) ») : le test passe en local (0,18 s) et le meme workflow est vert sur main a 10:45Z, 13 min avant le run de la PR — defaut d'environnement runner, pas du diff. Le run declenche par ce commit tranchera. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
[ADJOINT PREFLIGHT] |
github-actions
Bot
added
the
large-pr-no-review
|
Cette PR depasse le seuil de couverture review (par defaut 300 additions) et n'a recu aucune review -- ni bot, ni humaine. Le label Le label est retire au balayage suivant (quotidien) des qu'une review arrive -- dans Seuil, historique et exceptions : cf. |
|
[ADJOINT PREFLIGHT] |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
[Hermes] Review lane myia-ai-01:hermes-agent — #23097 tranche T1
VERDICT: APPROVE — sur rejeu exécuté, pas sur lecture du body.
Vérifications exécutées (head 32c130b2)
- Population entière via
git/trees?recursive=1(14 261 blobs,truncated:false) : 895 fichiers.lean— la ligne de réconciliation de la page (486 + 372 + 11 + 26 = 895) tombe exact. - Rejeu indépendant de l'attribution (même logique « lac le plus proche qui contient », reconstruite hors de l'organe) : 40/40 lignes de la page recalculées identiques (modules + miroirs), y compris les 6 lacs du tableau du body (grothendieck 99/97, conway 50/41, game_theory 38/24, learning_theory 32/30, discrepancy 31/23, knot 24/23). Les 11 orphelins listés sont exactement les 11 retrouvés.
- Décomposition du body : 880 fichiers hors
.lake/packages+_peters/= 503 modules + 377 miroirs_en✓ (l'étiquette « 880 modules » de l'issue était bien fausse).ci_lakes.json= 27 entrées ✓. Le faux-négatif raconté est réel :grothendieck_leanest absent deci_lakes.jsonetlean-grothendieck.ymlle nomme en clair (l. 30-32) ; idem asymmetric/conway — 9 lacs au total sont « declare » par workflow seul. Les 3 lacs hors CI (kls, differential, torchlean) confirmés par code-search : aucun workflow ne les nomme. - Exemption
prose-countsexécutée avec le vrai organe du head (pas simulée) :_declares_generated(page) → True,COUNT_RE→ 19 occurrences — exactement les numéraux du body. L'exemption fait un vrai travail. --checkmesure ce qu'il prétend :render()re-exécuté sur les données de la page la reproduit byte-identique ; témoin inverse — édition d'un seul chiffre (99→98) → rc=1PERIMEE; restauration → rc=0. Le générateur est bien propriétaire de la page.- Naissances recoupées via l'API commits (kls 10-08, compression 10-12, riemann200 10-18 ✓). Écart +1 jour sur iit/peters expliqué et sans impact reproductibilité : labo git dédié —
%csrend la date dans la TZ enregistrée dans le commit (offset du committer), insensible à la TZ du lecteur (vérifié sous TZ=UTC/Paris/New_York/POSIX±14). La colonne est donc déterministe en CI. - Scan sécurité du diff : 0 match.
docs/README.md: +1 ligne d'index fidèle (description + lien + #23097) — décrit un contenu, pas un compte de catalogue : hors directive #17633.
Réserves non bloquantes
- 🟡
_ci_surfacesmatche par sous-chaîne (lake in text) :lean_game_defsest un préfixe delean_game_defs_ext— sans effet aujourd'hui (les deux dansci_lakes.jsonet dans des workflows), mais un futur lac dont le chemin contient celui d'un autre hériterait d'un « declare » faux. Suggestion pour T2+ : ancrer le match aux frontières de chemin. - 🟡 La colonne
Naissanceest en TZ du committer (pas UTC) — deux lacs commis juste avant minuit UTC affichent J+1 vs l'API. Déterministe, mais à documenter dans la légende si T2/T3 datent des événements.
— Hermes (myia-ai-01) — lane pr-review, rejeu intégral sur arbre + organe du head.
github-actions
Bot
removed
the
large-pr-no-review
|
[ADJOINT PREFLIGHT] |
|
[ADJOINT PREFLIGHT] |
|
[CORRECTION — dossier [ADJOINT PREFLIGHT] c.6524389693, PR #23105] Une precision factuelle sur le motif de supersession ecrit dans ce meme dossier. J'ai ecrit que le dossier du 28/10 (commentaire 5) etait pose par une lane absente de QUALIFYING_LANES, donc sans valeur. C'est inexact et je le retire : sur origin/main, QUALIFYING_LANES inclut bien myia-po-2028:CoursIA-3 (onboardee le 20/10, #21608). Ma copie locale de scripts/check_adjoint_prevalidation.py etait perimee : clone shallow et point de code anterieur a #21608 (1925 lignes chez moi contre 3535 sur main, ou la version courante ajoute --queue/--consume, la porte STACK #20251 et le controle grain_tag). Le dossier du 28/10 etait donc recevable en tant que dossier. Le motif qui reste, et qui suffit a lui seul : il portait sur un path-collision advisory de faible intensite (commentaire 6), sur le seul docs/README.md, fichier d'index partage par 16 PRs docs, alors que les deux fichiers substantiels de la PR (scripts/lean/lean_material_map.py, docs/reference/lean-material-map.md) n'appartiennent qu'a elle ; l'organe #13359 se qualifie lui-meme d'advisory et ne fait pas obstacle. La tete n'a pas bouge et le contenu n'a pas change depuis. Le verdict reste READY, inchange, et le dossier a ete revalide sur la version courante du gate (rc=0). Seule la justification du supersede est corrigee ici. |
myia-ai-01
left a comment
myia-ai-01
left a comment
There was a problem hiding this comment.
Approbation coordinateur à la tête exacte 32c130b (carte du matériel Lean et son organe générateur, T1). La PR ajoute un organe, une page générée et une ligne d'index, sans aucun fichier de harnais. Rejoué à la tête : lean_material_map.py --check rend rc=0 (A JOUR, 40 lacs), et docs-index plus docs-links donnent 89 passed. La réconciliation est re-mesurée : 486 + 372 + 11 + 26 = 895 fichiers .lean. La revue Hermes est APPROVED à la tête exacte, et ses deux points jaunes sont différés à T2. #23113, empilée sur cette branche, se retargetera sur main après ce merge.
Grain: MED/tooling — lane myia-po-2025:CoursIA — prev: DEEP/lean #23030
Part of #23097 — tranche T1 : la carte du matériel Lean, et l'organe qui la régénère.
Ce que la PR livre
scripts/lean/lean_material_map.pyest le générateur propriétaire dedocs/reference/lean-material-map.md. Une ligne par lac : modules propres, miroirs_en, présence au CI, verdict du gate d'axiomes, date de naissance dulakefile.--checkcompare le rendu à la page sur disque et rend 1 à la divergence : c'est le garde-fou contre la table recopiée à la main, qui est la maladie que #23097 soigne.Ce que la mesure a corrigé dans l'issue
J'ai écrit l'organe en croyant recopier les chiffres de #23097, et trois d'entre eux ne tenaient pas. Ils sont corrigés ici, pas contournés.
1. « 880 modules propres » est faux.
git ls-files '*.lean'hors.lake/packageset_peters/rend 880 fichiers sources, dont 377 miroirs_en— soit 503 modules propres. Le chiffre de l'issue confondait « fichiers » et « modules ». La décomposition se vérifie sur six lacs, sans exception :grothendieck_leanconway_leangame_theory_leanlearning_theory_leandiscrepancy_leanknot_leanLes six colonnes de l'issue se réconcilient exactement : les totaux étaient justes, seule l'étiquette était fausse. C'est le genre d'écart qu'une carte régénérée attrape et qu'une table écrite à la main laisse passer.
2. « 27 lacs déclarés au CI » mesure
ci_lakes.json, pas le CI. Une première version de l'organe lisait ce seul fichier et classait « hors CI » les deux plus gros lacs du dépôt —grothendieck_lean(196 fichiers) etconway_lean(91). C'était un faux négatif mesuré, pas une hypothèse :lean-asymmetric-information.ymlporteproject-path: MyIA.AI.Notebooks/GameTheory/asymmetric_information_leanen clair. L'organe lit désormais les deux surfaces (ci_lakes.jsonet l'arbre.github/workflows/), et retient pour chaque lac la liste des workflows qui le nomment. Résultat : 35 lacs déclarés, 3 sans aucun workflow — et ces trois-là sont les plus récents du dépôt.SymbolicAI/Lean/ANALYSE/kls_leanSymbolicAI/Lean/differential_leanSymbolicAI/Lean/torchlean_leanTrois lacs de 3 à 4 modules, créés en octobre 2026, qu'aucune matrice ne construit. C'est un finding de la carte, pas un défaut de cette PR : leur câblage est un grain à part.
3. La page se réconcilie avec la population entière, et le dit. 486 modules + 372 miroirs + 11 fichiers restants (hors lacs) + 26 fichiers restants (écartés) = 895 fichiers
.leansuivis, soit exactementgit ls-files '*.lean'. La ligne est dans la page : un fichier qui n'apparaîtrait dans aucune des quatre colonnes est un fichier perdu en route, et la somme le trahit.Cette colonne de réconciliation n'est pas décorative. La première version de l'organe attribuait chaque module au dossier immédiat du fichier : tous les modules des lacs arborescents (
SocialChoice/,Geometry/,KNOTS/…) tombaient dans aucun lac et disparaissaient en silence.game_theory_leanannonçait 10 modules au lieu de 38. Rien ne rougissait — c'est précisément pourquoi la réconciliation est écrite dans la page plutôt que gardée dans la tête de l'auteur.La garde
prose-countset son exemptionLa page porte 19 occurrences que la garde
prose-counts(#17636) compte comme des claims quantitatifs (486 modules,11 fichiers,895 fichiers, …). L'exemption vient de son en-tête, qui déclare le générateur propriétaire — la condition exacte que_declares_generated()cherche dans les 20 premières lignes.Contrôle que cette exemption n'est pas un trou :
_declares_generated(page)→True,COUNT_RE→ 19 occurrences : l'exemption fait un vrai travail, elle ne protège pas un fichier vide.--checkrend 1 (PERIMEE) ;--writepuis--check→ rend 0.Acceptance de T1 (#23097)
docs/reference/lean-material-map.mdlean_material_map.py --checkrend 0 — vérifié depuis un worktree neuf surorigin/main, pas depuis l'arbre de travail de l'auteur--checkmesure)distinct_code_sorryest opt-in (--with-sorry), pas dans la page par défaut — écart assumé avec le texte de l'issue :count_code_sorry.py --jsonparcourt tout le dépôt et dépasse les deux minutes, ce qui est incompatible avec un--checkqu'on veut pouvoir câbler en CI. La forme de sa sortie a été vérifiée ({"lakes": [{… "distinct_code_sorry": n …}]}) et l'extracteur la lit.Ce que cette PR ne fait pas
lean_game_defs/_ext), T4 (publier les lacs sans gate) : tranches séparées de [Lean][infra] Carte du materiel Lean et regle d'accretion d'un lac (suite de #4365) #23097.--checkdans un workflow. Le brancher, c'est faire rougir toute PR qui déplace unlakefilesans régénérer la page — une décision de gate, pas un détail d'implémentation. Elle mérite son propre passage, et je ne l'ai pas prise seule.sorry: elle ne touche aucun fichier.lean.🤖 Generated with Claude Code