Repository navigation
fix(guard,#15666): le detecteur de voies lake voit l'executable tenu dans une variable - #20014
Conversation
…dans une variable Les formes 1 et 2 du garde ne lisent que des **litteraux** : une voie qui resout son binaire une fois (`lake = _find_lake()`) puis l'execute (`[lake] + args.split()`) etait **invisible**. Mesure du 2026-10-09 sur `lean_notebook_utils.py` (case 1 de #15666) : le garde y voyait **1 invocation directe sur 3** -- les deux voies natives (L239, L291) echappaient, seule la f-string WSL (L299) etait signalee. Le cliquet ne pouvait donc pas voir une migration partielle laissant une voie native derriere elle, puisqu'il ne voyait pas la voie a retirer. Un motif de detection se valide par ses **faux negatifs** : celui-la rendait un chiffre plus petit et plus propre, jamais une erreur. - `_lake_holder_names` : noms lies a un executable lake, par `shutil.which("lake")` ou par un helper dont le nom porte `lake`. - Forme 2bis : tete de liste tenue par un de ces noms (position de commande, comme la forme 2 dont elle est le pendant). - 4 tests ajoutes (2 positifs, 2 negatifs) ; 28 passent. - Census inchange hors `lean_notebook_utils.py` : le verdict reste `OK` (le fichier est deja allowliste), +2 lignes detectees, 0 stale. Verdict `check_lake_direct_invocation.py --all --check` : rc=0. See #15666 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
|
[ADJOINT PREFLIGHT] |
2 participants
Grain: MED/guard — lane myia-po-2026:CoursIA — prev: LIGHT/guard #19978
Le defaut
Les formes 1 et 2 du garde
check_lake_direct_invocation.pyne lisent que des litteraux. Une voie qui resout son binaire une fois puis le reutilise etait donc invisible :Mesure du 2026-10-09 sur
MyIA.AI.Notebooks/SymbolicAI/Lean/lean_notebook_utils.py(case 1 de #15666) : 1 invocation directe detectee sur 3. Les deux voies natives (L239[lake] + args.split(), L291[lake, "env", "lean", str(tmp_path)]) echappaient ; seule la f-string WSL (L299) etait signalee.Pourquoi ca compte plus qu'un chiffre
Le garde est un cliquet : il empeche la reintroduction d'une voie directe. Or il ne voyait pas la voie que la migration doit retirer. Consequence concrete : une migration partielle qui routerait
run_lean_snippetmais laisseraitrun_lakeappellerlakeen direct rendraitrc=0et un census inchange — la dette survivrait, invisible, et l'allowlist serait meme signaleeSTALE(« allowlistee sans violation : migrer puis retirer l'entree »), invitant a retirer une entree encore due.C'est la forme exacte que la doctrine anti-regression decrit : un motif de detection se valide par ses faux negatifs, et celui-la rendait un chiffre plus petit et plus propre, jamais une erreur.
Le correctif
_lake_holder_names: ensemble des noms lies a un executablelake, par deux voies mesurees —shutil.which("lake")(la sonde de toolchain) et un appel a un helper dont le nom portelake(_find_lake()), qui est la forme reellement ecrite.Verification
lean_notebook_utils.py--all --checkOK, rc=0OK, rc=0STALEpython -m pytest scripts/lean/tests/test_check_lake_direct_invocation.py -q→ 28 passed.Les 4 tests tiennent les deux bouts : deux positifs (variable issue de
shutil.which, variable issue d'un helper_find_lake) et deux negatifs — la sondeshutil.which("lake")seule reste propre (sinon la forme 2bis fabriquerait le bruit que la forme 2 exclut deja), et une tete de liste tenue par une variable ordinaire (tool = "pytest") n'est pas signalee.Aucun autre fichier du depot n'est emporte : le rayon d'impact a ete mesure avant d'ecrire (une seule ligne de code reelle dans tout le depot, celle de
lean_notebook_utils.py).Ce que cette PR ne fait pas
Elle ne migre pas
lean_notebook_utils.pyvers l'organe canonique, bien que ce soit le case 1 de #15666 et l'objet de mon claim (c.6071904681). La mesure a montre que l'organe ne peut pas encore l'accueillir :lean_exec runderive son repertoire de travail dePath.cwd()(L992) et n'expose aucun--cwd, alors querun_lake/run_lean_snippetrecoivent des chemins WSL et querun_lean_snippetecrit son fichier temporaire dans WSL. Router ces voies exigerait une inversion de chemin et une reprise du temporaire sur une surface importee par tous les carnets Lean. Le blocage et l'ordre de migration sont mesures et consignes sur #15666.See #15666
🤖 Generated with Claude Code