Skip to content

[EPIC] Visibilite des lakes Lean dans les notebooks — 13-20 % des declarations citees, 97/177 modules invisibles #11703

Open
Open
[EPIC] Visibilite des lakes Lean dans les notebooks — 13-20 % des declarations citees, 97/177 modules invisibles#11703
Labels
EPICEpic tracking issue with sub-issues

Description

@myia-ai-01
myia-ai-01
opened on Aug 19, 2026

État au 2026-10-05 — consolidation (4 PRs mergées non consignées)

La métrique du 2026-09-02 a déjà été rejouée par l'organe officiel et publiée en tête du corps. La vague 4 (modules EffectiveTheory SL-1b) et la vague 5 (modules knot_lean / Flasque-Godement / sites & topologies) ne sont pas consignées dans le corps ci-dessous, alors que leurs PRs sont mergées et leurs modules noirs rendus visibles.

Quatre PRs non consignées dans le corps ci-dessous :

PR Date merge Sujet Effet visibilité
#19110 2026-10-04 feat(lean,#11703): annexe sites & topologies dans Lean-15c — lake grothendieck_lean 0/83 modules noirs (toute la couche sites & topologies ajoutée à Lean-15c)
#19083 2026-10-04 feat(lean,#11703): annexe Flasque/Godement dans Lean-15c 16/83 → 8/83 modules noirs dans grothendieck_lean (8 modules Flasque + Godement rendus visibles)
#18925 2026-10-03 Add: Lean-17c section 6 — visibilité des trois modules sombres de knot_lean trois modules sombres de knot_lean couverts par Lean-17c
#18050 2026-09-29 feat(notebook-lean): rendre visibles cinq modules EffectiveTheory dans SL-1b vague 4 (5 modules EffectiveTheory rendus visibles)

Portée vérifiée : la correction ne touche ni la métrique de tête du 2026-09-02 (12 % de modules invisibles), ni les critères d'acceptance (« le plus petit critère non tenu » mentionné en 2026-09-02). Les 4 PRs affinent la couverture par lake sans contredire la pose.

