jsboige · Nov 4, 2026 · Nov 4, 2026
diff --git a/docs/ci/self-hosted-runners.md b/docs/ci/self-hosted-runners.md
@@ -550,17 +550,22 @@ Docker relance le conteneur à chaque démarrage du daemon (donc de la distro) ;
 
 La primitive de routage est le **jeu de labels dédié** : `DEDICATED_LABEL_SETS` dans `scripts/ci/check_self_hosted_runner_policy.py` porte un jeu par pool, et c'est le label distinct qui garantit le routage — jamais une convention de nommage.
 
-### Inventaire des pools (mesuré sur `main`, octobre 2026)
+**La règle jumelle, mesurée le 2026-11-04 : un pool qui sort de la flotte sort de la liste d'autorisation.** `DEDICATED_LABEL_SETS` est une liste de jeux **servis**, pas une liste de jeux **planifiés** : y laisser un pool éteint ouvre un trou *fail-open* — le garde certifie un routage qu'aucun runner ne peut prendre, et le job attend en file d'attente indéfiniment. Le retrait s'oppose donc à l'oubli : le jeu retiré est conservé, renommé, dans `RETIRED_LABEL_SETS`, et un test interdit sa ré-admission silencieuse.
+
+### Inventaire des pools (mesuré sur `main`, octobre 2026 ; re-mesuré les 2026-11-04 et 2026-11-05)
 
 | Pool | Jeu de labels | Support | Rôle |
 |---|---|---|---|
 | `coursia-fast-guards` | `REQUIRED_LABELS` | hôte Windows | gardes Windows (po-2024) |
 | `coursia-linux` | `LINUX_RUNNER_LABELS` | conteneur, image minimale + python/gh/jq | gardes PR pure-Python |
 | `coursia-waiter` | `WAITER_LABELS` | label distinct sans slot de travail | laisser un gate **attendre** sans consommer de CPU (arbitrage ai-01 2026-09-02 : « attendre ne coûte pas de CPU ») |
-| `coursia-lean` | `LEAN_RUNNER_LABELS` | conteneur, image `Dockerfile.lean` (elan + toolchain), `.lake` tenu chaud dans le volume par slot | scans et builds Lean ; un slot lean ne porte **jamais** `coursia-linux` |
+| `coursia-lean` | `RETIRED_LEAN_RUNNER_LABELS` — **retiré**, pool éteint | conteneur, image `Dockerfile.lean` (elan + toolchain), `.lake` tenu chaud dans le volume par slot | scans et builds Lean ; **pool éteint** — extinction mesurée le 2026-10-23 par la sonde du dépôt, confirmée le 2026-11-04 (48 runners) et re-mesurée le 2026-11-05 (49 runners) — **zéro** porteur de `coursia-lean` dans les deux mesures ; les jambes Lean sont passées à `[self-hosted, coursia-ephemeral, coursia-linux]` |
+| `coursia-persistent` | jeu **non autorisé** par le garde | conteneur, slots persist de po-2024 | 7 slots **enregistrés mais offline** à la mesure du 2026-11-04 ; leur jeu de labels n'est pas dans `DEDICATED_LABEL_SETS`, donc aucun workflow ne peut y router ; ils portent `coursia-ephemeral` alors que leur spécification versionnée (`scripts/ci/docker/linux-runner/persist/po-2024/create-persist-slots.sh`) impose l'inverse (« un slot persist porte `coursia-persistent` et **NE porte PAS** `coursia-ephemeral` ») — arbitrage de composition de flotte, pas de lane |
 
 Les pools `coursia-docs` (quarto/pandoc) et `coursia-browser` (npm + navigateurs Playwright) restent des **candidats non livrés** : leur déploiement touche le conteneur runner porté par po-2024 — l'infra d'un autre workspace se demande au workspace qui la porte, elle ne s'applique pas depuis l'extérieur.
 
