Fix(notebooks): Search-07, Search-10, Sudoku-05 et Sudoku-13 C# sous Linux et macOS (PythonNetLoader, Z3NativeLoader)

[jsboige]

Hors flotte : PR de la session cloud d'agnosticisme du mainteneur (branche claude/*, exemption #17713, rôle décrit dans docs/reference/agent-cloud-agnosticisme.md). Pas de tag Grain:, pas de lane. See #17654, sous l'EPIC de parité Linux #10643. Suite de #19609, qui a introduit Config/PythonNetLoader.cs.

Summary

Quatre notebooks C# de Search et de Sudoku ne passent pas sous Linux sur main, ou n'y passent que par une copie locale de la résolution du CPython. Mesures sur un clone vierge Linux, version de main (6c3b4e983 pour Sudoku-05, dae4b07e4 pour les autres), avec les modules Python installés dans l'environnement actif et PYTHONNET_PYDLL non défini :

Notebook	Sur main
Sudoku-05	code 20 (pont mealpy) : FileNotFoundException: Aucun CPython avec mealpy trouve. La cellule ne cherche son CPython qu'à deux endroits, PYTHONNET_PYDLL et C:\ProgramData\miniconda3\python313.dll.
Search-07	code 6 (pont pyspiel) : InvalidOperationException: Variable d'environnement PYTHONNET_PYDLL absente.
Sudoku-13	code 5 (chargement de Z3) : DllNotFoundException: Unable to load shared library 'libz3'. Le .deploy du sous-module Z3.Linq ne contient que libz3.dll. Plus loin, le pont dd exige aussi PYTHONNET_PYDLL.
Search-10	au bout depuis #19000, mais par sa propre copie d'InitPythonFromInterpreter, que le chargeur partagé de #19609 a mise en commun.

Changes

Ponts PythonNet (4 notebooks). Dans chaque cellule pont, la résolution est remplacée par :

#load "../Config/PythonNetLoader.cs"        // "../../Config/…" depuis Search/Part1-Foundations/
PythonNetLoader.Initialize(typeof(PythonEngine).Assembly, "<module>");

Les modules demandés sont mealpy (Sudoku-05), automata (Search-10), pyspiel (Search-07) et dd (Sudoku-13). Le reste de chaque cellule est inchangé : instance, scope Python, budget, graines.

Le chargeur prend PYTHONNET_PYDLL s'il est défini. Sinon, il cherche dans les installations standard de Windows (dont C:\ProgramData\miniconda3, que l'ancienne liste de Sudoku-05 nommait), puis python3 et python du PATH, en retenant le premier interpréteur qui importe le module. Si aucun ne convient, il lève une erreur qui dit quoi installer ou définir.

using System.IO; ne sert plus dans les cellules de Search-10, Sudoku-05 et Sudoku-13 et en est retiré.

Z3 de Sudoku-13 (cellules 18 et 48). Les deux cellules chargent Microsoft.Z3 depuis le .deploy de Z3.Linq. Sous Windows, elles gardent leur résolveur, qui prend libz3.dll dans ce dossier. Ailleurs, elles appellent Z3NativeLoader.Register (SymbolicAI/SMT/Z3-API/Z3NativeLoader.cs, déjà utilisé par Sudoku-12, Search-10 et SC-04), qui charge la libz3 du paquet Python z3-solver, de Z3_LIBRARY_PATH ou du système.

Limite connue, inchangée : sous macOS Intel, Z3NativeLoader s'en remet à la bibliothèque native du paquet NuGet, absente quand Microsoft.Z3 vient du .deploy. Sudoku-13 n'y passait pas avant cette PR et n'y passe toujours pas.

Prose.

• Search-10, cellule 0 : la phrase des prérequis du pont nomme le chargeur, avec un lien relatif.
• Search-07, cellules 16 et 17 : les prérequis nomment le chargeur. Dans le tableau des verdicts, la ligne RECOVERABLE-USER-HAND passe de « Partiel : l'utilisateur doit définir PYTHONNET_PYDLL » à « Non : il suffit qu'un CPython installé importe pyspiel ».
• Sudoku-13, cellule 17 (note technique Z3) et cellule 52 (prérequis du pont dd) : elles nomment Z3NativeLoader.cs et PythonNetLoader.cs.

