runners: le pool coursia-lean n'a jamais ete deploye -- 3 PR Lean affamees depuis 15 h #15205

Trois PR Lean sont en file depuis jusqu'a 15 h derriere un label que rien ne sert. Mesure ai-01 firsthand, 2026-09-08T11:43Z.

La mesure

La file d'attente reelle du depot est de 3 runs (le compteur brut affiche 22 : 19 sont les fantomes wedged de plus de 20 jours, offset permanent connu). Les trois reels sont tous Lean Knot CI :

Et l'inventaire du parc :

runners portant le label coursia-lean : count=0

Les 11 runners enregistres portent coursia-waiter (7) ou coursia-linux (4). Aucun ne porte coursia-lean. Le pool n'a pas ete perdu : il n'a jamais ete deploye.

• docker images sur ai-01 ne contient que coursia-linux-runner:2.336.0 / 2.337.0. L'image Dockerfile.lean n'a jamais ete construite.
• systemctl list-unit-files "coursia*" rend 3 unites : coursia-runner.service, coursia-waiters.service, coursia-ci.slice. Aucune unite lean.

La cause, datee

Le routage a ete livre le 2026-09-05 par #14667 (ci(#14337): route lean-conway/lean-knot to the lean pool via composite actions (tranche 2a)), qui a fait passer lean-knot.yml de coursia-linux a coursia-lean. Le routage a ete merge ; le pool qui devait le servir ne l'a jamais ete. Depuis, le dernier run vert de lean-knot.yml date du 2026-09-06T23:13:08Z (sur main, dont un job reste sur coursia-linux) ; toutes les jambes PR sont queued ou cancelled.

Pourquoi les deux contournements evidents ne marchent pas

Je les ai verifies avant de proposer quoi que ce soit -- aucun des deux n'est un remede :

1. Revenir a coursia-linux (l'etat d'avant le 2026-09-05) : les slots de ce pool sont plafonnes a 1536 Mo par le drop-in de sizing d'ai-01. Un build Mathlib y serait OOM-tue, exactement comme Build Quarto site l'a ete (ci(runner): 'Build Quarto site' OOM (exit 137) sur le pool auto-heberge -- le dimensionnement du parc n'a jamais echantillonne le job le plus lourd, et main est rouge depuis 13 h #15202). On echangerait une famine contre un exit 137.
2. Router vers ubuntu-latest (l'etat d'avant le 2026-09-02) : lean-knot.yml n'installe pas elan lui-meme. Son commentaire l'ecrit (image Dockerfile.lean = elan + toolchain pre-cuits) et l'action composite .github/actions/lean-build/action.yml ne contient aucune etape elan/toolchain -- elle enchaine directement sur le sorry gate. Un runner hebergé recevrait le job sans toolchain Lean.

Le commentaire de retour arriere du workflow (« Retour arriere = remettre uses: ...lean-build.yml@main ») est donc incomplet : il faudrait aussi restaurer l'installation du toolchain. Meme classe de defaut que la note de rollback de quarto-pages-deploy.yml relevee dans #15202.

Ce qu'il reste, et l'arbitrage RAM

La seule voie qui serve reellement ces jobs est de construire et deployer le pool coursia-lean tel que Dockerfile.lean le decrit. Cela coute de la RAM, sous mandat user 2026-09-08 de ne pas depasser le disponible avec de la marge. L'etat mesure aujourd'hui :

• VM WSL2 : 125 Go total, 27 Go utilises, 97 Go disponibles.
• coursia-ci.slice : 9,87 Go consommes sous un plafond de 16,00 Go -- soit ~6 Go de marge dans le budget deja alloue au CI.

supervise.sh porte deja le support (LEAN_MEMORY defaut 8g, LEAN_MEMORY_SWAP defaut 24g) avec sa rationale : « Le swap n'est PAS de la RAM reservee -- l'hote ne paie que si le pic survient ». Un --memory Docker est un plafond, pas une reservation : un slot lean a 8g ne consomme pas 8 Go, il consomme ce qu'il touche.

Point d'attention chiffre : 9,87 + un pic lean reel proche de 8 Go depasserait le plafond de slice de 16 Go et se ferait OOM-tuer par la slice. Le dimensionnement doit donc etre decide sur une mesure du pic reel d'un build knot_lean, pas sur le defaut de 8g -- et le plafond de slice releve, ou le nombre de slots coursia-linux reduit pendant les builds lean, avant d'ajouter quoi que ce soit.

Acceptance

1. gh api repos/jsboige/CoursIA/actions/runners rend >= 1 runner portant coursia-lean.
2. Les 3 runs en file demarrent et rendent un verdict.
3. Le dimensionnement retenu est ecrit (slot cap, plafond de slice, nombre de slots) avec la mesure du pic qui le justifie -- et traçable depuis le depot, ce que le sizing actuel n'est pas (defaut adjacent : ci(runner): 'Build Quarto site' OOM (exit 137) sur le pool auto-heberge -- le dimensionnement du parc n'a jamais echantillonne le job le plus lourd, et main est rouge depuis 13 h #15202, supervise.sh dit 4g, la machine applique 1536m via un drop-in non versionne).
4. Le commentaire de retour arriere de lean-knot.yml est corrige pour mentionner la restauration du toolchain.

Portee

Le parc de runners est ma charge (mandat user 2026-09-08 : « toi ton taf c'est optimiser les runners »). Je ne deploie pas dans la precipitation un pool qui n'a jamais existe alors que le mandat porte precisement sur la RAM -- le dimensionnement se decide sur une mesure, pas sur un defaut de fichier.