ci(#14337): tranche 1 — pool de runners spécialisé Lean (label coursia-lean)

scripts/ci/check_self_hosted_runner_policy.py

@@ -58,7 +58,17 @@
     "self-hosted",
     "coursia-waiter",
 }
-DEDICATED_LABEL_SETS = (REQUIRED_LABELS, LINUX_RUNNER_LABELS, WAITER_LABELS)
+# Dedicated label set for the specialised Lean pool (#14337, po-2024): elan +
+# toolchain baked in a dedicated image (Dockerfile.lean), .lake kept warm in
+# the per-slot work volume. A lean slot never carries coursia-linux -- the
+# distinct label is the routing guarantee (a pure-Python guard must not land
+# on a lean slot, and a lake build must not land on the minimal image).
+LEAN_RUNNER_LABELS = {
+    "self-hosted",
+    "coursia-ephemeral",
+    "coursia-lean",
+}
+DEDICATED_LABEL_SETS = (REQUIRED_LABELS, LINUX_RUNNER_LABELS, WAITER_LABELS, LEAN_RUNNER_LABELS)
 # Owner-approved additions must cite the lane that owns the runner deployment:
 # - pr-gate-stale-sweep.yml: schedule-mutualized re-aggregation (pre-existing).
 # - windows-self-hosted-tests.yml: workflow_dispatch-ONLY vehicle for the 9

scripts/ci/docker/linux-runner/Dockerfile.lean

@@ -0,0 +1,53 @@
+# Runner GitHub Actions Linux specialise LEAN (#14337 tranche 1 : pools
+# specialises par labels plutot qu'une image unique qui grossit).
+#
+# RATIONALE (cf issue #14337) : le cout d'un job Lean n'est pas le toolchain,
+# c'est MATHLIB. Deux etats chauds, deux supports :
+#   - elan + toolchain stable : dans l'IMAGE (couche figee, reproductible,
+#     pincee par SHA-256 comme le tarball runner et gh du Dockerfile de base).
+#   - .lake/packages et .lake/build des lakes : dans le VOLUME _work PAR SLOT
+#     (pattern #14285 -- le checkout persiste, lake build devient incremental
+#     et `lake exe cache get` ne re-telecharge plus les oleans Mathlib).
+#     Aucune image, si grosse soit-elle, ne peut porter cet etat : il depend
+#     du lake et vit cote slot.
+#
+# Le toolchain par defaut est EPINGLE sur v4.32.1 : mesure du 2026-09-04,
+# 13/14 lakes du depot portent leanprover/lean4:v4.32.1 (seul conway_cgt_lean
+# pinne v4.31.0-rc2). Une image sur "stable" (v4.33.1 au jour du build) serait
+# alignee sur zero lake : chaque job paierait un telechargement elan a la volee
+# dans ~/.elan (ephemere par conteneur) -- exactement le cout que ce pool
+# existe pour eviter. Un lake qui pinne une autre version declenche quand meme
+# ce telechargement ; si le cas devient frequent, monter un volume dedie sur
+# /home/runner/.elan au deploiement (tranche 2+).
+#
+# Labels du pool : self-hosted,coursia-ephemeral,coursia-lean -- JAMAIS
+# coursia-linux : le label distinct EST la garantie de routage (un garde
+# Python ne doit pas atterrir sur un slot Lean, et inversement).
+
+FROM coursia-linux-runner:2.336.0
+
+# elan pince par SHA-256, meme discipline que le Dockerfile de base.
+# v4.2.4, asset elan-x86_64-unknown-linux-gnu.tar.gz (contient elan-init).
+ARG ELAN_VERSION=4.2.4
+ARG ELAN_SHA256=42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63
+
+USER root
+ADD https://github.com/leanprover/elan/releases/download/v${ELAN_VERSION}/elan-x86_64-unknown-linux-gnu.tar.gz /tmp/elan.tar.gz
+RUN echo "${ELAN_SHA256}  /tmp/elan.tar.gz" | sha256sum -c - \
+    && tar xzf /tmp/elan.tar.gz -C /tmp \
+    && chown runner:runner /tmp/elan-init \
+    && rm /tmp/elan.tar.gz
+
+# Installation sous l'utilisateur runner : elan est un installeur par-compte
+# (style rustup), ~/.elan doit appartenir a runner pour que les toolchains
+# telecharges au runtime soient accessibles sous l'UID 1001 du conteneur.
+ARG LEAN_TOOLCHAIN=leanprover/lean4:v4.32.1
+USER runner
+# ENV AVANT le RUN : --no-modify-path laisse ~/.elan/bin hors du PATH du shell,
+# donc le meme RUN ne retrouverait pas `elan` sans cette ligne (mesure :
+# "/bin/sh: 1: elan: not found", exit 127).
+ENV PATH=/home/runner/.elan/bin:$PATH
+RUN /tmp/elan-init -y --no-modify-path --default-toolchain ${LEAN_TOOLCHAIN} \
+    && rm /tmp/elan-init \
+    && elan default ${LEAN_TOOLCHAIN} \
+    && lake --version