Allègement déclaré (ratchet Source-collapse, advisory). La cellule pont de Search-10 (8dc1e652) perd 2,7 k caractères (36 %). C'est la copie d'InitPythonFromInterpreter, déplacée dans Config/PythonNetLoader.cs, un autre fichier.

Registre de parité jumelle : les quatre paires (Search-07 MCTS-And-Beyond, Search-10 SymbolicAutomata, Sudoku-05 PSO, Sudoku-13 SymbolicAutomata) reçoivent chacune une attestation --update --by claude-cloud:hors-flotte, posée après les strips outillés.

Le diff compte 8 fichiers : 4 notebooks et 4 attestations.

Diagnostic dérive

Exécutions sous Linux, dotnet-interactive 1.0.712001, CPython 3.11.17 d'un environnement virtuel (mealpy 3.0.2, automata-lib, open_spiel 2.0.1, dd 0.6.0), PYTHONNET_PYDLL non défini. MetaGeneticSharp construit en local au commit épinglé (2b21a6a). Pour Sudoku-13, Z3_LIBRARY_PATH désigne la libz3.so de z3-solver==4.12.2.0, la version du Microsoft.Z3.dll du .deploy.

Notebook	main	cette branche
Sudoku-05	arrêt en code 20	21/21 cellules de code, 290 s
Search-07	arrêt en code 6	17/17, 63 s
Sudoku-13	arrêt en code 5	20/20, 89 s
Search-10	(déjà au bout sous Linux)	15/15, 22 s

Comparaison cellule par cellule avec main, sur le texte des sorties :

• Search-10 : identique, sauf la ligne du pont : CPython 3.11.17, contre 3.11.15 dans l'exécution Linux committée.
• Search-07 : résultats identiques. Actions choisies, valeurs MCTS, taux optimaux et de victoire, visites moyennes et tournoi de Nim ne changent pas, ni l'action = 4 du pont OpenSpiel. Changent les temps (cellules 9, 12, 22, 26, 41) et la version du pont : CPython 3.11.17 au lieu de 3.12.13.
• Sudoku-13 : résultats identiques. Grille témoin Z3, verdicts SAT, faux négatif de la grille B, contre-vérifications RE#, BDD (90 nœuds, 6 lignes valides, modèle (2, 1, 3)). Changent les temps et la ligne du pont (CPython 3.11.17 … [GCC 13.3.0] au lieu de 3.13.12 | packaged by Anaconda … [MSC v.1942 64 bit (AMD64)]). Sous Linux, l'annexe S10 n'imprime plus (resolver libz3 deja pose par la cellule de chargement Z3 …) : Z3NativeLoader réutilise son résolveur sans message, et cette ligne reste celle de la branche Windows.
• Sudoku-05, pont mealpy (cellule de code 20) : CPython 3.11.17 … [GCC 13.3.0], contre 3.13.5 | packaged by Anaconda sur la base Windows. Avec les mêmes graines, les conflits résiduels sont 7 / 8 / 10 (seeds 42 / 7 / 99), contre 7 / 6 / 5 sur la base. La cellule d'interprétation qui suit le prévoit déjà : les flux RNG de l'interpréteur embarqué divergent malgré des seeds identiques, et elle annonce « 5 à 10 conflits résiduels » côté pont, fourchette que les deux exécutions respectent.
• Sudoku-05, PSO canonique MGS (cellule de code 17) : 16 conflits restants, contre 5 sur la base. Cette cellule n'est pas seedée ; son interprétation parle d'un « plafond de conflits résiduels », sans chiffre.
• Sudoku-05, GeneticSharp (cellules de code 14 et 15) : la résolution réussit (76 générations contre 43, non seedée). La table finale de la comparaison est identique : mêmes comptes de grilles résolues, mêmes statuts Disqualified, temps au plafond de 15 s. La cellule 15 imprime davantage de lignes de progression (3,3 k caractères contre 0,6 k) : ses tentatives parallèles écrivent dans le même flux, et cette machine en enchaîne plus avant le plafond. check_output_flood.py : 0 regressed.
• Fins de ligne : les sorties de la base Windows finissent en \r\n, celles-ci en \n.
• Première cellule de code de Search-07 et Sudoku-13 : strip_probe_banner.py laisse le reste du script d'amorçage (dotnet-interactive-this-cell-$CACHE_BUSTER$) une fois les lignes probeAddresses retirées, comme dans Fix(notebooks): pont pysat de SocialChoice-01 C# sous Linux et macOS, ponts GT-06/07/13/17 et SC-04 sur PythonNetLoader #20566 et Fix(notebooks): ponts mealpy de MGS-22 a MGS-30 sous Linux et macOS (PythonNetLoader) #20604. 0 adresse IP et 0 signature de bannière.
• Identifiants de cellule : trois cellules de Search-07 (31 à 33) n'en avaient pas ; l'exécution leur en attribue, comme le veut nbformat 4.5.
• language_info.version de Search-07 : vide sur main, 13.0 après exécution, comme sur les trois autres notebooks. C'est ce que relève check_kernel_drift.py.