Réserve signalée : la vague 5 (#19110 + #19083) est arrivée après le constat du 2026-09-02 ; le chiffre « 8/83 » affiché dans le tableau par-lake n'inclut pas ces deux livraisons. Une ré-exécution de l'organe scan_lake_notebook_visibility.py à la tête 72008d621 (main actuel) est attendue pour mesurer la couverture actualisée — le geste n'est pas couvert par cette consolidation (qui se borne à consigner les PRs mergées sans fermer l'EPIC).

L'EPIC reste OPEN — le critère « le plus petit critère non tenu » mentionné au 2026-09-02 attend sa propre décision (probablement une vague 6).

État au 2026-09-02 — 55 % de modules invisibles est devenu 12 %, et le seul critère non tenu est le plus petit

Passe de curation (défaut #13906). Cet EPIC a réussi, et son corps ne le dit pas : chaque ligne de son tableau du 2026-08-19 est fausse aujourd'hui, toutes dans le même sens. Sa méthode — mesurer la visibilité par un organe versionné plutôt qu'à l'impression — n'est pas amendée ; c'est elle qui permet de le constater.

La métrique de tête, rejouée par l'organe officiel

python scripts/lean/scan_lake_notebook_visibility.py --json <out> (exit 0, contrôle positif intégré PASS), ce jour :

corps (2026-08-19) rejeu 2026-09-02
modules invisibles 97 / 177 (55 %) 25 / 212 (12 %)
borne haute (décl. citées) 556 / 2 793 (20 %) 1 072 / 3 227 (33 %)
borne basse 359 / 2 793 (13 %) 791 / 3 227 (25 %)
lakes couverts 19 22

Le corpus a grossi de 2 793 à 3 227 déclarations et la couverture a monté : ce n'est pas un effet de dénominateur.

Le tableau par lake est faux ligne à ligne — dans le bon sens

Lake corps 19/08 rejeu 02/09
grothendieck_lean 44/47 noirs 11/64
conway_lean 18/40 1/37
learning_theory_lean 15/17 1/16
knot_lean 1/8 0/6
mimo_lean 1/6 0/6
kelly_lean 2/4 0/3

V1 (erc20, finiteness), V2 (les trois sous 50 %) et V3 (conway, knot, mimo, kelly) sont livrés ou dépassés, par les compagnons Lean-14b, Lean-15c, Lean-16j, Lean-17c, Lean-22b, Lean-26, SC-7b/SC-7c, Kelly_companion_lean, SL-1b, GT-27b, GT-08d, DecInfer-02, tous présents sur main.

Ce qui reste noir, et ce que ça vaut

Les 25 modules invisibles sont très concentrés :

Lake noirs Nature
discrepancy_lean 6 / 8 le vrai trou — lake créé le 2026-08-25 (d84eb35f5), postérieur au corps, jamais cité ici. Compagnon existant (Search-09d-Lean-Discrepancy-Komlos) mais 6 modules sur 8 non atteints
grothendieck_lean 11 / 64 reste du plus gros chantier, à 17 % contre 94 % à l'ouverture
finiteness_lean 1 / 1 faux-noir d'instrument — compagnon rendu -- AUCUN -- alors que SC-7b/SC-7c existent ; artefact de noms de module courts, documenté trois fois dans le fil
conway · learning_theory · decision_theory · minimax · sudoku · erc20 · assignment 1 chacun résidus unitaires, plusieurs de la même classe de faux-noir

Un rewrite honnête doit ajouter discrepancy_lean au périmètre : c'est aujourd'hui le seul lake dont la majorité des modules est invisible, et il n'existait pas quand le corps a été écrit. Il est porté par #12823.

Le critère d'acceptance 3 n'est PAS livré — et c'est le seul

« signal CI advisory listant les déclarations ajoutées non citées sur les PR *_lean/** »

grep -rli 'scan_lake_notebook_visibility' .github/workflows/   →   0

Aucun workflow ne référence l'organe. #11704 (mergée) a versionné le script et une section de règle — pas de CI. Le critère 4 (instrument versionné avec contrôle positif) est, lui, tenu : le script existe, son contrôle positif passe, exit 0 ce jour.

C'est le grain le plus net de cet EPIC : un workflow advisory d'une vingtaine de lignes, qui empêcherait la métrique de re-dériver au lieu de la faire re-mesurer à la main tous les quinze jours. Sans lui, ce corps redeviendra faux — c'est exactement ce qui vient de se produire.

Livraisons

gh pr list --state all --search "11703 in:body" → 39 mergées, 2 ouvertes (#14105 et #14153, enrichissement markdown de Lean-22b-MIMO — pas de nouveau compagnon).

Contexte : #4362 et #11259 ouvertes ; #11148 fermée le 19/08.

Ce qui reste, dans l'ordre

  1. Le workflow advisory (critère 3) — le seul critère structurel ouvert, et celui qui protège tous les autres.
  2. discrepancy_lean — 6 modules sur 8, le plus gros trou réel, absent du corps.
  3. grothendieck_lean — 11 modules, la queue du plus gros chantier.
  4. Le faux-noir de nom court — corriger l'instrument plutôt que le contourner : sept des résidus unitaires en relèvent, et chacun coûte une investigation à qui le lit.

Corps d'origine conservé intégralement ci-dessous (2026-08-19). La méthode, les bornes haute/basse et les quatre critères d'acceptance restent valides mot pour mot ; seuls les chiffres, le tableau par lake et le périmètre de lakes avaient dérivé.

[EPIC] Visibilite des lakes Lean dans les notebooks — 13-20 % des declarations citees, 97/177 modules invisibles

state: OPEN | created: 2026-08-19T02:11:43Z | updated: 2026-08-31T20:16:36Z
labels: ['EPIC']

Prémisse (user, 2026-08-19) : « il faudrait créer un Epic pour assurer la MAJ des notebooks au fur et à mesure que nos lakes s'enrichissent car c'est leur vraie visibilité » — et, sur la forme : « ma préférence quand c'est possible va à la mise en place d'un Notebook sous kernel Lean à côté du Notebook Python, plus lisible que des loaders surtout quand il s'agit de présenter des lakes complexes. Idéalement on veut les deux ».

Ce que ce dépôt produit en Lean n'existe, pour un lecteur, que dans la mesure où un notebook le montre. Aujourd'hui, la majorité de ce que les lakes contiennent n'est visible nulle part.

La mesure (repo-wide, 2026-08-19)

Instrument : extraction des déclarations de chaque *.lean propriétaire (hors .lake/packages, _peters, reference_docs, foundry-lib/lib, siblings _en.lean dédupliqués), puis recherche de chaque nom dans le corpus entier des 1045 notebooks (471 MB). Deux bornes, parce qu'un nom court et générique (map, add, flipAt) peut coïncider par hasard :

Borne Définition Résultat
haute (généreuse) tout nom trouvé, y compris les courts/génériques 556 / 2793 = 20 %
basse (stricte) noms distinctifs seulement (≥ 10 car. ou contenant _) 359 / 2793 = 13 %

97 modules sur 177 (55 %) ne sont cités par aucun notebook — pas « peu cités » : zéro occurrence d'aucune de leurs déclarations, nulle part.

Contrôle positif (le zéro qui a failli être publié)

Une première passe rendait 0 / 2444 — un faux zéro : le fichier de motifs avait été écrit par un Python Windows dans un /tmp que Git Bash ne résout pas au même endroit, et grep -f sur un fichier absent ne rend pas d'erreur visible dans un pipe. Une seconde a manqué noncomputable def (donc mimoObj, la définition centrale de mimo_lean). L'instrument final assère son contrôle positif dans la même invocation et s'arrête si le contrôle échoue.

Par lake — et le constat de forme qui recoupe la préférence user

cité = borne stricte. invisibles = modules à 0 déclaration citée.

lake décl. cité invisibles notebook compagnon principal kernel
galois_lean 562 5 0/12 Lean-23-Galois-Probleme-Inverse-M23 python3
grothendieck_lean 481 14 44/47 Lean-15b-Lean-Grothendieck python3
learning_theory_lean 105 2 15/17 SL-1-LogicalLearning python3
kelly_lean 33 2 2/4 QuantConnect/kelly_lean/Kelly_companion python3
erc20_lean 17 0 3/3 aucun —
finiteness_lean 7 0 1/1 aucun —
conway_lean 696 126 18/40 Lean-16b (+ 16d/16e natifs) python3
game_theory_lean 445 54 7/26 GameTheory-15b-Lean-CooperativeGames lean4-wsl
knot_lean 131 26 1/8 Lean-17-Knots-a-Conway-and-Proofs python3
decision_theory_lean 89 30 2/8 DecInfer-2-Lean-ExpectedUtility lean4-wsl
mimo_lean 47 18 1/6 Lean-22-MIMO-Detection-Flips python3
calibration_lean 34 7 0/3 GameTheory-2b-Lean-Definitions lean4-wsl
sensitivity_lean 29 9 0/2 Lean-12 (+ Lean-12b natif) python3 (+lean4-wsl)
argumentation_lean 27 14 1/2 Tweety-5b-Lean-Argumentation lean4-wsl
sudoku_lean 24 13 1/3 Sudoku-19-Lean-Propagation lean4-wsl
minimax_lean 22 11 1/2 GameTheory-5b-Lean-Minimax lean4-wsl
search_lean 22 19 0/2 Lean-18-Search-AStar-Optimality python3
planning_lean 18 8 0/1 Planners-5b-Lean-Relaxation lean4-wsl
conway_cgt_lean 4 1 0/1 Lean-16a-Conway-Man-and-Work python3

Observation — les compagnons lean4-wsl sont médians à ~44 % de couverture, les python3 à ~19 %. Ce n'est pas une preuve de causalité : les deux lakes les plus massifs (galois, grothendieck, 1043 déclarations à eux deux) sont aussi python3, donc taille et kernel co-varient dans l'échantillon — le chiffre ne survivrait pas à un décroisement propre. Ce qu'il indique honnêtement : là où le compagnon est un loader Python, c'est aussi là que les modules disparaissent en masse, et c'est exactement la forme que le user identifie comme moins lisible.

Ce que cet Epic vise

Cible : « aucun module livré n'est entièrement invisible » — pas un ratio de citation. Viser 45/45 déclarations par notebook produirait un catalogue, pas un cours ; un module à 0 est, lui, un travail formel qui n'existe pour personne.

Forme préférée (mandat user) : un notebook à kernel Lean (lean4-wsl) à côté du notebook Python, plutôt qu'un loader Python qui affiche du .lean comme du texte. Le dépôt en porte déjà le patron et la convention de nommage — Lean-12 / Lean-12b, Lean-16b / Lean-16d, Lean-11 / Lean-11-Python, et tous les GameTheory-Nb-Lean-*. Il n'y a donc rien à inventer : il y a à l'étendre aux lakes qui n'ont qu'un loader. « Idéalement les deux » — le Python garde la narration, les figures et l'interfaçage ; le Lean montre les énoncés qui compilent.

Vagues

V1 — les deux lakes sans aucun compagnon (erc20_lean 17 décl., finiteness_lean 7). Petits, donc un notebook natif complet est atteignable d'un grain. Note : Lean-14-Finiteness-Derivatives.ipynb existe mais ne cite aucune déclaration distinctive de finiteness_lean — à vérifier avant de conclure « absent ».

V2 — les trois effondrements : grothendieck_lean (44 modules invisibles sur 47), learning_theory_lean (15/17), galois_lean (5 déclarations visibles sur 562). Ce sont les « lakes complexes » que le user cite nommément : compagnon lean4-wsl prioritaire.

V3 — les compagnons Python des lakes moyens : conway_lean (18 modules invisibles ; 16d/16e natifs existent, donc la marche est courte), knot_lean, mimo_lean, kelly_lean.

V4 — l'organe. Une règle de process ne tient pas par la vigilance (leçon maison). Signal CI advisory : sur toute PR touchant *_lean/**, lister les déclarations ajoutées qui ne sont citées par aucun notebook, et le rappeler dans le rollup. Advisory d'abord — un gate bloquant sur un ratio inciterait à citer des noms pour faire vert, ce qui est précisément le gaming que la cible « aucun module invisible » évite.

Critères d'acceptance

  1. erc20_lean et finiteness_lean ont un compagnon nommé (V1).
  2. Les trois lakes de V2 passent sous 50 % de modules invisibles, avec un compagnon lean4-wsl livré et exécuté (outputs réels, cf C.2).
  3. Le signal advisory de V4 tourne sur les PR *_lean/** et sa sortie est lisible dans le rollup.
  4. La mesure est rejouable : l'instrument est versionné dans scripts/lean/ avec son contrôle positif.

Ce que cet Epic ne fait pas

Il ne demande pas d'exécuter tous les lakes dans les notebooks (galois_lean seul = 562 déclarations), ni de citer chaque lemme. Il ne traite pas la qualité pédagogique de ce qui est cité — c'est le grain de #11259 et des règles d'enrichissement.

Ouvert sur demande user (2026-08-19). Voir #4362 (infrastructure des lakes, distinct), #11148 (le cas mimo_lean qui a déclenché la question).

Activity

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    EPICEpic tracking issue with sub-issues

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions