Repository navigation
Docs(lean): les pins Mathlib documentes contredisent les lakefiles (3 lakes mesures, cohorte GameTheory a mesurer) #24634
Description
Constat
Trois lakes Lean documentent une version de Mathlib que leur propre lakefile.lean contredit. Le fichier qui fait foi est le lakefile ; c'est la documentation qui est fausse.
Mesure du 2026-11-04, sur origin/main (bb19c7151ed), en lisant lean-toolchain et le require mathlib de chaque lake :
| Lake | lean-toolchain (fait foi) |
Mathlib (fait foi) | ce que la doc annonçait |
|---|---|---|---|
Search/search_lean |
v4.33.0 |
db584cd6 |
v4.31.0-rc1 (README L216) |
Probas/DecisionTheory/decision_theory_lean |
v4.33.0 |
db584cd6 |
v4.31.0-rc1 (README L42, L55) et v4.30.0-rc2 (docstrings Discount.lean L95, Discount_en.lean L94) |
Search/discrepancy_lean |
v4.33.0 |
db584cd6 |
v4.32.1 / 520045ab (README L55) |
search_lean se contredit à l'intérieur de son propre README : L216 annonçait v4.31.0-rc1, L221 annonçait déjà v4.33.0. Et decision_theory_lean portait deux versions périmées différentes (v4.31.0-rc1 et v4.30.0-rc2) pour une seule dépendance.
Pourquoi ça compte
Un lecteur qui suit la documentation télécharge la mauvaise Mathlib. Plus gênant : la phrase de Discount.lean (« tsum_le_tsum non disponible dans Mathlib v4.30.0-rc2 ») se lit aujourd'hui comme une affirmation sur le pin courant, alors qu'elle décrit la version contre laquelle le contournement a été écrit.
Portée du correctif
Les déclarations de pin sont corrigées sur la valeur mesurée. Les deux phrases historiques (Discount.lean/Discount_en.lean, README L75) ne sont pas rebasées sur v4.33.0 : je n'ai pas mesuré si tsum_le_tsum est encore absent sur ℝ nu au pin db584cd6, et l'écrire le serait sans preuve. Elles sont marquées comme décrivant la version alors utilisée, ce qui est vrai et ne prétend rien sur la version actuelle.
Hors périmètre de cette passe — même classe, cohorte non mesurée
Un balayage plus large montre que le défaut existe aussi dans GameTheory, sur des lakes que cette passe n'a pas mesurés :
GameTheory/conway_cgt_lean— lakefilev4.33.0-rc1/bb863d3d, doc annoncev4.31.0-rc1GameTheory/game_theory_lean— lakefilev4.33.0/db584cd6, README annoncev4.32.1/520045abGameTheory/minimax_lean— lakefilev4.33.0/db584cd6, README annoncev4.32.1GameTheory/lean_game_defs— lakefilev4.33.0, README annoncev4.32.1
Ces quatre-là sont mesurés ; d'autres lakes de la même famille (cooperative_games_lean, assignment_lean, asymmetric_information_lean, lean_game_defs_ext) n'ont pas été vérifiés et ne sont donc pas affirmés périmés. La première étape d'une passe suivante est de les mesurer, pas de les corriger en série.
social_choice_lean et repeated_games_lean ne portent pas de projet Lean à leur racine (le second est vide, ses sources vivent dans game_theory_lean) : leurs mentions de version demandent une lecture au cas par cas, pas un remplacement mécanique.
Critère de clôture
- les 3 lakes ci-dessus alignés sur leur lakefile (fait dans la PR liée)
- cohorte GameTheory mesurée lake par lake, puis alignée
- aucune affirmation de version écrite sans lecture du
lean-toolchain/lakefile.leandu lake concerné
Aucun sorry ajouté ni retiré par cette passe : elle ne touche que de la documentation et des docstrings.
Activity
jsboige commentedon Nov 4, 2026
[CLAIMED] lane myia-po-2024:CoursIA -- aligner les pins Mathlib documentes sur les lakefiles (3 lakes) -- paths: MyIA.AI.Notebooks/Search/search_lean/README.md, MyIA.AI.Notebooks/Search/discrepancy_lean/README.md, MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/README.md, MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/Gittins/Discount.lean, MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/Gittins/Discount_en.lean
(check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with
[RELEASED]when your PR lands.)jsboige commentedon Nov 4, 2026
[DELIVERED] lane myia-po-2024:CoursIA -- PR #24636 (paths: MyIA.AI.Notebooks/Search/search_lean/README.md, MyIA.AI.Notebooks/Search/discrepancy_lean/README.md, MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/**
Livraison partielle : les 3 lakes mesures sont alignes sur leur lakefile. La cohorte GameTheory nommee dans le body reste a mesurer lake par lake -- l'issue reste ouverte pour cette part.
Les deux phrases historiques sur tsum_le_tsum ne sont pas rebasees sur v4.33.0 : l'absence au pin db584cd6 n'est pas mesuree, l'affirmer serait sans preuve. Elles sont marquees comme decrivant la version alors utilisee.
jsboige commentedon Nov 4, 2026
[CLAIMED] lane myia-po-2024:CoursIA -- paths: MyIA.AI.Notebooks/GameTheory/game_theory_lean/README.md, MyIA.AI.Notebooks/GameTheory/minimax_lean/README.md, MyIA.AI.Notebooks/GameTheory/lean_game_defs/README.md, MyIA.AI.Notebooks/GameTheory/lean_game_defs_ext/README.md
Cohorte GameTheory mesuree (suite de la tranche #24636, qui portait Search/Probas) : 4 lakes sur 7 documentent un pin contredit par leur propre
lean-toolchain. Correction des 4 README, sans toucher aux pins eux-memes.jsboige commentedon Nov 4, 2026
[DELIVERED] lane myia-po-2024:CoursIA -- PR #24638 -- paths: MyIA.AI.Notebooks/GameTheory/game_theory_lean/README.md, MyIA.AI.Notebooks/GameTheory/minimax_lean/README.md, MyIA.AI.Notebooks/GameTheory/lean_game_defs/README.md, MyIA.AI.Notebooks/GameTheory/lean_game_defs/README.en.md, MyIA.AI.Notebooks/GameTheory/lean_game_defs_ext/README.md
Cohorte GameTheory entierement mesuree (7 lakes) : 4 documentaient un pin contredit par leur
lean-toolchain(v4.32.x annonce, v4.33.0 reel), corriges dans #24638.assignment_leanetconway_cgt_leanetaient deja justes ;asymmetric_information_leann'annonce aucun pin ;cooperative_games_leanest un dossier vide, pas un lake.Non touche volontairement : les 3 mentions
v4.32.1degame_theory_lean/README.mddecriventSocialChoice/social_choice_lean_peters/, lake separe reellement pinne v4.32.1 (verifie : sonlean-toolchaindit v4.32.1 et son lakefile epingle le commit520045ab14e).Reste ouvert sur cette issue : les autres series Lean (SocialChoice, Search residuel, Probas).
jsboige commentedon Nov 4, 2026
[CLAIMED] lane myia-po-2027:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/README.md
Extension de la classe #24634 à la cohorte
SymbolicAI/Lean, que l'issue n'avait pas mesurée (po-2024 tient Search/Probas/GameTheory, périmètres distincts, aucun chevauchement).Coorte SymbolicAI/Lean mesurée lake par lake ce cycle — 9 lacs porteurs d'un
README.md+lakefile.lean,lean-toolchainlu pour chacun :lean-toolchain(fait foi)ANALYSE/kls_lean520045a)GALOIS/galois_leanGeometry/geometry_leanLanglands/hecke_leandb584cd6d46c)differential_leanfiniteness_leanformal_groups_leangrothendieck_leansensitivity_leanUn seul décalage réel sur neuf. Les huit autres mentions de versions périmées que rend un balayage naïf sont de l'historique de migration légitime (« migrée depuis v4.31.0-rc1 par #10997 ») ou des revs d'autres paquets ; les corriger serait un faux positif, exactement ce que #24634 interdit (« une affirmation de version écrite sans lecture du
lean-toolchain»).Correction prévue : les trois affirmations d'état courant du README de
galois_lean(toolchain, rev Mathlib, formeglobs) + la phrase de pin de la prologue CoursIA deM23Lean4Web.lean. Aucune ne touche à un fichier de preuve ni à un pin.galois_leanest en lecture seule depuis le début de ce cycle : je viens de le relever pour #1453, aucun fichier modifié.jsboige commentedon Nov 4, 2026
[CLAIMED-AMEND] lane myia-po-2027:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/README.md, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/README.md
L'amend corrige une erreur de chemin dans la claim precedente, pas un elargissement de perimetre : la cohorte mesuree reste la meme (les lakes Lean sous
SymbolicAI/Lean), maisconway_leann'est plus a la racine deSymbolicAI/Lean.Il a demenage par
9c4c35fc36— « Refactor(lean,#23164): descendre le lake conway_lean vers GOL/conway_lean (#24166) ». Ma lecture initiale portait sur une copie locale en retard de 7 commits surorigin/main, ou l'ancien chemin existait encore. Le chemin declare ci-dessus est celui de l'arbre courant : verifie surorigin/main(e9583eb),find -name lakefile.leanrend./GOL/conway_lean, et rien a./conway_lean.Les deux fichiers restent disjoints de la partition de myia-po-2024 sur cette issue, qui porte
Search/,Probas/etGameTheory/.jsboige commentedon Nov 4, 2026
[DELIVERED] lane myia-po-2027:CoursIA -- PR #24642 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/GALOIS/galois_lean/README.md, MyIA.AI.Notebooks/SymbolicAI/Lean/GOL/conway_lean/README.md
Cohorte
SymbolicAI/Leanmesuree lake par lake, puis alignee : 2 derives reelles sur 19 lakes, corrigees dans #24642.Le chiffre utile n'est pas 2, c'est l'ecart entre ce qu'un balayage rend et ce qu'une lecture confirme. Le scan naif signalait 10 lakes ; la reevaluation en a elimine 8, chacun pour un motif different et nomme : mention historique parenthesee (
calibration_lean,sensitivity_lean), recit date d'une Partie (grothendieck_lean), version d'un lake frere citee comme repere (mimo_lean), ecart delibere documente ou le lake suit son amont et non le parc (differential_lean), et absence de README a la racine (riemann200_lean,serre100_lean,torchlean_lean). Sans la reevaluation, la PR aurait reecrit de l'histoire vraie.Deux derives de chemin corrigees au passage, qui expliquent pourquoi la mesure initiale avait RATE
conway_lean: le lake a demenage enGOL/conway_leanpar9c4c35fc36(#24166), et ma lecture portait sur une copie locale en retard de sept commits ou l'ancien chemin existait encore. Un scan sur un arbre non rafraichi ne voit pas ce qu'il pretend mesurer.Cloture de l'issue, mon avis : les trois criteres sont couverts par deux lanes — les 3 lakes d'origine et la cohorte GameTheory par po-2024 (#24636, #24638), la cohorte
SymbolicAI/Leanpar ce grain. Le troisieme critere (« aucune affirmation de version ecrite sans lecture du toolchain du lake ») est tenu par construction dans les deux PRs. Reste a trancher cote coordinateur ; je ne ferme pas.Une chose que ce grain n'a pas faite, et qui reste ouverte :
scripts/lean/setup_shared_mathlib.ps1liste encoreSymbolicAI/Lean/conway_leana l'ancien emplacement dans sa sortie de scan. C'est la meme classe de derive que celle corrigee ici, mais dans un script, pas dans un README — je ne l'ai pas touche pour ne pas melanger deux sujets dans une PR de documentation.jsboige commentedon Nov 4, 2026
[ACTION] Correction de la derniere ligne de mon
[DELIVERED]ci-dessus : le chemin perime que j'y signalais n'existe pas surmain.J'avais ecrit que
scripts/lean/setup_shared_mathlib.ps1listait encoreSymbolicAI/Lean/conway_lean. Mesure refaite sur l'arbre courant (origin/maine9583eb471, worktree isole) : le workflowlean-conway.ymlporte 0 occurrence de l'ancien chemin et 13 deGOL/conway_lean, et le log du dernier run CI construit bien sousGOL/(8802 jobs, cache.../GOL/conway_lean/.lake). Le demenagement #24166 a mis les filtres de chemin a jour correctement.La ligne venait de mon clone principal, en retard de sept commits : l'entree perimee est dans son cache local
.mathlib-cache/.../share-state.json, qui est gitignore et ne dit rien de l'etat du depot. C'est la meme cause que l'erreur de chemin de mon[CLAIMED-AMEND]plus haut — deux lectures consecutives sur un arbre non rafraichi, deux fausses conclusions.Ce qui reste vrai : les deux README corriges dans #24642, et la mesure des 19 lakes. Ce qui tombe : le suivi que j'annoncais comme ouvert. Aucune issue de suivi n'est due pour ce point.
Fix(docs,#24634): les deux pins GameTheory restes en ecart, releves p…
Fix(docs,#24634): L268 de decision_theory_lean ne pose plus au presen…
Fix(docs,#24634): review -- matrix CI named in README, glob docstring…
Fix(docs,#24634): README galois_lean et conway_lean alignes sur leurs…
Docs(lean,#24634): les pins Mathlib documentes contredisent les lakef…
Docs(lean,#24634): aligner les pins documentes de 4 lakes GameTheory …