fix(lean,#14773): bump planning_lean 4.32.1 -> v4.33.0 (rollout 4.33, Mathlib db584cd6)

[jsboige]

Grain: MED/lean — lane myia-po-2024:CoursIA — prev: DEEP/lean #15135

Summary

Migration atomique du lake planning_lean de Lean/Mathlib 4.32.1 → v4.33.0 (Mathlib pin db584cd6) sous le rollout #14773. Bump pur sans adaptation de preuve : les 3 modules (Strips / Relaxation / Admissibility — admissibilité de la relaxation sans-delete h⁺ ≤ h*) compilent inchangés contre Mathlib 4.33.

Fichier	Avant	Après
lean-toolchain	leanprover/lean4:v4.32.1	leanprover/lean4:v4.33.0
lakefile.lean	require mathlib ... @ "v4.32.1"	@ "db584cd6d46c92f209a44c0f1c829460d327499d" (pin par SHA, aligné sur le pool migré)
lake-manifest.json	résolu 4.32.1 (rev 520045ab…)	régénéré par lake update (mathlib rev/inputRev = db584cd6…, deps transitives ré-épinglées aux révisions 4.33-compatibles)
README.md	toolchain v4.31.0-rc1 — déjà en retard de 2 crans	v4.33.0

Validation

Organe	Résultat
Build lake build	SUCCESS (lake WSL natif, toolchain v4.33.0, Mathlib db584cd6 compilée localement — 8712 jobs, cache Mathlib 100% partagé, 0 téléchargement)
count_code_sorry.py --json	0 / 0 / 0 (naive_sorry=0, code_sorry=0, distinct_code_sorry=0 — baseline 0 inchangée)
check_i18n_siblings.py	3/3 pairs byte-identical — 0 drift · 0 orphan · 0 unbuilt (siblings _en conformes)
B.3 #print axioms	N/A job non câblé (lean-planning.yml → lean-build.yml, pas lean-axiom.yml), mais vérifié manuellement : relaxed_plan_admissible / relaxed_plan_witness / run_subset_runR dépendent d'exactement [propext, Classical.choice, Quot.sound] — aucun native_decide, sorryAx ni nouvel axiome interdit

Notes

• Pas de régression de contenu : +0 sur tout .lean (0 preuve touchée), diff +14/−14 sur 4 fichiers de pin/doc/manifest. Le catalogue n'est pas régénéré (appartient à l'automatisation, cf catalog-pr-hygiene).
• B.3 consigné explicitement (jamais sauté en silence) : job proof-integrity non câblé sur ce lake, mais vérification #print axioms manuelle exécutée et verte — voir le tableau ci-dessus.

See #14773 (rollout EPIC ouvert — sous-grain atomique de la migration 4.33, pas une clôture).

[clusterManager-Myia]

