From 63e33fcc2ad3da86a6752ced790daad4674ad7c2 Mon Sep 17 00:00:00 2001 From: jsboige Date: Mon, 21 Sep 2026 19:13:31 +0200 Subject: [PATCH] feat(ci,#17097): mesure stable de la couverture proof-integrity des workflows Lean Le script scripts/ci/measure_proof_integrity_coverage.py produit la liste : - 12 workflows dedies cablant lean-axiom.yml - 4 workflows non cables (lean-build, lean-ci-matrix, lean-i18n-drift, lean-visibility-advisory) - 0 lakes ayant perdu leur gate par suppression - 19 lakes du manifest ci_lakes.json sans gate proof-integrity La sortie est stable et reproductible, ce qui permet a un reviewer de trancher B.3 (pr-review-discipline.md) sans enqueter. docs/reference/lean-proof-integrity-coverage.md documente la mesure au 2026-09-21, le statut par lake, la recommandation, et un critere de reexecution. Issue de suivi a ouvrir pour le fix (cablage lean-axiom sur les 19 lakes du manifest). Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../lean-proof-integrity-coverage.md | 111 +++++++++++++++ .../ci/measure_proof_integrity_coverage.py | 126 ++++++++++++++++++ 2 files changed, 237 insertions(+) create mode 100644 docs/reference/lean-proof-integrity-coverage.md create mode 100644 scripts/ci/measure_proof_integrity_coverage.py diff --git a/docs/reference/lean-proof-integrity-coverage.md b/docs/reference/lean-proof-integrity-coverage.md new file mode 100644 index 0000000000..2c9627d1a5 --- /dev/null +++ b/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 diff --git a/scripts/ci/measure_proof_integrity_coverage.py b/scripts/ci/measure_proof_integrity_coverage.py new file mode 100644 index 0000000000..b1f895244d --- /dev/null +++ b/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()