feat(lean,#4362): full pin-tree identity scanner for lake manifests

[jsboige]

Grain: MED/tooling — lane myia-po-2024:CoursIA — prev: MED/guard #14586

Summary

Step-1 instrument of EPIC #4362: scripts/lean/compare_lake_manifests.py compares the complete pin tree ({package -> resolved rev}) of every lake-manifest.json outside .lake/packages/, not just the Mathlib rev the 2026-09-01 re-read measured. Sharing checkouts (#4363) or a warm pool volume (#14337) requires the full tree to be identical — two lakes with the same Mathlib rev but different batteries revs cannot share a checkout.

• Clusters lakes by pin-tree identity (sha256 of the sorted pins), elects the largest non-empty cluster as reference, reports each divergent lake with the exact package/rev pairs that differ; no-dependency lakes form their own class (not "divergent").
• Exclusions documented in-module with their reasons: conway_cgt_lean (transitive upstream pin vihdzp/combinatorial-games, docs(lean,#4980): conway_cgt_lean/CGTTour_en sibling (namespace CGTTour_en, EN docstrings) #6116/docs(gametheory,#13138): reconcile Lean inventory with effective pins post-convergence #13146) and reference_docs fixtures.
• --json for machine-readable output; exit code always 0 (measurement instrument, not a gate), exit 2 only when no manifest is found.

Verdict on current main (2026-09-04)

Lake manifests scanned: 20 (skipped 2, documented exclusions)
Identity clusters: ONE core cluster of 20 lakes, toolchain v4.32.1, mathlib=520045ab
Divergent: social_choice_lean_peters (+SocialChoiceLean only), mimo_lean (+slt only)
No-dependency lakes: 4

All shared revs are identical across the parc. The only two divergences are additions of an own dependency — no shared package rev differs anywhere. Checkout mutualisation (#4363) and the warm-pool volume (#14337) are therefore possible without a single dependency bump.

Tests

python -m pytest scripts/lean/tests/test_compare_lake_manifests.py -q — 9 passed (clustering, divergence reporting with package-level diffs, own-package addition shape, documented exclusions, .lake/packages/ ignore, toolchain read, text render, exit-2 path).

See #4362

[github-actions]

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

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=1 genre=3 cap=2)
• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=1 genre=3 cap=2)
• 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.

[jsboige]

[Hermes] review 9e9799a (contrainte token : COMMENT only, opener=jsboige).

Verdict : solide, vérifié par exécution réelle.

1. Tests exécutés : fichiers extraits au head SHA et passés sous pytest — 9/9 passed in 0.11s (identity clusters, divergence rev, package additionnel, exclusions documentées, pin-tree vide, nested .lake/packages ignoré, exit 2 sans manifest). Compile OK.
2. Design correct : fingerprint = arbre complet {name: rev} (pas juste Mathlib) — c'est bien la bonne granularité pour #4363 (junctions) et #14337 (warm pool). Lecture du rev résolu (pas inputRev) = bon choix, c'est ce qui détermine le checkout.
3. Edge cases couverts par tests : empty pin tree jamais référence ni divergente (commentaire explicite dans le code), 1-vs-1 split, package additionnel = divergence signalée sans fausser la pluralité du core.
4. Security scan : clean.

2 remarques (non bloquantes) :

• discover_manifests skip tout chemin contenant reference_docs n'importe où (needle in str(rel)) — un futur lake nommé p.ex. reference_docs_2027 serait exclu silencieusement. Acceptable tant que skipped est affiché dans le report (il l'est).
• toolchain est lu mais exclu de l'identity_key : deux lakes avec pins identiques mais toolchains différents partiraient un cluster alors qu'ils ne peuvent pas partager un checkout. Vu que le toolchain conditionne le cache Lean, un jour ou l'autre l'inclure dans le fingerprint (ou le signaler dans le cluster) évitera une surprise.

Rien d'autre — code lisible, exclusions motivées par des issues (#6116/#13146), exit code 0 documenté (instrument de mesure, pas gate).