From 84725bf197dffbeedd5f4b03bd45f24ede6f907e Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 26 Sep 2026 06:37:52 +0200 Subject: [PATCH] =?UTF-8?q?docs(14773,#14773):=20social=5Fchoice=5Flean=5F?= =?UTF-8?q?peters=20=E2=80=94=20documenter=20le=20blocage=20amont=20v4.33?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Le README affirmait que le pin `v4.32.1` de ce lake etait « converge » avec le parc et que « la convergence #4364 s'applique desormais ici aussi ». La cible du parc est passee a `v4.33.0` (EPIC #14773) : l'affirmation est donc perimee, et le lake est en realite une exception. Mesure firsthand (tentative instrumentee, journal conserve) : toolchain bascule, les huit dependances transitives explicitees aux revs du parc, `lake update`, `lake exe cache get`, `lake build`. Le contournement de version a fonctionne (les erreurs ont quitte Batteries/Qq/ProofWidgets) et a revele une incompatibilite reelle dans les sources du paquet externe `DominikPeters/SocialChoiceLean@94a4c650` : SocialChoice/Margin.lean:277,281,313,317,756,759 (rfl failed / Type mismatch) SocialChoice/Impossibilities/GibbardSatterthwaite/InductionStepCase2.lean:1286,1288 -> compilation atteint [3029/3044] puis echoue Classe d'erreur unique : les buts residuels opposent `V ⊕ Unit` a `V` (ex. `|- Sum.inr w ∈ {v | a < b} ↔ w ∈ {v | a < b}`). Ces fichiers ne sont pas les notres et le depot amont ne publie aucun etat compatible 4.33 (dernier commit 2026-07-21). On ne patche pas de code vendored : le verdict est « bloque en amont », rapporte sur l'EPIC #14773. Le README est corrige par ajout d'un bloc date « Etat mesure au 2026-09-26 » et d'addenda ; l'historique du §EPIC #4365 est conserve intact en dessous. Aucun notebook, aucun octet de code Lean touche. Part of #14773 Co-Authored-By: Claude Code --- .../social_choice_lean_peters/README.md | 54 +++++++++++++++++-- 1 file changed, 50 insertions(+), 4 deletions(-) diff --git a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/README.md b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/README.md index 1a6cd3f370..2f6fb8c794 100644 --- a/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/README.md +++ b/MyIA.AI.Notebooks/GameTheory/social_choice_lean_peters/README.md @@ -6,10 +6,50 @@ de Peters. ## Statut -- **Toolchain** : `leanprover/lean4:v4.32.1` (alignée sur le parc, pin effectif du `lean-toolchain`) +> **État mesuré au 2026-09-26 — la cible de toolchain du parc est passée à `v4.33.0` (EPIC #14773) +> et ce lake ne peut pas suivre. Il est désormais une *exception documentée* du parc, et non plus +> un lake « convergé ».** + +- **Toolchain** : `leanprover/lean4:v4.32.1` — pin effectif du `lean-toolchain`, mais **en retard sur + la cible du parc** (`v4.33.0`). L'écart est mesuré, sa cause est amont, et il est documenté ci-dessous. - **Compte de sorry** : 0 sorry en production -- **Build** : `lake build` — SUCCESS -- **Dépendances** : Mathlib4 (`520045ab`), `DominikPeters/SocialChoiceLean` (`94a4c650`) — revs effectives du `lake-manifest.json` +- **Build** : `lake build` — SUCCESS à `v4.32.1` (le pin effectif) +- **Dépendances** : Mathlib4 (`520045ab14e2`), `DominikPeters/SocialChoiceLean` (`94a4c650b6a3`) — revs effectives du `lake-manifest.json` + +### Pourquoi ce lake reste à `v4.32.1` (mesuré, 2026-09-26) + +La migration vers `v4.33.0` a été **tentée et instrumentée** : `lean-toolchain` basculé, les huit +dépendances transitives explicitées (bloc `require … from git … @ ` aux révisions du parc, pour +que nos revs l'emportent sur celles charriées par le manifest de `SocialChoiceLean`), `lake update`, +`lake exe cache get`, puis `lake build`. Le contournement de version a **fonctionné** — les erreurs +ont quitté `Batteries.Tactic.Alias`, `Qq.Typ` et `ProofWidgets.Component.MakeEditLink` — et ont +révélé une incompatibilité **réelle, dans les sources amont** : + +``` +error: SocialChoice/Margin.lean:277:10: Tactic `rfl` failed +error: SocialChoice/Margin.lean:281:10: Type mismatch +error: SocialChoice/Margin.lean:313:10: Tactic `rfl` failed +error: SocialChoice/Margin.lean:317:10: Type mismatch +error: SocialChoice/Margin.lean:756:8: Tactic `rfl` failed +error: SocialChoice/Margin.lean:759:8: Tactic `rfl` failed +error: SocialChoice/Impossibilities/GibbardSatterthwaite/InductionStepCase2.lean:1286:2: unsolved goals +error: SocialChoice/Impossibilities/GibbardSatterthwaite/InductionStepCase2.lean:1288:2: unsolved goals +``` + +La classe d'erreur est unique et cohérente : les buts résiduels opposent la somme indexée +`V ⊕ Unit` au type nu `V` — par exemple +`⊢ Sum.inr w ∈ {v | a < b} ↔ w ∈ {v | a < b}` — soit un changement de la normalisation de `filter` +sur les sommes dans Mathlib 4.33. La compilation atteint `[3029/3044]` avant d'échouer. + +**Ces fichiers ne sont pas les nôtres.** Ce sont ceux du paquet externe +[`DominikPeters/SocialChoiceLean`](https://github.com/DominikPeters/SocialChoiceLean), épinglé à +`94a4c650b6a3` (dernier commit amont du 2026-07-21, « Clean up Lean 4.32 warnings » ; branches +disponibles `master`, `duggan-schwartz`, `claude/formalize-duggan-schwartz-AyuSa` — aucune ne porte +de portage 4.33). On **ne patche pas** du code *vendored* : le verdict est **bloqué en amont**, et il +est rapporté comme tel sur l'EPIC #14773 plutôt que contourné ici. + +**Conséquence** : le `v4.32.1` de ce lake est une **exception assumée** jusqu'à ce que l'amont +publie un état compatible 4.33. Ce n'est pas un défaut de ce dépôt, et ce n'est pas réparable ici. ## Modules @@ -53,6 +93,11 @@ Ce lake est **explicitement hors du périmètre d'absorption** dans Mathlib `520045ab` sur `lean-toolchain` `v4.32.1` — la famille du reste du parc. La convergence #4364 s'applique désormais ici aussi ; peters n'est plus résidu v4.27. + *(Addendum 2026-09-26 : cette phrase était vraie le 2026-08-21, quand la + cible du parc était `v4.32.1`. Depuis que la cible est passée à `v4.33.0` + (EPIC #14773), elle ne l'est plus — voir le bloc « Pourquoi ce lake reste à + `v4.32.1` » au §Statut. L'historique est conservé ci-dessus tel qu'il a été + écrit.)* 2. **Cadre sémantique distinct (toujours actif)** : ce lake expose un `LinearOrder` strict (Mathlib) qui **n'est pas** compatible avec l'API @@ -65,7 +110,8 @@ Ce lake est **explicitement hors du périmètre d'absorption** dans **Conséquence** : `social_choice_lean_peters/` reste un **lake autonome auto-suffisant** avec son propre `lake build`, son propre `lean-toolchain` -`v4.32.1` (convergé), et son propre CI. L'autonomie n'est plus motivée par un +`v4.32.1` (**exception documentée**, cf. bloc « Pourquoi ce lake reste à +`v4.32.1` » au §Statut), et son propre CI. L'autonomie n'est plus motivée par un verrou de version — elle est motivée par la nature du projet : une visite de référence d'une bibliothèque externe, dans son propre cadre sémantique.