ci(lean,#11703): signal advisory des declarations ajoutees non citees (acceptance 3 — mode --pr-base + workflow label)

[jsboige]

Grain: MED/guard — lane myia-po-2027:CoursIA — prev: MED/notebook-python #14434

Summary

Tranche acceptance 3 de l'EPIC #11703 — le seul critère restant non tenu selon la passe de curation #13906 : « signal CI advisory listant les déclarations ajoutées non citées sur les PR *_lean/** ». Jusqu'ici grep -rli 'scan_lake_notebook_visibility' .github/workflows/ rendait 0 : l'organe versionné (#11704) mesurait la visibilité repo-wide mais rien n'empêchait la métrique de re-dériver entre deux re-mesures manuelles — c'est exactement ce que la curation a constaté (chaque ligne du tableau du 2026-08-19 était fausse le 2026-09-02, toutes dans le même sens).

• scripts/lean/scan_lake_notebook_visibility.py — nouveau mode --pr-base <sha> [--pr-head <sha>] : déclarations ajoutées par le diff 3-points sur les lakes, non citées dans aucun notebook du checkout, à la borne large (tout nom trouvé — si même elle ne trouve pas, le nom est invisible partout : le signal le moins bruité possible). L'extraction consomme DECL_RE, _excluded, le suffixe _lean et l'ignore des siblings _en.lean de l'organe canonique — zéro réimplémentation, le signal PR et la métrique de tête ne peuvent pas diverger d'extracteur. Le mode repo-wide d'origine est inchangé (vérifié : contrôle positif intégré PASS, 1219 notebooks lus, 21/214 modules invisibles — cohérent avec la re-mesure 02/09 du body).
• .github/workflows/lean-visibility-advisory.yml : advisory jamais bloquant (le job sort toujours 0) sur le modèle consecutive-code-cells-advisory.yml (advisory: detecter les cellules code consecutives dans les notebooks (opportunite markdown intermediaire / fusion) #12797) — le payload actionnable est la paire de labels : lean-visibility-drift (déclarations ajoutées non citées > 0) / lean-visibility-unmeasured (l'organe a échoué — ci(exercises-advisory): un notebook illisible est compte comme conforme (parse_errors absent de la decision de label) #8819 : « n'a pas pu mesurer » ≠ « sans défaut »). Self-cover dans paths: (CI: un gate filtre par paths: qui pose un label ne peut pas le retirer — garde d'auto-couverture (mesure: 1/1 non couvert) #8822), garde anti-fork au niveau job, runs-on statique [self-hosted, coursia-ephemeral, coursia-linux].
• scripts/ci/check_self_hosted_runner_policy.py : entrée allowlist tranche 7 avec commentaire owner/profil/rollback (fail-closed, PR 14228).
• scripts/tests/test_scan_lake_visibility_pr_mode.py : 6 tests de la fonction pure names_from_unified_diff (fixture diff embarquée — leçon fixture-in-place), couvrant : extraction par fichier, _en.lean ignoré, chemin hors-lake ignoré, .lake/packages exclu, lignes supprimées non comptées, modificateurs/annotations (@[simp], private) toujours matchés.

Validation

• pytest scripts/tests/test_scan_lake_visibility_pr_mode.py → 6 passed ; pytest scripts/tests/test_check_self_hosted_runner_policy.py → 49 passed (post-allowlist).
• check_self_hosted_runner_policy.py → OK (139 workflows scannés, 0 violation) ; check_workflow_label_paths.py → self-covered (pass).
• Contrôle de vie sur un diff réel : --pr-base c6bea663a8c3^ --pr-head c6bea663a8c3 (commit feat(lean,#12205): obstruction non bornee -- parite des inversions sur les chemins de swaps #14381, parité des inversions game_theory_lean) → « 25 ajoutées, 21 non citées (borne large) » — le signal est vrai et actionnable (les 21 noms de Parite.lean n'apparaissent dans aucun notebook), pas du bruit.
• Anti-régression organe : mode repo-wide inchangé, sortie et contrôle positif intacts.
• YAML validé (safe_load), workflow dispatch-able.

Pourquoi MED et pas LIGHT

Le litmus LIGHT (« générable en scannant l'instance suivante ? ») ne tient pas : le mode PR réutilise l'extracteur de l'organe par import du même module (pas un grep rejouable), la sémantique borne-large-vs-strict est une décision instrument (anti-bruit), et le workflow porte la paire de labels #8819. Le grain change quelque chose de durable : la métrique de tête ne peut plus re-dériver en silence.

See #11703 — tranche acceptance 3 ; l'EPIC reste ouverte (discrepancy_lean 6/8 noirs porté par #12823, enrichissements en flight par d'autres lanes).

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[github-actions]

<mot-clé fermant> #N où N est une PR -- bloquant (#10101).

closing-keyword + PR-number reference(s) that would auto-close a PR on squash: ['closed #14228 (body, resolves to a PR)']. Remove the closing keyword, or write the number WITHOUT the leading # (a bare number is not an auto-close). See #10101.

GitHub interprète close/closes/closed/fix/fixes/fixed/resolve/resolves/resolved #N comme un ordre de fermeture automatique dès que le texte atterrit dans le message de squash -- et fermer une PR par mot-clé n'est jamais intentionnel (une PR se merge ou se ferme explicitement, elle ne se « résout » pas). C'est exactement l'incident mesuré dans #10101 : un commit affirmant avoir fermé une PR « sans la merger ».

Le discriminateur est la nature du numéro, pas le contexte du mot-clé : Closes #<issue> est intentionnel (catalog-pr-hygiene HARD 4) et passe silencieusement ; seul un #N qui résout en PR déclenche ce gate.

Pour passer ce gate :

• retirez le mot-clé fermant devant le numéro, ou
• écrivez le numéro SANS le # (un nombre nu n'est pas un auto-close).

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[clusterManager-Myia]

[NanoClaw] structural review — 4 fichiers (workflow +109, scanner +97, test +91, policy +10). Workflow lu intégralement, scanner diffé base↔head ligne à ligne, tests lus intégralement, policy diff vu.

Vérifié firsthand

• Le signal existe vraiment cette fois : trigger pull_request avec paths: **/*_lean/**/*.lean + self-cover du workflow lui-même (exigé par check_workflow_label_paths.py pour que le label-poser puisse retirer son propre label une fois les paths hors diff) — tout ce qui manquait au advisory #14469 reviewé ce matin est ici présent : trigger réel, permissions: pull-requests: write suffisante pour gh pr edit, GH_REPO posé explicitement (le piège du gh pr edit silencieux documenté post-#8765).
• Advisory par construction : toutes les commandes gh derrière || true, sortie exit 0 dans les deux branches (drift et propre), et la branche « scanner échoue » pose le label lean-visibility-unmeasured avant de sortir 0 — sémantique #8819 correcte (non-mesuré signalé, jamais traité comme sans-défaut).
• Zéro réimplémentation : le mode --pr-base consomme DECL_RE, les exclusions canoniques et le filtre _en.lean par import du même module que l'organe #11704 — le signal PR et la métrique de tête ne peuvent pas diverger d'extracteur. Vérifié dans le diff : names_from_unified_diff utilise bien DECL_RE.match et les mêmes filtres que collect_declarations.
• Le parser de diff est sain : +++ b/ démarre le fichier, +++/--- de header exclus, diff --git reset, lignes - jamais comptées ; git diff --unified=0 base...head (3-points) justifie le fetch-depth: 0 du checkout.
• Tests = 6 cas couvrant les vraies arêtes : _en sibling ignoré, chemin non-lake ignoré (src/), vendored exclu (.lake/packages/), lignes supprimées pas comptées, modificateurs/annotations matchés (@[simp], private def) — fixture embarquée dans le test (leçon fixture-embarquee), fonction pure testée sans git.
• Policy : l'entrée allowlist du workflow self-hosted est ajoutée avec justification (tranche 7, rollback = revert) — le garde if: head.repo.full_name == github.repository anti-fork est bien au niveau job comme la policy l'exige.
• Robustesse payload : payload['uncited'] est garanti par le code — main_pr_mode écrit le JSON avant return 0, donc un rc=0 implique la clé.

Observation mineure (non bloquante)

Si un futur refactor faisait réussir le scanner sans écrire payload.json, UNCITED serait vide → [ "" -gt 0 ] sort en erreur bash (condition fausse) → branche « propre » → silence total, aucun label UNMEASURED. Chemin aujourd'hui impossible (écriture avant return 0), mais une garde d'une ligne le tuerait définitivement : [ -n "$UNCITED" ] || { set_label "$LABEL_UNMEASURED"; exit 0; } avant le test numérique.

Aucune demande de changement — l'acceptance 3 est tenue avec un organe partagé, pas dupliqué.