Repository navigation
ci(lean,#13751): percolation_lean migre dans la matrice lean-ci — 22e lake, wrapper supprimé - #18996
Conversation
…wrapper supprime Consolidation workflows de #13751 : le dispatcher lean-percolation.yml (74 lignes) migre dans lean-ci-matrix.yml -- entree manifeste (sorry-baseline 0, sorry-filter-mode real, axiom-target-modules *, parametres reports a l'identique du wrapper) + paths push/pr + suppression du wrapper (jamais les deux declencheurs). La jambe proof-integrity est couverte par lean-build.yml (if: matrix.axiom-target-modules != ''), les self-cover gate (lean_server.py, lean-build.yml, actions) deja present au dispatcher. Garde check_lake_matrix_paths : OK, 22 lakes, union push/pr coherente, aucun double declencheur. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM
[Hermes] — review d'exécution au head fbe592a46 (22e lake de la consolidation #13751, aucun coverage préalable).
Garde anti-drift rejouée au head (checkout scripts+.github au SHA exact) : python scripts/ci/check_lake_matrix_paths.py → lake-matrix OK : 22 lake(s) couvert(s), union push/pr coherente avec le manifeste, aucun double declencheur, RC=0 — identique au body. Le wrapper lean-percolation.yml est bien absent de l'arbre (suppression effective, pas laissée en double déclencheur).
Parité paramétrique wrapper→matrice vérifiée à la source (lean-build.yml l.369-376), paramètre par paramètre : sorry-baseline "0" ✓, sorry-filter-mode real ✓ (manifeste), target-modules "*" ✓ (axiom-target-modules), allow-axioms "" = défaut || '' ✓, fail-on-sorry true = défaut || 'true' ✓. Les 3 chemins paths reportés à l'identique aux DEUX unions (push+PR) — aucune couverture perdue vs le wrapper (proof-integrity passe par le même if: matrix.axiom-target-modules != '', self-cover B.3 déjà aux paths du dispatcher, workflow_dispatch couvert par celui du dispatcher).
Sécu : diff workflow+JSON, aucun secret. Checks : 41 jambes pass, PR gate fail = jambe DWELL seule (tête 10 min < plancher 120, minuteur documenté).
[Hermes hermes-pr-review, cycle :14 03/10, host f6be46d1b7a3, sig=7f5cb6db]
Path-collision (organ #13359/#13615)Cette PR #18996 (
|
|
[ADJOINT PREFLIGHT] |
…ake, wrapper supprime (#19313) Tranche workflows de #13751 (axe « 12 per-lake restants »), recette du pilote #18996 : suppression du wrapper lean-geometry.yml (69 lignes) + entree geometry dans scripts/lean/ci_lakes.json (baseline 0, mode real, axiom-target-modules "*", parametres reportes a l'identique) + bloc paths aux DEUX unions de lean-ci-matrix.yml. README du lac recalle sur la matrice. Preuve : check_lake_matrix_paths.py -- 23 lakes couverts, union push/pr coherente, aucun double declencheur. Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
…min matriciel, verdict re-mesure (#20005) La ligne `percolation_lean` de la table de triage nommait `lean-percolation.yml`, supprime par #18996 quand le lake est passe dans la matrice lean-ci (#13751). Le cablage du gate d'axiomes existe pourtant toujours : il vit dans `scripts/lean/ci_lakes.json` (`axiom-target-modules: "*"`) et `lean-build.yml` l'execute (`if: matrix.axiom-target-modules != ''` -> `.github/actions/lean-axiom`). Le controle positif revendique par cette ligne etait attache au wrapper disparu : il n'avait jamais ete rejoue sur le chemin matriciel. Il l'est ici. Mesures du 2026-10-09 (step exact du gate `scripts/lean/axiom_check_step.py`, parametres du manifeste) : - GREEN : modules FR du lake enumeres, cloture axiomatique [propext, Classical.choice, Quot.sound] (defauts, `allow-axioms` vide), 0 sorryAx, RC=0. - Controle negatif : `sorry` injecte dans un module cible puis lake reconstruit -> axioms [propext, sorryAx, Classical.choice, Quot.sound], has_sorry True, RC=1. Source restauree (md5 identique, `git status` vide) -> RC=0. - Piege mesure : l'organe ne reconstruit pas le lake (il lit les oleans). Une mutation de source SEULE rougit par `build_failed_returncode` (`Unknown constant`), pas par `sorryAx` -- un controle fidele exige un `lake build` entre la mutation et le run. Etendue au meme defaut, meme cause (la migration matricielle a perime la table) : la derniere ligne annoncait « 15 autres lacs | workflows existants | NON », faux pour des lacs matriciels sans workflow dedie, et citait `sudoku` comme non cable alors qu'il l'est depuis #18349 (EPIC #18038). Les 15 sont desormais nommes et les borderline restants (`learningtheory`, `decisiontheory`) sont exacts. L'en-tete de colonne disait « Workflow `lean-*.yml` » pour une colonne qui repond desormais aussi « entree du manifeste matriciel » : reformule. Les compteurs bruts de la mesure (fichiers, modules, declarations) sont retires de la prose au profit de la portee nommee -- la donnee quantitative est tenue par le CI (#9377), et `check_prose_quantitative_claims.py` est repasse a [OK]. See #14910. Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
3 participants
Grain: LIGHT/tooling -- lane myia-po-2027:CoursIA -- prev: LIGHT/notebook-python #18986
ci(lean,#13751): percolation_lean migre dans la matrice lean-ci — 22e lake, wrapper supprimé
Summary
Tranche workflows de #13751 (axe « 13 per-lake réels à consolider ») : le dispatcher dédié
lean-percolation.yml(74 lignes) migre danslean-ci-matrix.yml. Lake pilote suivant de la consolidation entamée (21 lakes déjà au manifeste : sudoku, kelly, … serre100) — c'est la même recette mécanique, lake par lake.Diff (3 fichiers, +23/−74)
scripts/lean/ci_lakes.json(+13) : entréepercolation—sorry-baseline: "0",sorry-filter-mode: real,axiom-target-modules: "*"(paramètres reportés à l'identique du wrapper ; le manifeste est la source unique de vérité du dispatcher)..github/workflows/lean-ci-matrix.yml(+10) : bloc pathspercolation_leanajouté aux deux unions (push + pull_request), avec commentaire d'héritage..github/workflows/lean-percolation.yml(−74) : wrapper supprimé — la règle du manifeste interdit les deux déclencheurs à la fois (double build).Couverture préservée (rien perdu)
civialean-build.yml(build + sorry ratchet real, baseline 0)lean-matrix→lean-build.yml@./mode matriceproof-integrityvialean-axiom.yml(target-modules: "*",fail-on-sorry: true)lean-build.ymll.369-377 :if: matrix.axiom-target-modules != ''→ actionlean-axiom(le manifeste porte"*")lean_server.py,lean_utils.py,lean-axiom.yml,lean-build.yml, actions)on.pathsdu dispatcher (self-cover B.3 hérité des wrappers serre/social-choice supprimés)workflow_dispatchmanuelworkflow_dispatchdu dispatcher = tous les lakes du manifeste (self-cover)Preuves
python scripts/ci/check_lake_matrix_paths.py→lake-matrix OK : 22 lake(s) couvert(s), union push/pr coherente avec le manifeste, aucun double declencheur.See #13751 (tranche workflows — résiduel après celle-ci : 12 per-lake réels)
🤖 Generated with Claude Code