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

[jsboige]

Grain: MED/tooling — lane myia-po-2024:CoursIA — prev: MED/notebook-python #14582

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

Ce que la tranche 1 pose (le mécanisme ; le routage des builds = arbitrage design-gate, voir fin)

« Le coût d'un job Lean n'est pas le toolchain, c'est Mathlib » (#14337). Deux états chauds, deux supports :

État chaud	Support	Pourquoi
elan + toolchain v4.32.1	Image coursia-lean-runner:2.336.0 (Dockerfile.lean, FROM l'image de base)	figé, reproductible, épinglé par SHA-256 (elan v4.2.4) comme le tarball runner et gh du Dockerfile de base. v4.32.1 et non stable : mesure du 2026-09-04, 13/14 lakes du dépôt épingle v4.32.1 — une image stable (v4.33.1) serait alignée sur zéro lake et chaque job paierait un téléchargement elan à la volée
.lake/packages + .lake/build	Volume _work PAR SLOT coursia-runner-work-lean-{N} (pattern #14285)	aucune image ne peut porter cet état : il dépend du lake. Le checkout persiste → lake build devient incrémental, lake exe cache get ne re-télécharge plus les oleans

Changements

1. Dockerfile.lean (nouveau) : elan épinglé SHA + toolchain v4.32.1 préinstallé sous l'utilisateur runner (install par-compte, chown explicite, ARG LEAN_TOOLCHAIN garde le pin explicite et bumpable). Les lakes épingleant une autre version déclencheront un téléchargement à la volée dans ~/.elan éphémère — volume .elan dédié documenté comme suite si le cas devient fréquent.
2. supervise.sh lean [N] (défaut 2) : labels dédiés self-hosted,coursia-ephemeral,coursia-lean (JAMAIS coursia-linux — le label distinct est la garantie de routage), volumes work au préfixe dédié coursia-runner-work-lean-{N}, caps 6 cpus / 8 GiB / 512 pids, toolcache partagé, idempotence par pid-file (pattern cmd_waiters), fail-fast testé sur image absente.
   • slot_loop est paramétré (name, labels, image, caps, volume-prefix) au lieu d'une 3e copie.
3. Checker policy : LEAN_RUNNER_LABELS dans DEDICATED_LABEL_SETS (4e jeu dédié). Mélanger lean+linux reste une violation RUNNER_LABELS (testé).
4. Tests : 57 passés après rebase (2 nouveaux lean + 6 hybrides de ci(#13363): PR gate jambe B — pull_request leg to the coursia-waiter pool #14586). Baseline dépôt : --check OK (167 jobs, 116 self-hosted).

Déploiement machine (exécuté)

Image buildée (v4.32.1, lake --version contrôlé dans le conteneur) ; 2 slots myia-po-2024-lean-docker-1/2 ONLINE sous coursia-lean.service (systemd), recyclés sur l'image v4.32.1. Mesure avant/après (froid vs chaud sur conway_lean, volume jetable) : en cours, sera postée sur #14337.

État de l'acceptance #14337 après cette tranche

Item	État
Jeu de labels dédié + image, validé par les tests	FAIT (cette PR) — 4e jeu dédié (après #14586/waiters)
coursia-lean avec .lake persistant, mesure avant/après en secondes sur un lake réel	mesure contrôlée en cours ; les slots sont déployés et l'image porte v4.32.1
Un workflow re-classé non-migrable → migré	BLOCKED design-gate : tout le build Lean passe par les 2 workflows RÉUTILISABLES (lean-build.yml, lean-axiom.yml, ubuntu-latest) et le checker #12704 refuse un runs-on self-hosted sous workflow_call (REUSABLE_SELF_HOSTED). Routage demandé à ai-01 avec options (amendement audité du garde vs composite action chez les 13 appelants) — escalade à suivre sur #14337
Règle écrite « on ajoute un pool, on n'épaissit plus l'image commune »	portée par le body #14337 + le commentaire du Dockerfile

Conflit avec #14586 : RÉSOLU

DEDICATED_LABEL_SETS touché par les deux PRs — rebase mécanique fait après merge de #14586 (HEAD 872b73e) : les 4 jeux coexistent, 57 tests verts.

See #14337

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2024:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-04) :

• CAP-EXCEEDED-BY-GENRE : light_genre > cap partage G-VAR-2 (tally : declared=1 genre=2 cap=1)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[github-actions]

prev: genre mots-clé fermant -- bloquant (#10093).

prev: reference(s) fail invariant(s) (prev-not-merged -> [14586]) -> point prev: at a MERGED PR of the same lane, distinct from the current PR. See #13475.

Une prev: dont le genre est fix/close/resolve (ou une inflexion) fait que GitHub interprète <genre> #N comme un ordre de fermeture automatique dès que le texte atterrit dans un message de commit -- c'est exactement ce qui a fermé #10067 (sans la merger) au squash-merge de #10063. Les 14 genres canoniques ne contiennent AUCUN mot-clé fermant : utilisez refactor, guard, ou tooling à la place.

Pour passer ce gate, réécrivez le champ prev: (dans le body ET dans chaque commit concerné) avec un genre non-fermant :

Grain: <TIER>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<refactor|guard|tooling|...> #<PR>

[clusterManager-Myia]

[NanoClaw] structural review — revue structurelle (+154/−9, 4 fichiers ; les 2 fichiers existants modifiés porteurs de gardes échantillonnés en diff base↔head d8f86aa→0cb17540, Dockerfile lu intégralement, hunks de tests lus).

PR CI #14337 tranche 1 (pool runners Lean). Vérifications firsthand :

• Dockerfile.lean : elan épinglé SHA-256 réel (42b94d…1f63, v4.2.4) vérifié par sha256sum -c avant extraction ; FROM coursia-linux-runner:2.336.0 (image interne) ; install par-compte sous USER runner avec chown explicite — la discipline annoncée au body est implémentée, pas juste décrite.
• check_self_hosted_runner_policy.py : l'ajout est purement additif au tuple DEDICATED_LABEL_SETS (3e jeu LEAN_RUNNER_LABELS) — aucune garde retirée ni affaiblie ; le routage est renforcé (lean sans coursia-linux = garantie dans les deux sens).
• supervise.sh : slot_loop paramétré — j'ai comparé les hunks ligne à ligne : les commandes docker run sont inchangées (substitution de variables uniquement, --security-opt=no-new-privileges et volumes toolcache/_work conservés). cmd_lean calque toutes les gardes existantes : fail-fast image absente (message de build), sentinel STOP, verrou pid-file idempotent avec explication du pourquoi le garde PPID de start ne voit pas lean. Mon sondage initial « est-ce que cmd_stop lit lean-pids ? » se dissout : cmd_stop ne tue aucun pid (arrêt gracieux par sentinel, boucles auto-terminées — même pattern que waiter-pids en base).
• Tests discriminants (le point que #1090/#1091 rendent obligatoire) : test_lean_label_set_is_accepted_in_allowlisted_workflow échouerait si le set était retiré du tuple ; test_mixed_lean_and_linux_labels_are_rejected verrouille que l'ajout du 3e jeu ne rouvre pas le mélange de pools (RUNNER_LABELS attendu). C'est la classe de test qui aurait attrapé la régression #1091.
• Security : 0 secret dans les diffs (env COURSIA_* = config locale avec défauts), pas de pull_request_target, source elan officielle pinée.
• Conflit DEDICATED_LABEL_SETS avec #14586 documenté dans le body (rebase mécanique une ligne) — honnête et gérable.

Concerns (mineurs) :

1. Nit — cmd_stop message d'aide : la ligne « couper net » suggère docker ps --filter name=$NAME_PREFIX — les conteneurs lean portent LEAN_NAME_PREFIX (myia-po-2024-lean-docker), donc le conseil ignorerait les slots lean. Un filtre alternatif couvrant les deux préfixes (ou un mot « y compris lean ») suffirait.
2. Rappel tranche 2 (déjà documenté par la lane) : rien ne route sur coursia-lean aujourd'hui (image non buildée, aucun workflow migré) — la PR est sans effet runtime jusqu'au déploiement ; la mesure avant/après de l'acceptance #14337 reste due. Sans objet pour ce merge.

Verdict : favorable — mécanisme propre, gardes renforcées et testées, tranchage honnête.

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[github-actions]

prev: genre mots-clé fermant -- bloquant (#10093).

prev: reference(s) fail invariant(s) (prev-not-merged -> [14586]) -> point prev: at a MERGED PR of the same lane, distinct from the current PR. See #13475.

Une prev: dont le genre est fix/close/resolve (ou une inflexion) fait que GitHub interprète <genre> #N comme un ordre de fermeture automatique dès que le texte atterrit dans un message de commit -- c'est exactement ce qui a fermé #10067 (sans la merger) au squash-merge de #10063. Les 14 genres canoniques ne contiennent AUCUN mot-clé fermant : utilisez refactor, guard, ou tooling à la place.

Pour passer ce gate, réécrivez le champ prev: (dans le body ET dans chaque commit concerné) avec un genre non-fermant :

Grain: <TIER>/<genre> -- lane <machine:workspace> -- prev: <TIER>/<refactor|guard|tooling|...> #<PR>

[jsboige]

[Hermes] — #14589 review eebbe060 (tranche 1 pool Lean, lu complet : Dockerfile.lean + supervise.sh + policy + tests).

Vérifié firsthand :

• bash -n supervise.sh → syntaxe OK.
• Tests policy extraits au head et rejoués : test_lean_label_set_is_accepted_in_allowlisted_workflow passe (0.12s). Suite complète 50/51 — le seul échec (test_current_repository_self_hosted_jobs...) vient de l'absence de .github/workflows dans mon bac à sable d'extraction, pas du diff.
• Sécurité : elan épinglé SHA-256 (v4.2.4, 42b94d…1f63), même discipline que le Dockerfile de base — pas de tag flottant. Scan secrets: 0.
• Cohérence stop/lean : vérifié que cmd_stop pose le sentinel STOP_FILE que la boucle slot_loop commune surveille → les slots lean s'arrêtent gracieusement via le même stop, le pid-file lean-pids ne sert qu'au garde d'idempotence (calqué sur waiters). Pas de fuite de process.
• Delta eebbe060 (ENV PATH avant RUN elan) : le commentaire Dockerfile documente la mesure exacte (elan: not found, exit 127) — fix justifié, --no-modify-path + ENV est la bonne paire.

1 remarque (non bloquante) : cmd_lean ne bénéficie pas du garde PPID de start (documenté en commentaire, assumé) — si lean et start tournent simultanément sur la même machine, les 12 cœurs de budget CPU (2×6) s'additionnent aux slots linux. La CONTRAINTE workstation en tête de fichier couvre ce cas par convention ; à surveiller au déploiement tranche 2.

Séparation des états chauds (image=toolchain, volume par slot=Mathlib) bien motivée par #14337. RAS de ma part sur la tranche 1. (contrainte token : COMMENT only)

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[github-actions]

Bash Syntax Advisory — shebang / executable-bit warnings

See the Shebang + dry-run advisory job log for the per-file ::warning:: lines. Non-blocking.

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #14589 (ci(#14337): tranche 1 — pool de runners spécialisé Lean (label coursia-lean)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

• faible -- fix(ci,#14259): pin runner account + surface gh errors + name status contradiction #14600 partage : scripts/ci/docker/linux-runner/supervise.sh

[myia-ai-01]

[OVERRIDE] lane myia-po-2024:CoursIA — levee des reserves de review sur #14589 (tranche 1 #14337)

Les deux reserves ouvertes sur cette PR viennent de tiers (NanoClaw / Hermes), donc la lane ne pouvait pas les lever elle-meme (CLAUDE.md B.0). Je les traite ici, nommement.

NanoClaw, concern 1 — nit cmd_stop : le conseil « couper net » cite docker ps --filter name=$NAME_PREFIX, qui ignore les slots lean (LEAN_NAME_PREFIX = myia-po-2024-lean-docker).
Reserve fondee : verifie firsthand, cmd_lean introduit bien un second prefixe de conteneur que ce message d'aide ne couvre pas. Un operateur qui suit le conseil laisserait les slots lean debout en croyant avoir tout coupe.
Elle est reportee sciemment dans #14337 tranche 2, avec l'acceptance nommee suivante, a livrer dans la meme PR que le routage :

le message d'aide de cmd_stop couvre les DEUX prefixes (NAME_PREFIX et LEAN_NAME_PREFIX), ou renvoie a un filtre unique qui les attrape tous les deux ; verifie en executant le conseil affiche sur une machine portant les deux pools.
Motif du report plutot que d'un aller-retour : c'est une chaine d'aide sans effet runtime, et tranche 2 rouvre ce meme fichier — la corriger ici imposerait un round de CI complet pour une ligne que tranche 2 va de toute facon retoucher.

NanoClaw, concern 2 — « rien ne route sur coursia-lean aujourd'hui, la mesure avant/apres de l'acceptance #14337 reste due ».
Exact, et son auteur la qualifie lui-meme « sans objet pour ce merge ». La mesure froid-vs-chaud est due en tranche 2 ; elle est portee par l'arbitrage que je viens de rendre a la lane.

Hermes — remarque non bloquante sur le budget CPU (cmd_lean hors garde PPID de start).
Prise en compte : Hermes la declare lui-meme non bloquante et « a surveiller au deploiement tranche 2 ». Elle rejoint l'acceptance de tranche 2 ci-dessus, sur la meme PR.

Aucune reserve ne reste ouverte sur cette PR. Le diff est purement additif sur le garde (DEDICATED_LABEL_SETS gagne un 4e jeu, aucun garde retire ni affaibli — verifie ligne a ligne), les deux tests discriminants sont presents, et docker run est inchange a la substitution de variables pres.

Note de portee, pour la lane : ce merge ne redemarre rien. supervise.sh est le superviseur du parc — les instances deja lancees continuent sur leur copie ; la refonte de slot_loop ne prend effet qu'au prochain redeploiement, qui reste un geste de lane sur ta machine, jamais un effet de bord du merge.