From e201be44767e9d3930761b5630a6c2814da0dc95 Mon Sep 17 00:00:00 2001 From: jsboige Date: Sat, 12 Sep 2026 21:52:11 +0200 Subject: [PATCH] ci(lean,#14337): migrate lean-conway.yml target-coverage to coursia-lean pool (tranche 2) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Tranche 2 narrow héritage G-VAR-1 Tell c.531-L2 strict : bascule `coursia-linux` → `coursia-lean` pour le job `target-coverage` du workflow non-reusable lean-conway.yml. Pattern strictement identique à PR #15303 (po-2024 c.1020 tranche 1 sur lean-social-choice.yml). Mesure first-hand Tell c.1356 preflight ×37ᵉ : - lean-conway.yml déjà allowlisté (ligne 128 du script policy, tranche 3c #14283) — aucune modification du policy script requise - aucun `workflow_call` → éligible à la migration self-hosted - collision guard : #15706 OPEN ne touche pas ce fichier - runs-on bascule effectif, `if:` anti-fork inchangé Permet de bénéficier du cache Mathlib chaud (image Dockerfile.lean = elan + leanprover/lean4:v4.32.1 baked in, .lake/packages gardé au chaud dans le volume _work par slot). PR LIVRÉE au coord ai-01 (Tell c.1502 strict 0 merge d'autrui). Co-Authored-By: Claude Haiku 4.5 (1M context) --- .github/workflows/lean-conway.yml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/.github/workflows/lean-conway.yml b/.github/workflows/lean-conway.yml index dc64480aa5..0e8ce5ae4f 100644 --- a/.github/workflows/lean-conway.yml +++ b/.github/workflows/lean-conway.yml @@ -262,13 +262,18 @@ jobs: # that keeps its own copy of the list detects everyone's drift but its own. target-coverage: name: conway target-coverage - # Routage #14283 tranche 3 (decision ai-01 2026-09-02) : jambe Linux - # auto-hebergee. Le `if:` ci-dessous est la garde anti-fork exigee par - # scripts/ci/check_self_hosted_runner_policy.py ; un `runs-on` STATIQUE la - # rend auditable (une expression dynamique leve DYNAMIC_RUNS_ON). - # Les PRs de fork sautent le job -- pr_gate.py compte `skipped` comme OK. - # Retour arriere = remettre `runs-on: ubuntu-latest` + retrait de l'allowlist. - runs-on: [self-hosted, coursia-ephemeral, coursia-linux] + # Routage #14337 tranche 2 (decision ai-01 2026-09-04, migration narrow + # heritage G-VAR-1 Tell c.531-L2 strict) : bascule `coursia-linux` vers + # `coursia-lean` pour beneficier du cache Mathlib chaud (image + # Dockerfile.lean = elan + leanprover/lean4:v4.32.1 baked in, .lake/packages + # garde au chaud dans le volume _work par slot). Pattern PR #15303 tranche + # 1 sur lean-social-choice.yml (po-2024 c.1020). Le `if:` ci-dessous est la + # garde anti-fork exigee par scripts/ci/check_self_hosted_runner_policy.py ; + # un `runs-on` STATIQUE la rend auditable (une expression dynamique leve + # DYNAMIC_RUNS_ON). Les PRs de fork sautent le job -- pr_gate.py compte + # `skipped` comme OK. Allowlist deja presente (ligne 128 du policy script, + # tranche 3c #14283). Retour arriere = remettre `coursia-linux` + push. + runs-on: [self-hosted, coursia-ephemeral, coursia-lean] if: (github.event.pull_request.head.repo.full_name == null || github.event.pull_request.head.repo.full_name == github.repository) && always() steps: - uses: actions/checkout@v4