scripts/ci/docker/linux-runner/supervise.sh

@@ -23,6 +23,8 @@
 #                                  # N slots (defaut 2) ; --force leve
 #                                  # un sentinel STOP_FILE prealable
 #   ./supervise.sh waiters [N]   # N slots d'attente PR-gate (label coursia-waiter, defaut 24)
+#   ./supervise.sh lean [N]      # N slots Lean specialises (label coursia-lean, image
+#                                  # dediee elan+toolchain, .lake chaud par slot, defaut 2)
 #   ./supervise.sh stop          # arret gracieux : pas de nouveau conteneur
 #   ./supervise.sh status
 #
@@ -80,6 +82,32 @@ WAITER_CPUS="${COURSIA_RUNNER_WAITER_CPUS:-1}"
 WAITER_MEMORY="${COURSIA_RUNNER_WAITER_MEMORY:-1g}"
 WAITER_PIDS="${COURSIA_RUNNER_WAITER_PIDS:-128}"
 
+# Pool Lean specialise (#14337 tranche 1) : le cout d'un job Lean n'est pas le
+# toolchain mais MATHLIB. Image dediee (Dockerfile.lean : elan + toolchain
+# stable pinnnes), labels dedies (JAMAIS coursia-linux -- le label distinct
+# est la garantie de routage), caps hautes (lake build est CPU/RAM lourd).
+# Le .lake chaud vit dans le volume _work PAR SLOT au prefixe dedie
+# coursia-runner-work-lean-{N} (pattern #14285) : .lake/packages et .lake/build
+# survivent aux conteneurs, lake build devient incremental.
+LEAN_IMAGE="${COURSIA_LEAN_RUNNER_IMAGE:-coursia-lean-runner:2.336.0}"
+LEAN_LABELS="${COURSIA_LEAN_RUNNER_LABELS:-self-hosted,coursia-ephemeral,coursia-lean}"
+LEAN_NAME_PREFIX="${COURSIA_LEAN_RUNNER_NAME_PREFIX:-myia-po-2024-lean-docker}"
+LEAN_WORK_VOLUME_PREFIX="${COURSIA_LEAN_RUNNER_WORK_VOLUME_PREFIX:-coursia-runner-work-lean}"
+# 2 slots * 6 cpus = 12 des 16 coeurs au pire ; l'hote workstation prime
+# (cf CONTRAINTE en tete de fichier) -- baisser N ou les caps si la machine
+# gene pendant un lake build.
+LEAN_CPUS="${COURSIA_LEAN_RUNNER_CPUS:-6}"
+LEAN_MEMORY="${COURSIA_LEAN_RUNNER_MEMORY:-8g}"
+LEAN_PIDS="${COURSIA_LEAN_RUNNER_PIDS:-512}"
+# Swap au-dela de la RAM du slot : les modules Hashlife de conway_lean
+# pointent a >16 Go au build a froid (exit 137 mesure sous --memory 8g,
+# 8716/8727 modules OK puis Walls.{SE,SW,NE} tues ; les runners hosted
+# s'en sortent par 32G de fallocate swap, lean-axiom.yml L~100). Un job
+# conteneurise n'a pas sudo pour creer son swap, donc le pool le porte :
+# memory-swap 24g = 8g RAM + 16g swap. Le swap n'est PAS de la RAM
+# reservee -- l'hote ne paie que si le pic survient.
+LEAN_MEMORY_SWAP="${COURSIA_LEAN_RUNNER_MEMORY_SWAP:-24g}"
+
 mkdir -p "$STATE_DIR"
 
 # Git Bash (MSYS) sous Windows reecrit les arguments de forme /posix/path des