Prose contre sorties, base contre tête : check_markdown_claims_output.py 4 → 4 (Search-10), 0 → 0 (Sudoku-05), 8 → 6 (Search-07), 5 → 5 (Sudoku-13) ; check_stale_claims.py et check_factual_mislabel.py 0 → 0 sur les quatre ; check_machine_dep_timing.py 0 → 0 : aucune prose ne fige un temps.

Causes :

• (a) env/kernel : résolution du CPython et de libz3, objet de la PR. Verdict CAUSE_FIXED.
• (e) stochasticité : PSO canonique MGS et GeneticSharp ne sont pas seedés, et les flux RNG de mealpy divergent entre interpréteurs. La prose en tient déjà compte. Verdict CAUSE_INTRINSIC dans le périmètre de cette PR.
• (a) machine : temps, fins de ligne. Verdict CAUSE_INTRINSIC.

Aucune sortie n'a été touchée à la main.

Verdict SOTA : SOTA-OK. Les vrais mealpy, automata-lib, OpenSpiel, dd, Z3 et MetaGeneticSharp s'exécutent ; rien n'est substitué. Organe-first : rien n'est réimplémenté, quatre résolutions cèdent la place au chargeur partagé, et Sudoku-13 rejoint le chargeur Z3 de la série Z3-API.

Signalé

