Repository navigation
Search-03e : 3 sorties committées affichent le théorème fantôme consistent_implies_admissible — ré-exécuter après #16677 #16705
Description
Ce qui se passe
Search-03e-AStar-Optimality.ipynb imprime le contenu des fichiers .lean avec numéros de
ligne. Trois de ses sorties affichent donc, mot pour mot, des lignes de commentaire de
search_lean/Astar/Consistency.lean :
| Emplacement | Extrait de la sortie committée |
|---|---|
cell[9].out[0] (stream) |
…La consistance implique l'admissibilité (`consistent_implies_admissible`), et garantit… |
cell[15].out[0] (stream) |
9 | Issue #4048, théorème cible `consistent_implies_admissible`. La **consistance**… |
cell[15].out[0] (stream) |
46 | (`consistent_implies_admissible`). Une heuristique **consistante** nulle au but… |
PR #16677 renomme précisément ces lignes-là dans Consistency.lean (et son sibling _en), vers
consistent_implies_admissible_bound. Avant elle, source et sortie concordaient. Après elle,
la sortie committée du notebook affiche un nom que le fichier source ne contient plus.
Le nom nu est un fantôme : seules deux déclarations existent dans tout le dépôt, et les deux portent
_bound —
search_lean/Astar/Consistency.lean:95: theorem consistent_implies_admissible_bound (h : V → NNReal) (goal : V)
search_lean/Astar/Consistency_en.lean:103: theorem consistent_implies_admissible_bound (h : V → NNReal) (goal : V)
Le notebook est la surface la plus lue par les étudiants : c'est exactement la confusion que #16651
existe pour supprimer, et c'est le dernier endroit où elle survit.
Ce qu'il ne faut PAS faire
Ne pas éditer les sorties à la main. Ce sont des outputs — le compte rendu de ce que le code a
réellement imprimé. Les maquiller est interdit (secrets-hygiene.md règle 6 : corriger la cause et
ré-exécuter) et, ici, le matériel resauterait au prochain passage kernel puisque la cause est en
amont, dans le .lean.
Ce qu'il faut faire
Ré-exécuter MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb après
le merge de #16677, pour que les sorties réaffichent le contenu réel des fichiers Lean. Committer
les sorties réelles (C.2). Toolchain Lean requis — règle F : on installe, on ne contourne pas.
Vérifier la mort de cette issue :
git grep -cE 'consistent_implies_admissible([^_]|$)' origin/main \
-- 'MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb'→ doit rendre 0. Aujourd'hui : 3.
Hors périmètre, signalé et non traité
.github/workflows/lean-search.yml:6 porte aussi le nom fantôme, dans un commentaire d'en-tête
(« phase-2 consistent_implies_admissible (téléscopage) »), pas dans une cible de gate — aucun
organe ne s'appuie dessus. À corriger en passant si quelqu'un touche ce fichier ; ne justifie pas
une PR à soi seul (§E : docs < 20 lignes, groupement exigé).
Ouverte avant le merge de #16677, dont elle lève la réserve de périmètre.
Activity
fix(search,#16705): re-executer Search-03e post-#16677 - nom fantome …
jsboige commentedon Sep 18, 2026
[CLAIMED] lane myia-po-2023:CoursIA — 2026-09-18T23:05Z — paths: MyIA.AI.Notebooks/Search/Part1-Foundations/Search-03e-AStar-Optimality.ipynb
Préflight : #16677 MERGED (15:09:43Z) — la réserve de périmètre est levée. Le notebook tourne sur kernel python3 et lit les sources
.leandirectement (convention Lean-15 :lake env leanexplicitement évité — la dernière exécution committée provient de cette machine,D:\Dev\CoursIA-14893-rename, outputs réels). Aucun build lake requis ni tenté (interdit machine, et non nécessaire au livrable : les cellules fantômedisplay_lean_module('Heuristic'/'Consistency')sont de la lecture de fichiers).Plan : worktree frais sur origin/main → re-exécution complète batch-mode → vérification de mort (
git grep -cE 'consistent_implies_admissible([^_]|$)' -- <nb>→ 0, actuellement 3) → commit outputs réels (C.2) → PRCloses #16705.Le commentaire d'en-tête
lean-search.ymlreste hors périmètre (§E) — signalé, non traité.jsboige commentedon Sep 18, 2026
[DELIVERED] PR #16740 — ré-exécution complète Search-03e (kernel python3, lecture directe des fichiers, zéro build lake, convention Lean-15) : 12/12 cellules, 0 erreur, 0 fuite. Check de mort : 3 → 1 ; les 2 fantômes stale éteints ; la résiduelle = affichage exact du commentaire délibéré
Consistency.leanL9 (rédigé par #16677 : « cible :consistent_implies_admissible— prouvé sous le nom_bound») — elle survit à toute ré-exécution tant que le source la porte, l'extindre = éditer la prose du.lean(hors périmètre). Outputs = source, vérifié ligne à ligne. — lane myia-po-2023:CoursIA 2026-09-18T23:15Zfix(search,#16705): re-executer Search-03e post-#16677 - nom fantome …