@@ -119,9 +147,18 @@ fetch_token() {
   gh api --method POST "repos/$REPO/actions/runners/registration-token" --jq .token 2>/dev/null
 }
 
+# Parametre depuis #14337 : un slot = une boucle, mais nom/labels/image/caps
+# dependent du pool (linux genrique, lean). Les volumes toolcache/_work restent
+# la regle pour les pools D'EXECUTION (les waiters ont leur propre boucle sans
+# volume).
 slot_loop() {
-  local slot="$1"
-  local name="${NAME_PREFIX}-${slot}"
+  local slot="$1" name="$2" labels="$3" image="$4" cpus="$5" memory="$6" pids="$7"
+  local vol_prefix="${8:-$WORK_VOLUME_PREFIX}"
+  # Swap optionnel (pool lean : les modules Hashlife pointent >16 Go, mesure
+  # #14337). Vide = pas de --memory-swap, docker default (memory == swap).
+  local mem_swap="${9:-}"
+  local swap_args=()
+  [ -n "$mem_swap" ] && swap_args=(--memory-swap "$mem_swap")
   echo "[slot $slot] demarrage, nom runner=$name"
   while [ ! -f "$STOP_FILE" ]; do
     local token
@@ -136,16 +173,17 @@ slot_loop() {
     # mais le cache de depot (volume par slot) survit au conteneur (#14285).
     docker run --rm \
       --name "$name" \
-      --cpus="$CPUS" --memory="$MEMORY" --pids-limit="$PIDS" \
+      --cpus="$cpus" --memory="$memory" --pids-limit="$pids" \
+      "${swap_args[@]+"${swap_args[@]}"}" \
       --security-opt=no-new-privileges \
       -v "$TOOLCACHE_VOLUME":"$TOOLCACHE_MOUNT" \
-      -v "${WORK_VOLUME_PREFIX}-${slot}":"$WORK_MOUNT" \
+      -v "${vol_prefix}-${slot}":"$WORK_MOUNT" \
       -e RUNNER_TOOL_CACHE="$TOOLCACHE_MOUNT" \
       -e ACTIONS_RUNNER_INPUT_TOKEN="$token" \
       -e ACTIONS_RUNNER_INPUT_URL="https://github.com/$REPO" \
       -e ACTIONS_RUNNER_INPUT_NAME="$name" \
-      -e ACTIONS_RUNNER_INPUT_LABELS="$LABELS" \
-      "$IMAGE" >>"$STATE_DIR/$name.log" 2>&1
+      -e ACTIONS_RUNNER_INPUT_LABELS="$labels" \
+      "$image" >>"$STATE_DIR/$name.log" 2>&1
     local rc=$?
     echo "[slot $slot] conteneur termine (rc=$rc)"
     # Anti-emballement : si le conteneur meurt immediatement et en boucle
@@ -211,7 +249,7 @@ fait) puis '$0 start', OU relancer avec '$0 start $n --force'."
     # message clair (docker run -v creerait le volume tout seul, mais muet).
     docker volume create "${WORK_VOLUME_PREFIX}-${i}" >/dev/null \
       || die "volume ${WORK_VOLUME_PREFIX}-${i} impossible a creer -- docker volume create"
-    slot_loop "$i" &
+    slot_loop "$i" "${NAME_PREFIX}-${i}" "$LABELS" "$IMAGE" "$CPUS" "$MEMORY" "$PIDS" &
     echo "$!" >> "$STATE_DIR/pids"
   done
   echo "slots lances. Arret gracieux : $0 stop"
@@ -317,10 +355,42 @@ cmd_waiters() {
   wait
 }
 
+cmd_lean() {
+  local n="${1:-2}"
+  command -v docker >/dev/null || die "docker introuvable"
+  command -v gh >/dev/null || die "gh introuvable"
+  docker image inspect "$LEAN_IMAGE" >/dev/null 2>&1 \
+    || die "image $LEAN_IMAGE absente -- construire d'abord :
+    docker build -t $LEAN_IMAGE -f scripts/ci/docker/linux-runner/Dockerfile.lean scripts/ci/docker/linux-runner/"
+  [ -f "$STOP_FILE" ] && die "sentinel STOP pose -- arreter d'abord ($0 stop)"
+  # Idempotence calquee sur cmd_waiters : le garde PPID de `start` filtre
+  # `supervise.sh start` et ne verrait pas `lean`. Verrou par pid file.
+  if [ -f "$STATE_DIR/lean-pids" ]; then
+    local head_pid
+    head_pid="$(head -1 "$STATE_DIR/lean-pids" 2>/dev/null || true)"
+    if [ -n "$head_pid" ] && kill -0 "$head_pid" 2>/dev/null; then
+      die "pool lean deja lance (pid $head_pid) -- arreter d'abord ($0 stop)"
+    fi
+  fi
+  rm -f "$STATE_DIR/lean-pids"
+  echo "demarrage de $n slot(s) lean ; labels=$LEAN_LABELS ; caps : cpus=$LEAN_CPUS memory=$LEAN_MEMORY pids=$LEAN_PIDS ; image=$LEAN_IMAGE ; .lake chaud=${LEAN_WORK_VOLUME_PREFIX}-{1..$n} -> $WORK_MOUNT"
+  for i in $(seq 1 "$n"); do
+    docker volume create "${LEAN_WORK_VOLUME_PREFIX}-${i}" >/dev/null \
+      || die "volume ${LEAN_WORK_VOLUME_PREFIX}-${i} impossible a creer -- docker volume create"
+    slot_loop "$i" "${LEAN_NAME_PREFIX}-${i}" "$LEAN_LABELS" "$LEAN_IMAGE" \
+      "$LEAN_CPUS" "$LEAN_MEMORY" "$LEAN_PIDS" "$LEAN_WORK_VOLUME_PREFIX" \
+      "$LEAN_MEMORY_SWAP" &
+    echo "$!" >> "$STATE_DIR/lean-pids"
+  done
+  echo "slots lean lances. Arret gracieux : $0 stop"
+  wait
+}
+
 case "${1:-}" in
   start)   shift; cmd_start "${1:-2}" "${2:-}" ;;
   waiters) shift; cmd_waiters "${1:-24}" ;;
