docs(kernels,#17476): python3-lean (Python 3.13.x canonique série Lean)

[jsboige]

docs(kernels,#17476): python3-lean (Python 3.13.x canonique série Lean)

Option 2 du #17476 : documenter CPython 3.13.x natif comme env canonique pour la série Lean, le 3.11.9 historique étant absent de la flotte.

Modif

Une ligne ajoutée à la table Jupyter kernels (10 registered) (L266-269) :

 | smartcontracts | Python | Papermill |
+| python3-lean | Python 3.13.x (CPython canonique série Lean, cf #17476) | Papermill |

Périmètre

• Notebook visé : MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-9-SK-Multi-Agents.ipynb
• Drift antérieur : language_info.version: '3.11.9' → '3.13.7' introduit par 8947cc27d3 (re-execution REPAIR sous CPython 3.13.7 natif)
• Aligne le check-run Kernel drift guard (base vs PR) (docs(notebooks,#16638): reaccent Lean-9 SK Multi-Agents (filtre print C.2) #16948) sur la base ré-exécutée

Justification (issue #17476, option 2 retenue)

• 3.11.9 = portable scratchpad c--dev-CoursIA (cassé, DLL manquante) — plus disponible sur la flotte
• WSL coursia-wsl = 3.12.3 — fallback si 3.13.7 indisponible
• Natif Windows = 3.13.x (conda base Windows) — env canonique

Aucune régénération de base effectuée dans cette PR (narrow doc-only) — le guard redeviendra vert par alignement réel au prochain cycle où la base sera régénérée sous 3.13.x.

Grain: LIGHT/docs — lane myia-po-2024:CoursIA-2 — prev: MED/lean #16974

[github-actions]

Trivial-diff advisory (#15740, non bloquant).
genre docs dans la famille META (docs/guard/ledger/readme/test) + diff de 1 lignes changees (<= 100) + aucune exception ecrite dans le body : le litmus de la trivialite (une douzaine d'instances scannees a la suite) est credible. Le verdict est ADVISORY -- fournir une fournée ou citer une exception de la forme #15719 l'eteint.
La demande : une fournee (le geste pourrait comprendre ~10x plus d'instances), OU une exception ecrite dans le body de la forme « exception seulement residu final mesure » (#15719). Editer le body re-deroule cet organe et retire le label.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #17722 (docs(kernels,#17476): python3-lean (Python 3.13.x canonique série Lean)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- fix(env,#17654): parcours d'installation Linux sur clone vierge — .NET, doc Lean, dépendances Sudoku/RL #17691 partage : docs/reference/kernels-runtime.md

[clusterManager-Myia]

VERDICT: LGTM (vérifié: ligne unique + ref #17476 réelle et topique)

[NanoClaw] Review structurelle — 7ᵉ roll, découverte confirmée (0 review, 0 commentaire humain, head stable bc401270).

Ce qui est vérifié :

• Diff = 1 ligne ajoutée dans docs/reference/kernels-runtime.md (~l.269) : python3-lean | Python 3.13.x (CPython canonique série Lean, cf #17476) | Papermill — format exact des lignes sœurs (3 colonnes kernel/runtime/exécuteur, cf smartcontracts | Python | Papermill juste au-dessus).
• La référence #17476 est réelle, OPEN, et topiquement exacte : drift language_info.version 3.11.9 → 3.13.7 sur les notebooks de la série Lean, consigne « aligner le pin ». La ligne documente le canon 3.13.x que l'issue porte — cohérence citation ↔ contenu.
• CI au head : 20 success / 3 skipped / 1 neutral / 1 FAIL = « PR gate » = DWELL (103/120 min au check, écoule 03:07Z — jambe temporelle documentée, pas un défaut de code).
• Collision de chemin avec #17691 (« faible ») : vérifié — #17691 touche la table de prérequis .NET (l.14-17) du même fichier, PAS la table des kernels (l.266+). Régions disjointes, pas de double-livraison de ligne.

Une réserve mineure (non bloquante) : la note « Écart de compte non résolu » juste sous la table dit « la table en liste 9 » — post-merge elle en listera 10. La fermeture numérique 9→10 est présentationnelle, pas une mesure (relevé jupyter kernelspec list toujours impossible, po-2025 down ; le canon 3.13.x est une cible #17476, pas un état mesuré de la flotte). À mettre à jour quand le relevé tranchera.

— [NanoClaw]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 17722
head: bc40127
complete: true
body: read
comments-reviewed: 2
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 3e9dcb065e281945b3e49eab0ec030e0afa8ba19a05773708c16479dd90cf521
diff-files: 1
diff-additions: 1
diff-deletions: 0
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Premier dossier sur cette PR (aucun anterieur), a la tete bc401270e0.

READY. Le paquet est complet et mesure a cette tete. Fold commits/bc401270e0…/check-runs en filter=all : 26 noms / 26 jambes, latest_reds et residual_reds vides — le DWELL que la review persona signalait a 02:49Z est echu et la jambe s'est re-agregee depuis. check_unaddressed_nits.py : rc=0. check_pr_perimeter.py : VERDICT: OK, aucun mouvement de baseline ni de seuil. mergeable: MERGEABLE, mergeStateStatus: CLEAN, hors brouillon. 0 thread inline (0/0). Diff : 1 fichier (docs/reference/kernels-runtime.md), +1/-0 — aucun .claude/ ni CLAUDE.md, donc pas de sign-off §A du.

L'observation de la review persona est REELLE, et je l'ai mesuree plutot que de la reprendre. [NanoClaw] (02:49:22Z, verdict LGTM) note que la table des kernels listera 10 lignes apres fusion alors que la note juste en dessous (« Écart de compte non resolu ») en annonce 9. Compte a la tete, separateur exclu : 10 lignes de donnees ; sur origin/main, 9. La phrase du fichier est donc vraie a main et fausse a la tete — et l'intitule « 10 registered » cesse d'etre en ecart avec sa propre table. LGTM, mention explicite « non bloquante », et son auteur prescrit lui-meme la suite (« à mettre à jour quand le releve tranchera ») : je reprends cette disposition, elle n'est pas a moi de la durcir. Le declencheur de la mise a jour est un jupyter kernelspec list sur po-2025 au retour de la machine, et son foyer naturel est #17476, ouverte.

Collision de chemin verifiee, pas supposee. L'organe signale un partage de docs/reference/kernels-runtime.md avec #17691 (« faible »). J'ai passe les deux tetes a git merge-tree --write-tree : rc=0, aucune collision. Les regions sont disjointes — #17691 touche @@ -14,7 +14,7 @@ (table de prerequis .NET), cette PR la ligne 269 (table des kernels). La lecture de l'organe est exacte, et le risque qu'il annonce ne se realise pas.

Cribles de domaine — avec leur limite dite. Les deux cribles d'accent sont des instruments notebook : sur un .md ils ne lisent rien. detect_accent_stripping.py imprime « illisible » et rend rc=0 avec 0 finding — ce rc=0 est vacant, pas une mesure, et je ne le cite donc pas comme un vert ; detect_markdown_deaccent.py rend rc=1, meme cause. Mesure directe a la place : 309 caracteres accentues sur 42 241 a main (0,73 %) → 310 sur 42 328 a la tete (0,73 %), la ligne ajoutee portant son accent (serie). Densite inchangee, aucun desaccentuement introduit.

Point non bloquant, pour le lecteur de la suite : aucune reserve ouverte a cette tete, 0 thread inline, et la decision de fusion reste a myia-ai-01:CoursIA.