From 1e81bdb49a8f8ece872dea17c838ae36011948bb Mon Sep 17 00:00:00 2001 From: jsboige Date: Sun, 13 Sep 2026 13:03:17 +0200 Subject: [PATCH] build(mimo,#14773): migrate lake to Lean 4.33 Pin Mathlib to the repository-wide 4.33 closure and use the bounded SLT compatibility commit required by Lean 4.33. Co-Authored-By: Claude Code --- .../SymbolicAI/Lean/mimo_lean/README.md | 20 +++++++---- .../Lean/mimo_lean/lake-manifest.json | 34 +++++++++---------- .../SymbolicAI/Lean/mimo_lean/lakefile.lean | 26 +++++++++----- .../SymbolicAI/Lean/mimo_lean/lean-toolchain | 2 +- 4 files changed, 48 insertions(+), 34 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/README.md b/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/README.md index 40679ac26d..78d1eb4bff 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/README.md +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/README.md @@ -1,9 +1,9 @@ # mimo_lean — Détection MIMO par descente à flips (Lean 4) Port formel de l'algorithme de détection MIMO par flips de coordonnées -(Papailiopoulos, 2026 — issue #10984). Le lake naît directement sur -`v4.32.1` (Mathlib résolu à `520045ab14e26149ee970e2e617ca04b09bde5d6`, -fin de la migration #10986) et suit la convention i18n #4980 +(Papailiopoulos, 2026 — issue #10984). Le lake cible désormais +`v4.33.0` (Mathlib résolu à `db584cd6d46c92f209a44c0f1c829460d327499d`, +rollout #14773) et suit la convention i18n #4980 (docstrings FR par défaut, sibling `_en` avec namespace `Mimo_en`). ## Phases et libs compilées @@ -40,12 +40,18 @@ autres lakes du dépôt). | Lake | Source | Pin | Consommé par | |----------------|-------------------------------------------------------------------------|-------------------------------------------|------------------------------------| -| **mathlib4** | github.com/leanprover-community/mathlib4.git | `v4.32.1` (résolu `520045ab…`) | Objective, Lmmse, Converse, Bridge, NormTails | -| **slt** | github.com/YuanheZ/lean-stat-learning-theory.git (Apache 2.0) | `d0f506f0a695018265dccb33bcb05e2f5ca1c876` | Converse (Hanson–Wright), NormTails (Lipschitz) | +| **mathlib4** | github.com/leanprover-community/mathlib4.git | `v4.33.0` (résolu `db584cd6…`) | Objective, Lmmse, Converse, Bridge, NormTails | +| **slt** | github.com/jsboige/lean-stat-learning-theory.git (fork Apache 2.0) | `0b1020a4771037b89d0b3809913608d177c09a14` | Converse (Hanson–Wright), NormTails (Lipschitz) | Le pin SLT est **identique** à `lake-manifest.json` — la `require` ne dérive -pas. Aucune mise à jour de SLT n'est prévue sans revue dédiée (sécurité de -la frontière formelle). +pas. Il ajoute à la base upstream `d0f506f0a695018265dccb33bcb05e2f5ca1c876` +une seule adaptation : la preuve explicite de non-négativité du cas de rayon +nul dans `SLT.HansonWright`, nécessaire sous Lean 4.33. Le lake SLT cible encore +Lean/Mathlib 4.32 ; dans `lakefile.lean`, Mathlib est donc déclaré en dernier afin +que Lake 5 sélectionne sa fermeture transitive 4.33 (Batteries, Qq, Cli, etc.) +plutôt que celle héritée de SLT. Cet ordre est une contrainte de résolution +documentée, pas un tri cosmétique. Toute autre mise à jour de SLT demande une +revue dédiée (sécurité de la frontière formelle). ## Inventaire détaillé des phases diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lake-manifest.json b/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lake-manifest.json index 93d88f8b1a..baf5d4c477 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lake-manifest.json +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lake-manifest.json @@ -1,31 +1,31 @@ {"version": "1.2.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/YuanheZ/lean-stat-learning-theory.git", + [{"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "d0f506f0a695018265dccb33bcb05e2f5ca1c876", - "name": "slt", + "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "d0f506f0a695018265dccb33bcb05e2f5ca1c876", + "inputRev": "db584cd6d46c92f209a44c0f1c829460d327499d", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4.git", + {"url": "https://github.com/jsboige/lean-stat-learning-theory.git", "type": "git", "subDir": null, "scope": "", - "rev": "520045ab14e26149ee970e2e617ca04b09bde5d6", - "name": "mathlib", + "rev": "0b1020a4771037b89d0b3809913608d177c09a14", + "name": "slt", "manifestFile": "lake-manifest.json", - "inputRev": "v4.32.1", + "inputRev": "0b1020a4771037b89d0b3809913608d177c09a14", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "6e311e2a844da9b2cc3971187df2fe0066947b93", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -85,7 +85,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -95,10 +95,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "88679d088c9720c27ebdf2ba4dafe17341747f94", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.32.0", + "inputRev": "v4.33.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "mimo_lean", diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lakefile.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lakefile.lean index 7f3a7609c5..b8d6e384d9 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lakefile.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lakefile.lean @@ -5,9 +5,9 @@ open Lake DSL # Lake mimo_lean — détection MIMO par descente à flips (Lean 4) Port formel de l'algorithme de détection MIMO par flips de coordonnées -(Papailiopoulos, 2026 — cf issue #10984). Le lake naît directement sur -`v4.32.1` (fin de la migration #10986) — Mathlib résolu à -`520045ab14e26149ee970e2e617ca04b09bde5d6` (cf `lake-manifest.json`). +(Papailiopoulos, 2026 — cf issue #10984). Le lake cible désormais +`v4.33.0` (rollout #14773) — Mathlib résolu à +`db584cd6d46c92f209a44c0f1c829460d327499d` (cf `lake-manifest.json`). Six libs compilées, deux phases utilitaires + quatre phases du papier §11 : @@ -25,8 +25,9 @@ Six libs compilées, deux phases utilitaires + quatre phases du papier §11 : - **Phase 3b / Converse** (`Converse.lean`) : converse §11 — concentration Hanson–Wright du bruit (`‖w‖²` chi-square), union bound `(1−p)^n ≤ e^{−np}`, appui sur le lake externe - `YuanheZ/lean-stat-learning-theory` (SLT, pinned - `d0f506f0a695018265dccb33bcb05e2f5ca1c876`, Apache 2.0). + `YuanheZ/lean-stat-learning-theory` (SLT, base + `d0f506f0a695018265dccb33bcb05e2f5ca1c876`, Apache 2.0) avec un commit de + compatibilité Lean 4.33 borné à la preuve du cas de rayon nul. - **Phase 4 / Bridge** (`Bridge.lean`, grignotage #11148) : pont entre `mimoObj` (Phase 2) et converse (Phase 3b) — identité de différence de coût `cost_diff`, fragment de converse connecté au ML. @@ -41,11 +42,18 @@ Convention i18n #4980 : docstrings FR par défaut, sibling `_en` package «mimo_lean» where leanOptions := #[⟨`autoImplicit, false⟩] -require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "v4.32.1" - +/- +Le fork SLT ajoute à la base upstream d0f506f une unique adaptation de preuve +pour Lean 4.33 ; son lake reste épinglé à Mathlib 4.32. Lake 5 résout les +dépendances directes dans l'ordre inverse de leur déclaration : Mathlib doit +rester en dernier pour que sa fermeture transitive 4.33 (Batteries, Qq, Cli, +etc.) l'emporte sur celle de SLT. +-/ require slt from git - "https://github.com/YuanheZ/lean-stat-learning-theory.git" @ "d0f506f0a695018265dccb33bcb05e2f5ca1c876" + "https://github.com/jsboige/lean-stat-learning-theory.git" @ "0b1020a4771037b89d0b3809913608d177c09a14" + +require mathlib from git + "https://github.com/leanprover-community/mathlib4.git" @ "db584cd6d46c92f209a44c0f1c829460d327499d" @[default_target] lean_lib «Descent» where diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lean-toolchain b/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lean-toolchain index 2b61957be5..025e59548e 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lean-toolchain +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/mimo_lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.1 +leanprover/lean4:v4.33.0