+  lean)    shift; cmd_lean "${1:-2}" ;;
   stop)    cmd_stop ;;
   status)  cmd_status ;;
-  *) echo "usage: $0 {start [N] [--force]|waiters [N]|stop|status}"; exit 2 ;;
+  *) echo "usage: $0 {start [N] [--force]|waiters [N]|lean [N]|stop|status}"; exit 2 ;;
 esac

scripts/tests/test_check_self_hosted_runner_policy.py

@@ -387,6 +387,41 @@ def test_linux_label_set_is_accepted_in_allowlisted_workflow(tmp_path):
     assert result.self_hosted_jobs == 1
 
 
+def test_lean_label_set_is_accepted_in_allowlisted_workflow(tmp_path):
+    # #14337: the specialised Lean pool (po-2024) carries its own dedicated
+    # label set -- coursia-lean routes lake builds to the elan image with the
+    # warm .lake work volume, never to the minimal linux image or the Windows
+    # runners.
+    write_workflow(tmp_path, "linux-self-hosted-tests", """
+        name: lean
+        on: workflow_dispatch
+        jobs:
+          test:
+            runs-on: [self-hosted, coursia-ephemeral, coursia-lean]
+            steps:
+              - run: echo safe
+        """)
+    result = policy.scan_workflows(tmp_path)
+    assert result.violations == []
+    assert result.self_hosted_jobs == 1
+
+
+def test_mixed_lean_and_linux_labels_are_rejected(tmp_path):
+    # Mixing the lean and linux dedicated sets must stay a violation: a job
+    # eligible for both pools would make the routing guarantee meaningless.
+    write_workflow(tmp_path, "linux-self-hosted-tests", """
+        name: mixed
+        on: workflow_dispatch
+        jobs:
+          test:
+            runs-on: [self-hosted, coursia-ephemeral, coursia-linux, coursia-lean]
+            steps:
+              - run: echo unsafe
+        """)
+    result = policy.scan_workflows(tmp_path)
+    assert codes(result) == {"RUNNER_LABELS"}
+
+
 def test_mixed_linux_and_fast_guards_labels_are_rejected(tmp_path):
     # Mixing the two dedicated sets must stay a violation: a job eligible
     # for both the Windows runners and the Linux container would make the