tooling(lean): count_code_sorry.py — IndexError sur en-tete instance multi-ligne, et .mathlib-cache non exclu du walk #17016

Constat (mesuré 2026-09-20, lane myia-po-2024:CoursIA)

L'organe canonique du critère B.1 (pr-review-discipline.md §B.1, evidence obligatoire de tout
body PR Lean) casse sur une invocation naturelle — et, là où il ne casse pas, il élargit son
périmètre au Mathlib vendu.

1. IndexError: no such group — en-tête instance multi-ligne

Repro (aucun lake requis) :

python scripts/lean/count_code_sorry.py --lake . --json
# Traceback ... count_code_sorry.py:358 in scan_lake
#              ... count_code_sorry.py:321 in scan_file
#   kw = hdr.group("kw")
# IndexError: no such group

Cause, dans scan_file :

318   hdr = _DECL_RE.match(line) or _INSTANCE_ANON_RE.match(line)
319   if hdr:
320       _flush_vacuous()
321       kw = hdr.group("kw")          # <- IndexError si hdr vient de la 2e regex

_DECL_RE porte le groupe nommé kw ; _INSTANCE_ANON_RE (^(?P<indent>\s*){_DECL_MODIFIERS}instance\b)
ne porte que indent. Or _DECL_RE exige \s+ après le mot-clé, donc il échoue dès que
instance est le dernier token de la ligne — l'anonyme gagne alors, et hdr.group("kw") lève.

Ce n'est pas un cas tordu : c'est le style Mathlib quand l'en-tête s'écrit sur plusieurs lignes.

-- .mathlib-cache/leanprover_lean4_v4.33.0-db584cd6/mathlib/Mathlib/CategoryTheory/Monad/Comonadicity.lean:204
instance
    [∀ A : adj.toComonad.Coalgebra, HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))]
    (B : C) : HasLimit (parallelPair ...)

-- .../Mathlib/Algebra/Category/ModuleCat/Colimits.lean:137
noncomputable instance
    [HasColimitsOfSize.{u, v} AddCommGrpMax.{w, w'}] :
    PreservesColimitsOfSize.{u, v} (forget₂ (ModuleCat.{max w w'} R) AddCommGrpCat) where

6 fichiers lèvent (scan_file appelé sur chaque). Tous sous .mathlib-cache, sous les deux
toolchains présents :

.mathlib-cache/leanprover_lean4_v4.33.0-db584cd6/mathlib/Mathlib/CategoryTheory/Monad/Comonadicity.lean
.mathlib-cache/leanprover_lean4_v4.33.0-db584cd6/mathlib/Mathlib/CategoryTheory/Monad/Monadicity.lean
.mathlib-cache/leanprover_lean4_v4.33.0-db584cd6/mathlib/Mathlib/Algebra/Category/ModuleCat/Colimits.lean
.mathlib-cache/leanprover_lean4_v4.32.1-520045ab/mathlib/Mathlib/CategoryTheory/Monad/Comonadicity.lean
.mathlib-cache/leanprover_lean4_v4.32.1-520045ab/mathlib/Mathlib/CategoryTheory/Monad/Monadicity.lean
.mathlib-cache/leanprover_lean4_v4.32.1-520045ab/mathlib/Mathlib/Algebra/Category/ModuleCat/Colimits.lean

Note de méthode : les occurrences du même motif dans les lakes first-party sont dans des
commentaires et disparaissent au strip_lean_comments (vérifié : knot_lean/Knots/Invariant.lean,
sudoku_lean/Sudoku.lean, GittinsTheorem_en.lean, Screening_en.lean, HashlifeMarginFragment_en.lean
passent scan_file sans lever). Ce sont bien les fichiers de .mathlib-cache qui déclenchent.

2. .mathlib-cache n'est pas exclu du walk

EXCLUDE_DIR_PARTS = (".lake", "_peters", "reference_docs", "foundry-lib")

Le store Mathlib partagé issu de la migration des junctions (scripts/lean/setup_shared_mathlib.ps1,
cf #13962/#16969) ne vit pas sous un lake : il est à la racine du dépôt, en
.mathlib-cache/<toolchain>-<rev>/mathlib/. Il n'est donc exclu par aucune part.

Conséquence mesurée : un walk sur la racine voit 19 337 fichiers .lean là où les lakes
first-party en comptent 626 (~31×). Au-delà du coût, un --lake <racine> qui aboutirait
compterait la dette de Mathlib comme celle du dépôt — un chiffre B.1 faux.

Le chemin par défaut (--repo <racine>, découverte sous MyIA.AI.Notebooks/) n'est pas touché :
c'est pourquoi --repo . --json passe et que --lake . casse.

3. Piège d'invocation (contexte, pas un défaut)

main() ligne 450 fait repo_root / lk pour un --lake relatif : --lake . désigne donc la
racine du dépôt, jamais le cwd de l'appelant. C'est ce qui m'a fait croire d'abord à un crash
sur un lake de 5 fichiers.

Correctif attendu (2 lignes)

1. EXCLUDE_DIR_PARTS += (".mathlib-cache",) ;
2. branche anonyme robuste : kw = hdr.groupdict().get("kw") or "instance" — ou faire porter
   (?P<kw>instance) à _INSTANCE_ANON_RE.

Acceptance

• python scripts/lean/count_code_sorry.py --lake . --json sort 0 et un JSON valide ;
• un --lake <racine> ne contient plus aucun fichier .mathlib-cache/** ;
• non-régression : --repo . rend les mêmes totaux qu'avant (626 fichiers first-party).

Pourquoi ça compte

Des deux défauts, c'est le second qui est dangereux : un organe qui crashe se voit et se
contourne ; un organe qui élargit silencieusement son périmètre rend un chiffre plausible et
faux — exactement ce que la règle B.1 existe pour empêcher (elle a déjà remplacé grep -c sorry par
cet organe parce que l'instrument artisanal sur-comptait la prose).

Rapporté par la lane myia-po-2024:CoursIA (worker). Mesuré firsthand le 2026-09-20 ; non corrigé
ici (un sujet par PR, et le correctif touche l'organe partagé).