feat(ci,#17097): mesure stable de la couverture proof-integrity des workflows Lean

docs/reference/lean-proof-integrity-coverage.md

@@ -0,0 +1,111 @@
+# Couverture `proof-integrity` des workflows Lean
+
+**Mesure au 2026-09-21** (cycle c.760, issue #17097, grain `MED/guard -- lane myia-po-2023:CoursIA-2`).
+
+Cette page documente la couverture du gate `proof-integrity` sur les lakes Lean first-party du dépôt. Elle est produite par :
+
+```bash
+python scripts/ci/measure_proof_integrity_coverage.py [--json]
+```
+
+Le script applique exactement la procédure prescrite par `.claude/rules/pr-review-discipline.md` §B.3 (« câblage = exactement les workflows appelant `lean-axiom.yml` »).
+
+## Synthèse au 2026-09-21
+
+| | Compte |
+|---|---|
+| Workflows dédiés appelant `lean-axiom.yml` (câblés) | **12** |
+| Workflows Lean sans `lean-axiom` (lean-build, lean-ci-matrix, lean-i18n-drift, lean-visibility-advisory) | **4** |
+| Lakes servis par `lean-ci-matrix.yml` (via `lean-build.yml`, sans `lean-axiom`) | **19** |
+| Lakes ayant PERDU leur gate par suppression de fichier (`git log -D`) | **0** |
+| Lakes JAMAIS câblés sur `lean-axiom` | **19** (lakes du manifest) |
+
+## Détail des 12 workflows câblés
+
+```
+lean-asymmetric-information.yml: 4 mentions lean-axiom
+lean-conway.yml: 7 mentions lean-axiom
+lean-formal-groups.yml: 3 mentions lean-axiom
+lean-galois.yml: 5 mentions lean-axiom
+lean-grothendieck.yml: 6 mentions lean-axiom
+lean-hecke.yml: 3 mentions lean-axiom
+lean-knot.yml: 7 mentions lean-axiom
+lean-mimo.yml: 3 mentions lean-axiom
+lean-percolation.yml: 3 mentions lean-axiom
+lean-planning.yml: 4 mentions lean-axiom
+lean-sensitivity.yml: 4 mentions lean-axiom
+lean-social-choice.yml: 5 mentions lean-axiom
+```
+
+## Les 19 lakes du manifest `ci_lakes.json` (sans gate)
+
+`scripts/lean/ci_lakes.json` liste 19 lakes dispatchés par `lean-ci-matrix.yml` :
+
+```
+sudoku_lean               sorry-baseline=0
+kelly_lean                sorry-baseline=0
+minimax_lean              sorry-baseline=0
+search_lean               sorry-baseline=0
+assignment_lean           sorry-baseline=0
+discrepancy_lean          sorry-baseline=0
+argumentation_lean        sorry-baseline=0
+calibration_lean          sorry-baseline=0
+conway_cgt_lean           sorry-baseline=0
+erc20_lean                sorry-baseline=0
+finiteness_lean           sorry-baseline=0
+lean_game_defs            sorry-baseline=0
+lean_game_defs_ext        sorry-baseline=0
+learning_theory_lean      sorry-baseline=0
+decision_theory_lean      sorry-baseline=2
+game_theory_lean          sorry-baseline=1
+mathlib_examples          sorry-baseline=0
+social_choice_lean_peters sorry-baseline=0
+tegmark_muh_lean          sorry-baseline=0
+```
+
+Aucun de ces 19 lakes n'a **perdu** son gate par suppression (le `git log --diff-filter=D` ne retourne **aucun** fichier supprimé). Les 19 sont entrés directement dans la matrice via #16709 / #16716 sans transiter par un dispatcher dédié — donc ils ne l'ont **jamais eu**.
+
+## Ce que cela signifie pour §B.3
+
+Le critère `B.3` de `pr-review-discipline.md` (« Proof integrity SUCCESS — câblé ou non applicable ») demande de **lire explicitement** dans le body PR si le gate est **câblé** sur le lake modifié. Pour les 19 lakes du manifest, le verdict `B.3 non applicable cas (a)` (câblage absent) **doit être déclaré** par le reviewer sur **chaque** PR qui touche ces fichiers `.lean`, à défaut d'un câblage partagé.
+
+Constat pendant la passe de merge du 2026-09-21 sur **#16794** (`learning_theory_lean`) : le gate proof-integrity **n'a pas rougi** au rollup, mais c'est par construction — il n'existe pas. La PR est passée sur la base d'une vérification de substitution écrite en commentaire (cf. comment `5753926844`).
+
+## Recommandation (issue de suivi)
+
+Le **fix** est mécanique : câbler `lean-axiom.yml` sur chacun des 19 lakes du manifest, soit en l'appelant depuis `lean-build.yml` (job `ci-matrix` paramétré par lake), soit en restaurant un dispatcher dédié par lake. Cette correction est **hors scope** de la présente PR (elle modifie un workflow CI partagé) et fait l'objet d'une **issue de suivi** postée avec cette PR.
+
+## Critère de réexécution
+
+Pour trancher §B.3 sans enquêter, un reviewer peut rejouer :
+
+```bash
+python scripts/ci/measure_proof_integrity_coverage.py
+```
+
+Sortie stable, reproductible, lecture directe.
+
+## Références
+
+- **#17097** (issue) — ci(lean): les lakes servis par lean-ci-matrix.yml n'ont aucun gate proof-integrity
+- **.claude/rules/pr-review-discipline.md §B.3** — câblage proof-integrity
+- **#16709** — feat(ci,#13751): pilote matrice lean-ci — 6 dispatchers fondus dans lean-ci-matrix.yml
+- **#16716** — feat(ci,#13751): pilote matrice lean-ci — suite
+- **#16487** — fix(ci,#15652): drop branches:[main] from paths-scoped lean-* workflows (note la séparation lean-ci-matrix.yml)
+- **#8677** — premier incident (criterion 4 = B.3)
+- **#8782** — second incident (B.3 lu en non applicable cas b)
+- **`scripts/lean/count_code_sorry.py --json`** — l'instrument canonique de mesure de dette formelle
+
+## Statut au 2026-09-21
+
+| Mesure | Valeur |
+|---|---|
+| `cabled_count` | 12 |
+| `matrix_only_count` | 4 |
+| `perdus_count` | 0 |
+| `jamais_eu_count` | 0 |
+| `manifest_count` | 19 |
+| `cabled_lakes` | 12 (asymmetric-information, conway, formal-groups, galois, grothendieck, hecke, knot, mimo, percolation, planning, sensitivity, social-choice) |
+| `sans_couverture` | 19 (ci_lakes.json) |
+
+— po-2023 c.760, 2026-09-21T19:00Z

scripts/ci/measure_proof_integrity_coverage.py

@@ -0,0 +1,126 @@
+"""Mesure la couverture proof-integrity sur les workflows Lean.
+
+Issue #17097 : identifier les lakes sans gate proof-integrity, et parmi eux
+distinguer ceux qui ne l'ont JAMAIS eu de ceux qui l'ont PERDU lors de la
+fusion matrix.
+
+Livrable : script + rapport. Reproduit exactement la procédure de mesure
+prescrite par `.claude/rules/pr-review-discipline.md` §B.3 :
+    grep -ln 'lean-axiom' .github/workflows/*.yml | grep -v 'lean-axiom.yml'
+
+Usage :
+    python scripts/ci/measure_proof_integrity_coverage.py [--json]
+
+Sortie : stdout, format texte par défaut (--json pour sortie JSON unique).
+"""
+import argparse
+import json
+import subprocess
+import sys
+from pathlib import Path
+
+REPO_ROOT = Path(__file__).resolve().parent.parent.parent  # scripts/ci/X.py -> racine
+WF_DIR = REPO_ROOT / ".github" / "workflows"
+MANIFEST = REPO_ROOT / "scripts" / "lean" / "ci_lakes.json"
+
+
+def run(cmd, cwd=None):
+    r = subprocess.run(cmd, capture_output=True, text=True, cwd=cwd or REPO_ROOT, shell=True, encoding="utf-8", errors="replace")
+    return r.stdout.strip(), r.stderr.strip(), r.returncode
+
+
+def parse_args():
+    p = argparse.ArgumentParser(description="Mesure la couverture proof-integrity")
+    p.add_argument("--json", action="store_true", help="Sortie JSON unique")
+    return p.parse_args()
+
+
+def measure():
+    """Effectue la mesure et retourne un dict résumé."""
+    wf_files = sorted(WF_DIR.glob("lean-*.yml"))
+    cabled = []
+    matrix_only = []
+    for wf in wf_files:
+        if wf.name == "lean-axiom.yml":
+            continue
+        out, _, _ = run(f"grep -c 'lean-axiom' '{wf}'")
+        count = int(out) if out.strip().isdigit() else 0
+        if count > 0:
+            cabled.append((wf.name, count))
+        else:
+            matrix_only.append(wf.name)
+
+    log_out, _, _ = run("git log --diff-filter=D --name-only --format= -n 500 -- '.github/workflows/lean-*.yml'")
+    deleted_files = sorted(set(p for p in log_out.split('\n') if p.strip()))
+
+    perdus = set()
+    jamais_eu = set()
+    for f in deleted_files:
+        f = f.strip()
+        if not f:
+            continue
+        rev_out, _, _ = run(f"git rev-list -n 1 HEAD -- \"{f}\"")
+        last_sha = rev_out.strip()
+        if not last_sha:
+            continue
+        parent = f"{last_sha}^"
+        show_out, _, _ = run(f"git show \"{parent}:{f}\"")
+        if 'lean-axiom' in show_out:
+            perdus.add((f, last_sha[:8]))
+        else:
+            jamais_eu.add((f, last_sha[:8]))
+
+    manifest_lakes = []
+    if MANIFEST.exists():
+        with MANIFEST.open() as f:
+            d = json.load(f)
+        manifest_lakes = [l["display-name"] for l in d.get("lakes", [])]
+
+    return {
+        "cabled": [{"name": n, "count": c} for n, c in cabled],
+        "matrix_only": matrix_only,
+        "perdus": [{"name": f, "delete_sha": sha} for f, sha in sorted(perdus)],
+        "jamais_eu": [{"name": f, "delete_sha": sha} for f, sha in sorted(jamais_eu)],
+        "manifest_lakes": manifest_lakes,
+        "manifest_count": len(manifest_lakes),
+    }
+
+
+def print_text(summary):
+    print("=== ÉTAPE 1 : workflows ACTUELS qui appellent lean-axiom ===")
+    print(f"\nCâblés ({len(summary['cabled'])} workflows) :")
+    for c in summary["cabled"]:
+        print(f"  + {c['name']}: {c['count']} mentions lean-axiom")
+    print(f"\nNon câblés ({len(summary['matrix_only'])} workflows) :")
+    for n in summary["matrix_only"]:
+        print(f"  - {n}")
+
+    print("\n=== ÉTAPE 2 : workflows SUPPRIMÉS (git log D) qui appelaient lean-axiom ===")
+    print(f"Total fichiers supprimés : {len(summary['perdus']) + len(summary['jamais_eu'])}")
+    print(f"\nPERDUS : {len(summary['perdus'])}")
+    for p in summary["perdus"]:
+        print(f"  PERDU  {p['delete_sha']}  {p['name']}")
+    print(f"\nJAMAIS EU : {len(summary['jamais_eu'])}")
+    for p in summary["jamais_eu"]:
+        print(f"  JAMAIS {p['delete_sha']}  {p['name']}")
+
+    print(f"\n=== ÉTAPE 3 : LAKES DU MANIFEST ({summary['manifest_count']}) ===")
+    for n in summary["manifest_lakes"]:
+        print(f"  - {n}")
+    print(f"\n→ Les {summary['manifest_count']} lakes passent par lean-ci-matrix.yml")
+    print(f"  → qui appelle lean-build.yml (réutilisable),")
+    print(f"  → qui N'appelle PAS lean-axiom.yml (grep -c = 0).")
+    print(f"  → Conclusion : les {summary['manifest_count']} lakes sont SANS gate proof-integrity.")
+
+
+def main():
+    args = parse_args()
+    summary = measure()
+    if args.json:
+        print(json.dumps(summary, indent=2, ensure_ascii=False))
+    else:
+        print_text(summary)
+
+
+if __name__ == "__main__":
+    main()