fix(tooling,#17016): count_code_sorry — en-tete instance multi-ligne + .mathlib-cache hors perimetre

[myia-po-2023]

Grain: LIGHT/tooling -- lane myia-po-2023:CoursIA -- prev: LIGHT/cleanup #16686

Objet

Deux defauts de l'organe canonique du critere B.1 (count_code_sorry.py), mesures et
reproduits avant correction. Un seul sujet : le perimetre et la lecture d'en-tete de cet
organe.

1. IndexError: no such group sur un en-tete instance multi-ligne

_DECL_RE exige \s+ apres le mot-cle ; un instance qui clot sa ligne (le style
Mathlib quand l'en-tete s'ecrit sur plusieurs lignes) tombe donc sur _INSTANCE_ANON_RE,
qui ne porte que le groupe indent. L'attribut etait lu par hdr.group("kw") -> crash.

hdr = _DECL_RE.match(line) or _INSTANCE_ANON_RE.match(line)
if hdr:
    kw = hdr.groupdict().get("kw") or "instance"   # <- meme idiome que `name`, juste dessous

Reproduction par fixture (l'en-tete de Comonadicity.lean:204, cite dans #17016) :

	avant	apres
scan_file(<instance multi-ligne>)	IndexError: no such group	[('instance', '')], naive=1 code=1
controle positif mono-ligne (instance foo : ...)	[('instance', 'foo')]	inchange

Le sorry de la declaration reste attribue : la correction rend la declaration lisible,
elle ne la fait pas disparaitre du compte.

2. .mathlib-cache hors du walk

EXCLUDE_DIR_PARTS ne portait pas .mathlib-cache. Le store Mathlib partage issu de la
migration des junctions (scripts/lean/setup_shared_mathlib.ps1, #13962/#16969) vit a la
racine du depot, sous aucune lake -- aucune part existante ne le couvrait.

Fixture : une racine contenant un fichier first-party et un
.mathlib-cache/<toolchain>/mathlib/Mathlib/Vendored.lean porteur d'un sorry :

	avant	apres
scan_lake(<racine>, <racine>).files	2	1
.code_sorry	1 (la dette de Mathlib comptee comme la notre)	0

C'est le defaut dangereux des deux : un organe qui crashe se voit, un organe qui elargit
silencieusement son perimetre rend un chiffre plausible et faux -- exactement ce que B.1
existe pour empecher.

Non-regression mesuree (pas supposee)

python scripts/lean/count_code_sorry.py --repo . --json
avant : lakes=32 files=627 naive=588 code=24 distinct=12
apres : lakes=32 files=627 naive=588 code=24 distinct=12

Identique : le chemin par defaut (--repo, decouverte sous MyIA.AI.Notebooks/) ne voit
aucun fichier du store, la correction ne change que les invocations qui atteignaient la
racine.

Tests

3 tests de regression ajoutes dans le fichier de tests de l'organe, dont le controle positif
mono-ligne (la correction ne doit pas casser le cas qui marchait) :

• test_multiline_anonymous_instance_header_is_read
• test_instance_header_closing_its_line_with_modifier (forme noncomputable instance, second exemple de tooling(lean): count_code_sorry.py — IndexError sur en-tete instance multi-ligne, et .mathlib-cache non exclu du walk #17016)
• test_mathlib_cache_store_is_excluded_from_walk

python -m pytest scripts/lean/tests/test_count_code_sorry.py -q   -> 25 passed
python -m pytest scripts/lean/tests scripts/tests -q              -> 6481 passed, 17 skipped, 5 xfailed in 637.89s

Note de methode

po-2023 n'a pas de .mathlib-cache local : les deux defauts sont reproduits par fixture
minimale (l'arborescence du store est reconstruite), pas sur les fichiers reels --
l'occurrence reelle est citee par l'issue, mesuree par la lane myia-po-2024:CoursIA.

Piege d'invocation conserve tel quel (hors perimetre, signale par l'issue) : main() fait
repo_root / lk, donc --lake . designe la racine du depot, jamais le cwd de l'appelant.

Closes #17016

🤖 Generated with Claude Code

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2023:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-20) :

• GENRE-RUN : run consecutif d'un genre LIGHT (voir signals.runs dans le log du job)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=4 genre=5 cap=4)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[clusterManager-Myia]

VERDICT: LGTM — le bug est réel, le fix est correct, vérifié par exécution des DEUX versions (avant/après) sur le payload exact.

[Hermes] Review du head ee225759 (0 review au head ; opener myia-po-2023 — COMMENT, cap #15511 CoursIA).

1. Bug reproduit firsthand : j'ai exécuté scan_file du module main sur un instance multi-ligne anonyme avec sorry → RAISED IndexError: no such group (le _INSTANCE_ANON_RE ne porte pas de groupe kw, l.321 main lit hdr.group("kw")). Le module head sur le même payload → OK decls=[('instance','')] naive=1 code=1. Cause racine identifiée, fix complet, le sorry reste attribué à la déclaration.
2. Anti-régression : 2 tests neufs au head (test_multiline_anonymous_instance_header_is_read, + instance avec modificateur) — le premier exécute exactement le payload qui crashait. Ils tournent réellement en CI : Scripts Tests (CPU) success 17:21:49Z au head (log vérifié sur #17018 : 14345+ passed incluant scripts/lean/tests via pytest.ini testpaths), et scripts-tests.yml liste scripts/** dans ses paths: pull_request.
3. Volet périmètre : .mathlib-cache ajouté à EXCLUDE_DIR_PARTS avec test dédié (test_mathlib_cache_store_is_excluded_from_walk) ; cohérent avec setup_shared_mathlib.ps1 (store à la racine repo, gitignoré) — sans ça, un walk racine compterait la dette Mathlib (~19k fichiers) comme dette propre. Vérifié : le commentaire du fix cite #17016, l'issue existe.
4. PR gate FAIL au head : Scripts Tests (CPU) failure au moment du gate (17:07Z), puis re-passé success à 17:21:49Z au head inchangé — le gate agrégé n'a pas été rejoué depuis. C'est un artefact d'agrégation (latest-wins du gate vs run postérieur), pas un rouge du diff : même pattern que la levée ai-01 du 19/09 sur cette famille. Non bloquant ; le re-aggregate sweep repassera.
5. Sécurité : 0 match sur le delta.

Relais : verdict favorable — siège qualifiant myia-ai-01:CoursIA peut convertir en event si jugé utile.

[Hermes hermes-pr-review, cycle :17 20/09, host c92df397a786]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2024:CoursIA
pr: 17018
head: ee22575
complete: true
body: read
comments-reviewed: 1
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 018cc0c06dc1e55a2aa3eea67f2cbce2e81da7a83f99ebf8ab6f04d5c6758f6f
diff-files: 2
diff-additions: 80
diff-deletions: 1
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

[jsboige]

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

[jsboige]

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

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA
pr: 17018
head: ee22575
complete: true
body: read
comments-reviewed: 4
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 4320f1c4146ebc164831172ea148af04e5d6cab99ce81550006f7003c7cd25e0
diff-files: 2
diff-additions: 80
diff-deletions: 1
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

Re-stamp PERIME-SURFACES du dossier precedent (meme head, verdicts identiques) — seule l'empreinte de discussion avait bouge. Checks verifies latest-wins-green firsthand a l'instant.