feat(ci,#15709): lake-build heartbeat -- make long builds visible in the step log

[jsboige]

Grain: MED/tooling -- lane myia-po-2026:CoursIA -- prev: DEEP/slides #15865

See #15709 (items 1-5 delivered as the forensic diagnosis comment; this PR delivers item 6, the "éventuelle" instrumentation PR).

What was wrong

The Lake build step pipelines lake -R build 2>&1 | tee "$RUNNER_TEMP/lake.log" | tail -10, and tail renders its window only at EOF — during the whole build the step log shows nothing. The two wedged knot_lean runs diagnosed in #15709 (job 103451688746: 3 h 13:54 of total console silence after "Already decompressed 8639 file(s)", cache HIT, runner docker-2; rerun job 103592855941: 2 h 10:03, cache MISS, runner docker-1 — same orphan signature lake+tee+tail+lean in both) were cancelled blind at arbitrary durations: the log file on the runner contained the real progress, but nothing surfaced it, so nobody could tell a slow serialized elaboration from a dead hang. With the CI pool under active famine, a runner pinned hours without a readable signal is exactly the failure mode to make legible.

The fix

Run the existing pipeline unchanged inside a subshell, and while the subshell pid is alive, print elapsed time + the tee'd log's last line every 10 min:

• [lake-heartbeat] still running after 30 min - last line: ⏹ info: ... — a growing/dated last line distinguishes slow elaboration from a hang in real time, which settles hypothesis 3 of lean(#15698): diagnostiquer le wedge de 3 h 17 de Proof integrity knot_lean #15709 at the next occurrence instead of after the fact.
• Median build = 8 min → zero heartbeats on the median path (quiet by design; the log stays terse for the 95% case).

Invariants preserved byte-for-byte (the subshell's exit status is what wait returns, pipefail intact):

1. 2026-06-14 pipefail invariant — a FAILED build still exits != 0 (verified in control below).
2. CI: trois gates echouent sans emettre leur diagnostic (lake tronque a tail -10/-20, navlinks en --quiet) #8915 error surfacing — the ::group:: full-log error extraction still fires on failure (verified in control below).

Same one-subject fix on all four carriers of the pattern: composite twins .github/actions/lean-build/action.yml + .github/actions/lean-axiom/action.yml, and reusable workflows .github/workflows/lean-build.yml + .github/workflows/lean-axiom.yml. The lean-knot gate self-covers both action files in its paths: triggers (lesson #8712), so this PR exercises its own gate.

Controls (positive + negative, per the #15709 acceptance)

Harness: exact step structure replicated, tick scaled 600 s → 2 s (scratchpad hb_control.sh):

=== POSITIVE: long build (8s), tick 2s -> expect rc=0, >=2 heartbeats ===
[lake-heartbeat] still running after 10 min - last line: progress: elaborating module 2
[lake-heartbeat] still running after 20 min - last line: progress: elaborating module 4
[lake-heartbeat] still running after 30 min - last line: progress: elaborating module 6
RESULT rc=0 heartbeats=3
=== NEGATIVE-OK: short build (1s) -> expect rc=0, 0 heartbeats ===
RESULT rc=0 heartbeats=0
=== NEGATIVE-FAIL: short failing build (1s) -> expect rc=1, 0 heartbeats, ::group:: fired ===
::group::Error lines from the full lake log (See #8915)
2:error: fake build failure
::endgroup::
RESULT rc=1 heartbeats=0

YAML validity of all four files re-parsed post-edit (yaml.safe_load OK ×4).

Out of scope (deliberately)

• timeout-minutes: 300 backstops (fix(ci,#15698): borner les jobs Lean pour convertir un wedge en red check #15706/Aucun des 12 workflows Lean ne borne son job : un wedge de 3 h 17 immobilise la moitie du pool coursia-lean et son check ne conclut jamais #15698): untouched — they did their job.
• Runner pool / serialization instrument (feat(lean,#2874): preuves kernel conway+KT — maison-mère du split 4 unités (#15434 ✓, #15440, #15460 ✓, #15583) #14821 build-jobs: "1"): untouched.
• The "axiom leg rebuilds the lake under its own cache key" question: CI: pools de runners specialises par labels (cache Mathlib chaud, quarto, navigateurs) plutot qu'une image unique qui grossit #14337 owns it.

Périmètre

4 fichiers, tous sous .github/ : .github/actions/lean-build/action.yml, .github/actions/lean-axiom/action.yml, .github/workflows/lean-build.yml, .github/workflows/lean-axiom.yml. No code, no notebooks, catalogue byte-identical to main.

🤖 Generated with Claude Code

[github-actions]

prev: genre mot-clé fermant (#10093) — LEVÉ (2026-09-13T08:37:18Z).

aucun genre mots-clé fermant dans le body ni les commits ; prev: accepté(s) : #15865

Run vert du garde : ce commentaire bloquant est obsolète. Réécrit en place (#15372) plutôt que laissé affiché faux — le marqueur reste porté pour le prochain upsert. Historique : runs Always-on guards de la PR.

[clusterManager-Myia]

VERDICT: LGTM (vérifié: lecture intégrale des 4 patches — invariant pipefail tracé à travers le refactor)

[Hermes] — lake-build heartbeat #15709 item 6, head c2fdf7fa. Aucune review préexistante.

Lecture complète des 4 fichiers (2 composite actions + 2 workflows, pattern identique ×4) :

1. Invariant CI: trois gates echouent sans emettre leur diagnostic (lake tronque a tail -10/-20, navlinks en --quiet) #8915/pipefail préservé : le pipeline lake | tee | tail partiellement existant est déplacé inchangé dans un subshell ( … ) &. if pipeline; then exempte d'errexit mais $? porte bien le statut pipefail → rc=$? puis exit "$rc" dans le subshell ; le script principal fait wait "$_lake_pipeline" qui propage ce code de sortie. FAILED reste != 0 — l'invariant 2026-06-14 (rfl masqué en CI PASS) est intact.
2. Heartbeat read-only : boucle kill -0 + sleep 600, affiche elapsed + tail -1 | cut -c1-160 — n'écrit rien, n'interrompt rien ; le break après le second kill -0 évite l'affichage d'un heartbeat post-mortem. Le diagnostic lean(#15698): diagnostiquer le wedge de 3 h 17 de Proof integrity knot_lean #15709 (3h13/2h10 de silence console) est directement adressé.
3. Symmetric application : les 4 sites (action.yml lean-axiom/lean-build + workflows lean-axiom.yml/lean-build.yml) portent le même heartbeat — pas de site oublié. Les 2 variantes (tail -10 vs tail -20) préservent leurs différences d'origine.
4. Grain MED/tooling conforme (instrumentation CI, pas de contenu).

Security scan : 0 match (HF_TOKEN|API_KEY|BEARER|PASSWORD|SECRET|TOKEN\s*=).

[github-actions]

Path-collision (organ #13359/#13615)

Cette PR #15929 (feat(ci,#15709): lake-build heartbeat -- make long builds visible in the step log) 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.

• terminal -- ci(lean,#2874): plomberie build-jobs (LEAN_NUM_THREADS) — unité infra du split de PR 14821 #15434 partage : .github/actions/lean-axiom/action.yml, .github/actions/lean-build/action.yml, recouvrement de chemins 50% -- ci(lean,#2874): plomberie build-jobs (LEAN_NUM_THREADS) — unité infra du split de PR 14821 #15434 est deja sur main.
• faible -- fix(search,#13751): standardize Search/Applications/CSP/ Csharp -> CSharp (4 files + 8 refs) #15813 partage : .github/workflows/lean-axiom.yml, .github/workflows/lean-build.yml

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.