• fix(notebooks,#20167): retire execution_count/outputs des cellules markdown (lot C) #20595 retire des clés execution_count/outputs de cellules markdown dans Sudoku/Sudoku-05-PSO-Python.ipynb, le jumeau Python de Sudoku-05. Ce diff ne touche pas ce fichier. Si fix(notebooks,#20167): retire execution_count/outputs des cellules markdown (lot C) #20595 merge avant, l'attestation sudoku-05-pso posée ici enregistre l'ancien SHA du jumeau Python ; je la reposerai alors après rafraîchissement de la base.
• fix(search,#20547): analyse de convergence MCTS -- ensemble A* sur trois positions #20579 modifie Search/Part1-Foundations/Search-07-MCTS-And-Beyond.ipynb, le jumeau Python de Search-07 : même conséquence pour l'attestation search-07-mcts-and-beyond.
• Fix(notebooks,#20190): le strip probeAddresses retire l'enveloppe display_data vide #20262 retire l'enveloppe display_data vide de la première cellule de code de Search-07 et de Sudoku-13. Ces notebooks ré-exécutés n'en portent plus, donc la PR qui merge en second garde la version de la tête. Le recouvrement se limite à cette sortie.

Review Checklist

• 1. Scope : quatre cellules pont, deux cellules de chargement Z3, des phrases de prérequis, quatre attestations de parité.
• 2. Post-fix validation, relancée après le dernier commit :
  • validate_pr_notebooks.py : PASS (4/4) ;
  • check_output_failure_text.py, check_output_flood.py : 0 regressed ;
  • check_output_collapse.py : 0 flagged ;
  • check_source_collapse.py : 1 MAGNITUDE (Search-10), justifié ci-dessus ;
  • check_kernel_drift.py : Search-07 '' -> '13.0', documenté ci-dessus ;
  • check_papermill_ratchet.py : 0 regression ;
  • check_prose_quantitative_claims.py --diff … --strict : OK ;
  • check_cell_source_parses.py --target-py 3.12 --pr-diff : 0 finding ;
  • check_twin_parity.py --per-pair --check : 157 paires OK, INTRO=0 ; --verify-recorded-sha : les quatre paires OK, le seul MISMATCH restant porte sur App-10 Portfolio, que ce diff ne touche pas ; check_twin_index_collisions.py --head HEAD : OK ;
  • check_split_reading_cells.py, check_interp_positioning.py, strip_machine_paths.py --scan, detect_bare_cross_dir_load.py --check : 0 sur les 4 ;
  • scripts/check_docs_links.py --check : 0 nouveau lien cassé ;
  • detect_organ_duplication.py : CLEAN.
• 3. Pedagogical coherence : exercices et stubs inchangés.
• 4. Real execution : notebook_tools.py execute <nb> --kernel .net-csharp, 4 exécutions sur 4 au bout, 0 erreur. Puis strip_probe_banner.py --apply et scrub_papermill_paths.py --apply.
• 5. Regression check :
  • Sous Windows avec PYTHONNET_PYDLL défini, la bibliothèque désignée est chargée comme avant. Sans la variable, le chargeur parcourt les installations standard, dont C:\ProgramData\miniconda3. Sous Windows, les cellules Z3 de Sudoku-13 gardent leur résolveur .deploy à l'identique. Je l'ai déduit du code, sans l'exécuter sous Windows ni sous macOS.
  • Plus aucun InitPythonFromInterpreter, dllCandidates ni Runtime.PythonDLL dans les quatre notebooks (git grep).

Anti-regression

• Pas de Lean/Coq touché.
• Aucun test désactivé.
• Les suppressions sont les résolutions locales du CPython, remplacées par l'appel au chargeur partagé. Aucun calcul n'est retiré.

Notebook-specific

• Aucun raise NotImplementedError / assert False / 1/0 introduit.
• Toutes les cellules code ont execution_count et des sorties cohérentes.
• Seuls les notebooks dont une cellule source a changé sont committés (C.3).

Test plan

Sur Linux ou macOS, avec .NET, dotnet-interactive 1.0.712001, un python3 du PATH qui importe mealpy 3.0.2, open_spiel, dd 0.6.0 et z3-solver==4.12.2.0, et les sous-modules initialisés (git submodule update --init --recursive, puis dotnet build MyIA.AI.Notebooks/Search/MetaGeneticSharp/src/MetaGeneticSharp.Domain/MetaGeneticSharp.Domain.csproj) :

python3 scripts/notebook_tools/notebook_tools.py execute MyIA.AI.Notebooks/Sudoku/Sudoku-13-SymbolicAutomata-CSharp.ipynb --kernel .net-csharp
python3 scripts/notebook_tools/notebook_tools.py execute MyIA.AI.Notebooks/Search/Part1-Foundations/Search-07-MCTS-And-Beyond-CSharp.ipynb --kernel .net-csharp

Sudoku-13 doit afficher Z3 charge … Version Z3 4.12.2.0, puis Pont PythonNet : .NET -> CPython … -> dd.autoref.BDD. Search-07 doit afficher MCTSBot … action = 4. Sur main, ils s'arrêtent respectivement sur DllNotFoundException: … 'libz3' et sur PYTHONNET_PYDLL absente.

Environnement de mesure : conteneur Linux x64, 4 threads, clone vierge, hors flotte.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VuVMY5fhzd5cQhzHiyvjka

---

Generated by Claude Code

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

[github-actions]

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

[jsboige]

Mise à jour du 2026-10-15 vers 15:25 UTC. Les deux causes hors diff décrites ci-dessous (Scripts Tests et check-nav-chain) sont corrigées sur main par #20777 (398d019df), qui reprend le contenu de #20589 et #20704 ; ces deux PRs ont été fermées en conséquence. Vérifié localement sur main : check_notebook_nav_chain.py --check rend 0 nouveau constat, et test_full_repo_state_passes_parity passe. Base de cette PR rafraîchie par update-branch (fusion sans conflit, nouvelle tête b447e19a0). Ces deux jambes repasseront avec la CI de cette tête. La file Actions du dépôt reste saturée (environ 2 500 runs en attente), les jambes peuvent tarder.

Historique ci-dessous, conservé tel quel.

---

Mis à jour le 2026-10-15 vers 02:20 UTC. Tête : 38c946c9c (Search-07 et Sudoku-13 ajoutés).

Scripts Tests (CPU) en échec sur 565b9638a : la cause n'est pas dans ce diff. Sur 38c946c9c, la jambe n'a pas encore tourné ; elle échouera sur le même test tant que main n'aura pas reçu #20589.

Ce qui échoue : 1 test sur 18 985, scripts/translation/tests/test_check_translation_parity.py::test_full_repo_state_passes_parity. La paire 01-2-GPT-5-Image-Generation_en est en STRUCTURE_DRIFT : 37 cellules dans 01-2-GPT-5-Image-Generation.ipynb, 30 dans le jumeau anglais. Il manque au jumeau 8 cellules, dont nv-exo1-code à nv-exo3-md.

Pourquoi ce n'est pas cette PR : ce diff touche deux carnets C# (Search-10, Sudoku-05) et deux attestations de parité jumelle, ni GenAI ni les traductions. La dérive vient de #20551, mergée sur main. Je l'ai mesurée sur main à 1cef8a550 : 37 cellules contre 30. #20566 échoue sur le même test, pour la même raison.

Le correctif : #20589, encore ouverte, traduit les cellules manquantes et re-rend le jumeau anglais. Je ne la recopie pas ici : elle modifie le même fichier, et cette PR mêlerait alors GenAI et Search/Sudoku.

Relance : une relance sur la base actuelle rejouerait le même échec. Une fois #20589 mergée, je rafraîchis la base de cette PR, ce qui relance Scripts Tests.

Always-on guards -- 16 organes, 1 checkout en échec sur 38c946c9c (02:02 UTC) : 42 gardes sur 43 passent, seul check-nav-chain échoue, et la cause est sur main. Lancé localement, check_notebook_nav_chain.py --check rend 0 nouveau constat sur la branche, et 2 sur main à e33ffdfdb : [orphan_entry] sur ANALYSE-06-Sensibilite-2026-Lean-Python_en.ipynb (#20392) et ANALYSE-10-Reflexion-Thurston-Python.ipynb (#20429), rendus bloquants par la règle d'entrée intra-série de #20396. Le correctif existe : #20704, qui rattache ces deux carnets à la chaîne. Je ne le recopie pas ici : il touche deux carnets Lean/ANALYSE, hors du sujet de cette PR, et doublerait une PR en cours sur les mêmes fichiers. Une relance rejouerait la même fusion avec main ; la jambe repassera au rafraîchissement de base, après #20589 et #20704.

PR gate sur 38c946c9c : conclu STARVED à 21:13 UTC. Aucune de ses jambes n'a encore trouvé de runner sur le pool auto-hébergé. Le balayage pr-gate-stale-sweep.yml le rejoue quand les runners se libèrent, et je le rejoue moi-même une fois les jambes passées.

---

Generated by Claude Code

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	8.2s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	7.0s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	8.1s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	7.4s
Search-01-StateSpace.ipynb	✅ SUCCESS	9.9s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	4.7s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	16.3s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.0s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	10.9s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #20605 (Fix(notebooks): Search-07, Search-10, Sudoku-05 et Sudoku-13 C# sous Linux et macOS (PythonNetLoader, Z3NativeLoader)) 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(notebooks,#20190): le strip probeAddresses retire l'enveloppe display_data vide #20262 partage : MyIA.AI.Notebooks/Search/Part1-Foundations/Search-07-MCTS-And-Beyond-CSharp.ipynb, MyIA.AI.Notebooks/Sudoku/Sudoku-13-SymbolicAutomata-CSharp.ipynb

[github-actions]

Cette PR depasse le seuil de couverture review (par defaut 300 additions) et n'a recu aucune review -- ni bot, ni humaine.

Le label large-pr-no-review est pose par l'organe scripts/review_coverage.py porte par l'issue #11232. Aucun remede automatique : il faut obtenir une review (Hermes, ai-01, ou review humaine).

Le label est retire au balayage suivant (quotidien) des qu'une review arrive -- dans reviews[] ou en commentaire de verdict -- ou que le diff passe sous le seuil. Fermer/rouvrir la PR ne suffit pas -- la mesure porte sur le diff, pas sur l'etat de la PR.

Seuil, historique et exceptions : cf. docs/reference/review-coverage-threshold.md.