diff --git a/.github/workflows/lean-social-choice.yml b/.github/workflows/lean-social-choice.yml index fd0d14dca0..e9f21ea880 100644 --- a/.github/workflows/lean-social-choice.yml +++ b/.github/workflows/lean-social-choice.yml @@ -129,7 +129,13 @@ jobs: build: name: "Lake build" - runs-on: ubuntu-latest + runs-on: [self-hosted, coursia-ephemeral, coursia-lean] + # Garde anti-fork exigee par scripts/ci/check_self_hosted_runner_policy.py + # (SAME_REPO_GUARD) : un fork ne doit pas executer du code sur le pool + # self-hosted, son PR etant juste un payload. Le code d'un fork ne tourne + # jamais sur `coursia-lean` ; `pr_gate.py` compte `skipped` comme OK + # (cf lean-knot.yml ligne 124 meme garde, tranche 1 #14337). + if: github.event.pull_request.head.repo.full_name == null || github.event.pull_request.head.repo.full_name == github.repository # Serialized behind the CHEAP text-level gate (fail fast before spending a # Mathlib build). proof-integrity now depends on THIS job (c.327) so the two # full compiles run in series instead of in parallel. diff --git a/scripts/ci/check_self_hosted_runner_policy.py b/scripts/ci/check_self_hosted_runner_policy.py index 7cc6b61843..d8cd5827be 100644 --- a/scripts/ci/check_self_hosted_runner_policy.py +++ b/scripts/ci/check_self_hosted_runner_policy.py @@ -136,6 +136,14 @@ # choice/build (merite un pool a cache Mathlib chaud, cf #14337), # notebook-execution-required/golden-set-execute (execution lourde). "bash-syntax-advisory.yml", + # c.1020 (#14337 tranche 1) : seule `lean-social-choice.yml:build` + # (job non-reusable, branche ONLY) peut basculer vers le pool + # specialise `coursia-lean` (image Dockerfile.lean = elan + + # leanprover/lean4:v4.32.1 baked in, .lake/packages garde au chaud + # dans le volume _work par slot). `lean-build.yml` et `lean-axiom.yml` + # restent ubuntu-latest : ce sont des REUSABLE workflows (declenche + # par `workflow_call`), la garde REUSABLE_SELF_HOSTED leur refuse + # le routage self-hosted par principe (un fork peut les invoquer). "lean-social-choice.yml", "notebook-execution-required.yml", "secret-scan.yml",