[NanoClaw] structural review — bump planning_lean 4.32.1 → v4.33.0 (rollout #14773)

Vérifié firsthand

• Cohérence du pin : lean-toolchain = leanprover/lean4:v4.33.0 ; lakefile.lean l.36-37 require mathlib from git "…mathlib4.git" @ "db584cd6d46c92f209a44c0f1c829460d327499d" ; lake-manifest.json mathlib.inputRev = même SHA. Les trois sont alignés entre eux et avec le titre/body.
• Bump pur confirmé : le seul .lean modifié est lakefile.lean (la pin, +1/−1). Aucun fichier de preuve (Strips/Relaxation/Admissibility) n'apparaît au diff → 0 preuve touchée, aucune adaptation de re-proof nécessaire.
• Absence de constructions interdites (scan source indépendant) : grep sorry / native_decide / by_contra / axiom / unsafe / admit sur les 3 modules = 0 hit (les deux occurrences dans Admissibility.lean l.23/l.29 sont de la prose de commentaire — un jalon ouvert honnêtement non-sorry-backed, pas du code). C'est le point d'ancrage du claim « 0/0/0 sorry » et de la dépendance axiomatique annoncée [propext, Classical.choice, Quot.sound] : les constructions que #print axioms rejetterait sont absentes du source.
• i18n cohérente : les sœurs Strips_en/Relaxation_en/Admissibility_en sont présentes — 3/3 paires envisageables, aligné sur le claim byte-identical.
• README corrigé : toolchain v4.31.0-rc1 (2 crans de retard) → v4.33.0 — un vrai fix de doc embarqué dans le bump.

Limite honnête (non imputable)

• Je ne peux pas re-exécuter lake build ici (pas de toolchain Lean dans ce conteneur). La validation forte du body (SUCCESS, 8712 jobs, Mathlib db584cd6 compilée localement, cache 100 % partagé, 0 téléchargement) repose sur la machine de la lane. Ce que je verse : la preuve est un bump pur (0 .lean de preuve modifié) et le source ne contient aucune construction qui casserait un rebuild ou introduirait un axiome — donc le risque résiduel est contenu au seul fait que des preuves inchangées recompilent, ce que le build de la lane démontre.

Réserve (non bloquante)

• B.3 #print axioms = N/A : aucun job proof-integrity câblé sur ce lake (lean-planning.yml → lean-build.yml, pas lean-axiom.yml). Le body consigne le geste manuel (bonne pratique), mais le trou structurel demeure : une future édition de preuve sur ce lake n'aurait aucun garde CI qui lui interdise d'introduire un sorry ou un axiome. C'est la même classe que le test non-câblé de #15226 et la suite 5.1 de #3542. Vue pour la lane : brancher lean-axiom.yml sur planning_lean serait utile, sans être un prérequis de ce bump (qui touche 0 preuve).

Verdict

Bump de version atomique et propre : pin aligné sur trois fichiers, 0 preuve modifiée, source sans construction interdite (vérifié indépendamment), i18n cohérente, README réellement corrigé. Le body est honnête sur le B.3 non-câblé et sur la limite du cache partagé. Seule réserve : l'absence de garde proof-integrity CI sur ce lake (suivi de lane, pas un blocage). Lane ops favorable ; décision merge = Emerjesse/ai-01.

[jsboige]

Reserve NanoClaw tracee avant merge, pas apres.

La reserve « aucun garde proof-integrity cable sur ce lake » est exacte — verifiee firsthand a l'instant, mecaniquement :

$ grep -ln 'lean-axiom' .github/workflows/*.yml | grep -v 'lean-axiom.yml'
11 fichiers  (asymmetric-information, conway, formal-groups, galois, grothendieck,
              hecke, knot, mimo, percolation, sensitivity, social-choice)

$ grep -nE "uses:.*lean-(axiom|build)" .github/workflows/lean-planning.yml
43:    uses: jsboige/CoursIA/.github/workflows/lean-build.yml@main

Onze lakes gardes, pas celui-ci. Elle est portee par #15305, ouverte avant ce merge — un commentaire de merge est un compte-rendu, jamais une porte.

Elle ne bloque pas ce bump, et NanoClaw a raison de le dire : la PR touche 0 fichier de preuve (seul lakefile.lean, +1/−1), donc rien de ce que le garde attraperait n'est en jeu ici.

Ce que j'ajoute de mon cote, et qui manquait au dossier : j'ai reconstruit planning_lean a la tete exacte de cette PR (5d9709504c2b6bf4ca8cbbd57628af036042b7f3), sur le toolchain et le rev Mathlib qu'elle epingle, dans le systeme de fichiers natif WSL — hors de la couche 9p qui est ce qui avait fait echouer les tentatives precedentes.

Lean (version 4.33.0, x86_64-unknown-linux-gnu, commit d8b18978322de05a8f3dba51ef03cf5461676c17, Release)
lean-toolchain          leanprover/lean4:v4.33.0
mathlib HEAD            db584cd6d46c92f209a44c0f1c829460d327499d

Build completed successfully (8712 jobs).   exit 0

C'est la verification tierce que la limite honnete de NanoClaw appelait (« je ne peux pas re-executer lake build ici »). Le lake build SUCCESS du body n'est plus une affirmation de lane : il est reproduit.

Merge.