+**Le tiroir ne s'arrête pas au garde.** La jambe Lean reste portée par deux autres organes, et l'écart est intentionnel plutôt qu'un oubli : le budget mémoire (`scripts/ci/assert_memory_budget.py`, jambe `lean : 1 x 6.0 GiB`) et l'épinglage d'image (`check_runner_version_pin.py` → `supervise.sh:LEAN_IMAGE`) conservent la jambe Lean jusqu'à sa ré-admission ou son démontage explicite. Tant que les slots existent sur le parc, la CI ne peut pas prétendre que le coût Lean a disparu ; le garde dit seulement que le **routage** vers le pool éteint est refusé. Le retrait du jeu de labels et la ré-admission du pool sont deux gestes distincts : le premier est fait, le second attend la mesure du parc.
+
 ### La gate mémoire de la migration des builds Lean
 
 La ligne de migration qui déplace le coût réel est le `runs-on` de `lean-build.yml` / `lean-axiom.yml` (workflows réutilisables : leurs builds s'exécutent **chez les callers**, une seule bascule déplace tout le monde). Elle est **gated sur l'arbitrage mémoire** : le pic d'élaboration de `HashlifeCorrectness.lean` dépasse 16 GB alors que le pool est budgété à 12 GB/slot (VM 24 GB max) — migrer avant l'arbitrage garantit l'OOM sur les gros modules, une régression CI pour gagner du temps de file. Chiffres mesurés (2026-09-21, cf #14337) : builds 9 224–12 302 s sur GitHub-hosted à `.lake` froid, contre 10–83 s pour les scans sur pool à `.lake` chaud. Un pool lean à slots ≥ 32 GB débloque la migration et fait de ces chiffres le « avant » de la mesure avant/après.
@@ -569,7 +574,8 @@ La ligne de migration qui déplace le coût réel est le `runs-on` de `lean-buil
 
 1. un nouveau jeu de labels dans `DEDICATED_LABEL_SETS` ;
 2. une image dédiée — jamais un ajout à l'image commune ;
-3. l'entrée correspondante dans `scripts/tests/test_check_self_hosted_runner_policy.py`.
+3. l'entrée correspondante dans `scripts/tests/test_check_self_hosted_runner_policy.py` ;
+4. **la mesure du parc** : `gh api repos/jsboige/CoursIA/actions/runners` rend les runners **en service** et leurs jeux de labels — c'est cette mesure, et non la présence du jeu dans la liste, qui dit si un routage est servi. Le symétrique est obligatoire : quand un pool s'éteint, son jeu sort de `DEDICATED_LABEL_SETS` et passe dans `RETIRED_LABEL_SETS` (constante conservée, test de non-ré-admission à l'appui), faute de quoi le garde certifie une file d'attente éternelle.
 
 ## Tranches suivantes, activation partielle
 

diff --git a/scripts/ci/check_self_hosted_runner_policy.py b/scripts/ci/check_self_hosted_runner_policy.py
@@ -65,17 +65,38 @@
     "self-hosted",
     "coursia-waiter",
 }
-# Dedicated label set for the specialised Lean pool (#14337, po-2024): elan +
+# RETIRED label set -- 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 = {
+#
+# The pool is EXTINCT: `gh api repos/jsboige/CoursIA/actions/runners` measured
+# on 2026-11-04 renders 48 runners and ZERO carrier of `coursia-lean`; the
+# extinction had already been measured by the repository's own probe on
+# 2026-10-23 (.github/workflows/runner-starvation-advisory.yml, lines 26-30:
+# "LE LABEL `coursia-lean` N'EXISTE PLUS"), which also notes that the Lean
+# legs moved to [self-hosted, coursia-ephemeral, coursia-linux].
+#
+# Keeping the set in DEDICATED_LABEL_SETS was a fail-open hole: the guard
+# certified a routing that no runner can serve, and the job then waited in the
+# queue forever. The rule is now written down: a pool that leaves the fleet
+# leaves the authorisation list, and a set that is not in service is refused
+# rather than admitted.
+#
+# The constant is kept, renamed, so the knowledge survives the removal. To
+# re-admit it: re-deploy the pool, measure that the runners carry the label,
+# then move the set back into DEDICATED_LABEL_SETS -- never silently.
+RETIRED_LEAN_RUNNER_LABELS = {
     "self-hosted",
     "coursia-ephemeral",
     "coursia-lean",
 }
-DEDICATED_LABEL_SETS = (REQUIRED_LABELS, LINUX_RUNNER_LABELS, WAITER_LABELS, LEAN_RUNNER_LABELS)
+# Label sets that are NOT authorised any more. A retired set must never be
+# re-admitted silently; the re-admission requires a fresh measurement of the
+# fleet, as the comment above spells out.
+RETIRED_LABEL_SETS = (RETIRED_LEAN_RUNNER_LABELS,)
+DEDICATED_LABEL_SETS = (REQUIRED_LABELS, LINUX_RUNNER_LABELS, WAITER_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
@@ -1837,13 +1858,33 @@ def scan_workflows(
                     "runner groups are unavailable for this personal-account repository",
                 ))
 
+            # Un jeu retire est refuse pour une raison qui lui est propre :
+            # le dire evite d envoyer le developpeur vers un autre pool
+            # ("missing: coursia-fast-guards") alors que le vrai motif est
+            # l'extinction du pool vise.
+            retired_set = next(
+                (retired for retired in RETIRED_LABEL_SETS if set(labels) == retired),
+                None,
+            )
             if any(set(labels) == allowed for allowed in DEDICATED_LABEL_SETS):
                 missing: list[str] = []
                 unexpected: list[str] = []
+            elif retired_set is not None:
+                missing = []
+                unexpected = []
             else:
                 missing = sorted(REQUIRED_LABELS - labels)
                 unexpected = sorted(labels - REQUIRED_LABELS)
-            if missing or unexpected:
+            if retired_set is not None:
+                violations.append(Violation(
+                    path.name,
+                    str(job_name),
+                    "RUNNER_LABELS",
+                    "retired pool -- this label set is out of service "
+                    "(cf. RETIRED_LABEL_SETS); re-admission requires a fresh "
+                    "measurement of the fleet, not an edit of this guard",
+                ))
+            elif missing or unexpected:
                 detail = []
                 if missing:
                     detail.append(f"missing: {', '.join(missing)}")

diff --git a/scripts/tests/test_check_self_hosted_runner_policy.py b/scripts/tests/test_check_self_hosted_runner_policy.py
@@ -387,28 +387,47 @@ 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.
+def test_retired_lean_label_set_is_rejected_in_allowlisted_workflow(tmp_path):
+    # #14337: the specialised Lean pool (po-2024) had its own dedicated label
+    # set -- coursia-lean routed lake builds to the elan image with the warm
+    # .lake work volume. The pool is EXTINCT (measurement 2026-11-04:
+    # `gh api .../actions/runners` renders 48 runners and ZERO carrier of
+    # `coursia-lean`; the repository's own probe had already measured the
+    # extinction on 2026-10-23). A routing that no runner can serve must be
+    # refused by the guard, not admitted: the job would otherwise wait in the
+    # queue forever while the guard had certified it.
     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
+              - run: echo unsafe
         """)
     result = policy.scan_workflows(tmp_path)
-    assert result.violations == []
-    assert result.self_hosted_jobs == 1
+    assert codes(result) == {"RUNNER_LABELS"}
+
+
+def test_retired_label_sets_are_not_authorised():
+    # Non-regression: a retired set must never re-enter the authorisation
+    # list without a fresh measurement of the fleet. This is the assertion
+    # that keeps the removal from being undone by a later edit.
+    #
+    # Non-vacuity: the loop below is vacuous when RETIRED_LABEL_SETS is
+    # empty -- emptying the tuple loses the very knowledge the removal
+    # preserves, and the test would still pass on that one-character edit.
+    # The membership assertion is what makes it fail.
+    assert policy.RETIRED_LEAN_RUNNER_LABELS in policy.RETIRED_LABEL_SETS
+    for retired in policy.RETIRED_LABEL_SETS:
+        assert retired not in policy.DEDICATED_LABEL_SETS
+    assert policy.RETIRED_LEAN_RUNNER_LABELS not in policy.DEDICATED_LABEL_SETS
 
 
 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.
+    # eligible for both pools would make the routing guarantee meaningless --
+    # and the lean set is retired anyway, so it is refused on both counts.
     write_workflow(tmp_path, "linux-self-hosted-tests", """
         name: mixed
         on: workflow_dispatch