Repository navigation
feat(probas,#19310): CausalBridges-00 — Pearl Ladder introductive (Pli 1 Origami causal) #16236
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: PR gate | |
| # The single check that can be made *required* on `main` without deadlocking | |
| # the repository. See issue #9819 and the module docstring of scripts/pr_gate.py. | |
| # | |
| # Background, measured firsthand 2026-08-07: | |
| # | |
| # gh api repos/jsboige/CoursIA/branches/main/protection -> no required_status_checks | |
| # gh api repos/jsboige/CoursIA/rulesets -> [] | |
| # | |
| # Nothing is required. A PR with a red build reports `UNSTABLE` (mergeable), | |
| # never `BLOCKED`, so the only gate is a human reading `gh pr checks` at ~180 | |
| # merges/day. That failed on 2026-08-07: #9762 merged with | |
| # `ci / Lean CI (grothendieck_lean) -> fail`, and `main` stayed red ~5 hours. | |
| # | |
| # Why not simply require the Lean check instead: GitHub counts a check that | |
| # never started as **pending forever** -- a workflow skipped by its `paths:` | |
| # filter never reports `skipped`. Requiring any path-filtered check would make | |
| # every PR that does not touch that path permanently unmergeable. This workflow | |
| # has NO `paths:` filter for exactly that reason: it must reach a verdict on | |
| # every PR, including PRs that trigger no other CI at all. | |
| # | |
| # Enabling it is a repository-settings change and therefore owner-only: | |
| # Settings > Branches > main > Require status checks > add "PR gate" | |
| # | |
| # Status (measured firsthand 2026-08-11, issue #10435): the flip has happened. | |
| # `PR gate` is now a **required** status check on `main` -- a PR with `PR gate` | |
| # as the only non-SUCCESS check reports `BLOCKED`, not `UNSTABLE`. This is why | |
| # the stale-rollup defect (#10435) hurts: a required check that never | |
| # re-aggregates after a guard it depends on flips green leaves the PR BLOCKED | |
| # until a manual rerun (~180 merges/day, not tenable). The structural fix | |
| # (re-aggregate on guard completion via `workflow_run`) is non-trivial -- a | |
| # `workflow_run`-triggered job posts its check-run on the workflow's default | |
| # branch commit, NOT on the PR head SHA, so it is invisible to `gh pr checks` | |
| # and to mergeState until the job also POSTs a check-run onto the PR head SHA | |
| # via the Checks API. That unblock path lives in the sister workflow | |
| # pr-gate-rerun.yml (#10433 item-1, #11519): a `workflow_run` trigger on guard | |
| # completion re-runs THIS workflow for the PR head SHA, so the fresh verdict | |
| # lands in the original check suite (a POSTed same-named check-run lands in a | |
| # foreign suite and GitHub ANDs the two -- measured 78 PRs blocked, #11519). | |
| # Kept in a separate file so this workflow's pull_request trigger does not | |
| # make the delivery canary (derive_always_on_jobs) wait for a | |
| # workflow_run-only job on every PR. | |
| on: | |
| pull_request: | |
| branches: [main] | |
| # #16624 (rev. ai-01 CHANGES_REQUESTED 2026-09-18T06:33Z): `edited` is | |
| # deliberately NOT listened to. The original defect stands -- a PR | |
| # retargeted onto main after living on a stack link emits `edited`, which | |
| # the default types exclude, so the required gate NEVER fired (BLOCKED | |
| # forever with zero red, 14 checks green + APPROVED, measured firsthand on | |
| # #16574) -- but listening to `edited` cannot be made safe HERE, because | |
| # this job IS the required check (`name: PR gate`, job-managed check-run): | |
| # every in-workflow form of "ignore title/body edits" still emits a verdict- | |
| # shaped check-run on the head SHA. A job-level guard yields a SKIPPED | |
| # same-named check-run -- under latest-wins that is the newest verdict for | |
| # the name, and a required check concluded `skipped` counts as passing, so | |
| # editing the body of a red PR would unblock it; an in-job early exit | |
| # concludes SUCCESS (clears the red outright). The only semantics that | |
| # cannot mutate a verdict on a title/body edit is NO RUN AT ALL, hence | |
| # `edited` stays out of the types. | |
| # | |
| # The retarget population is instead caught from the OUTSIDE by the | |
| # pr-gate-stale-sweep.yml gate-absent leg (hourly cron backstop + push | |
| # heartbeat, median 11 min between successful sweeps, #15770): it labels | |
| # the PR, comments the remedy, and auto-dispatches pr-gate-rerun.yml | |
| # `aggregate_absent` for the head (capped MAX_AUTO_REMEDIATE per pass) -- | |
| # the verdict is computed by the same pr_gate.py, never asserted. Manual | |
| # immediacy when wanted: `gh pr close N && gh pr reopen N` from a USER | |
| # token (`reopened` IS a default type; bot tokens are inert, #16624). | |
| # | |
| # `ready_for_review` stays: draft -> ready emits no push, hence no | |
| # synchronize, so without it the draft's `opened` verdict would be the | |
| # last one the PR ever gets. It carries no skip path: the gate always | |
| # runs, computes a real verdict. | |
| types: [opened, synchronize, reopened, ready_for_review] | |
| # No inputs. This leg aggregates the ref it runs on, nothing else. | |
| # | |
| # It carried a `sha` input ('Head SHA to aggregate') that the run step never | |
| # referenced -- the invocation below reads | |
| # `github.event.pull_request.head.sha || github.sha`, so on a dispatch it | |
| # always aggregated the default-branch commit and silently ignored the SHA it | |
| # was handed. Worse, this job has no `--post-check-run`: its check-run lands | |
| # on the commit it ran on, so even a wired input could not have moved a PR's | |
| # mergeState. Removed rather than wired, because the input made | |
| # `gh workflow run pr-gate.yml -f sha=<pr head>` look like the remedy for a | |
| # stale gate verdict -- it is a no-op, and it was tried as such on #11532 | |
| # (2026-08-17) before the real path was found. | |
| # | |
| # To re-aggregate a PR head: dispatch pr-gate-rerun.yml (inputs pr_number + | |
| # head_sha), which POSTs onto the PR head via `--post-check-run`. The | |
| # scheduled sweep in pr-gate-stale-sweep.yml does it automatically. | |
| workflow_dispatch: | |
| permissions: | |
| contents: read | |
| # `write`, not `read`, for #15693: the verdict is PATCHed onto this job's | |
| # OWN check-run `output` so the required check carries its motive. The step | |
| # summary does not reach that surface (measured: it renders on the run page | |
| # while `output.summary` stays null -- see `write_step_summary` in | |
| # scripts/pr_gate.py), and POSTing a twin check-run bearing this required | |
| # name is inert (GitHub ANDs same-named legs in different suites, #11519). | |
| # The PATCH requires a GitHub App token; the job's own GITHUB_TOKEN is one. | |
| # Fork PRs get a read-only token: there the PATCH degrades to a warning and | |
| # the verdict is unaffected. | |
| checks: write | |
| statuses: read | |
| # #13510: on starvation (deadline, nothing red, constituents still | |
| # pending) the script cancels ITS OWN run so the leg concludes CANCELLED | |
| # instead of FAILURE. The PR stays blocked (a cancelled required check is | |
| # not success) and pr-gate-stale-sweep re-drives cancelled gate legs | |
| # exactly like supersession-cancels (#11862). | |
| actions: write | |
| concurrency: | |
| group: pr-gate-${{ github.event.pull_request.number || github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| gate: | |
| # This string is the required-check name. Keep it stable: renaming it | |
| # silently detaches the branch-protection rule, leaving a rule that | |
| # references a check nobody produces -- pending forever, the very deadlock | |
| # this workflow exists to avoid. | |
| name: PR gate | |
| # No `if:` guard here, on purpose (#16624 rev., ai-01 2026-09-18T06:33Z): | |
| # a guard discriminating on `github.event.action == 'edited'` would skip | |
| # the job on title/body edits and emit a SKIPPED check-run under this very | |
| # name -- the newest verdict for the required check, and a `skipped` | |
| # required check counts as passing (a red PR would unblock on a body | |
| # edit). An in-job early exit is worse still (SUCCESS clears the red). | |
| # The edited population is handled entirely outside this workflow by the | |
| # stale-sweep gate-absent leg -- see the trigger comment above. | |
| # #13363 (arbitrage ai-01 2026-09-02, jambes A+B): under load this | |
| # aggregator held 11/14 self-hosted runners just waiting (famine #11405), | |
| # while a short timeout made it FAIL below the Quarto duration it waited | |
| # for (false negative #11770). The third term dissolves the tension: a | |
| # dedicated waiter pool -- waiting costs no CPU. | |
| # - Jambe A (po-2024, #14303 merged + deployed 2026-09-04): 24 waiter | |
| # slots (label coursia-waiter, 1 vCPU / 1 GiB / 128 pids) online via | |
| # coursia-waiters.service -- supervise.sh waiters. | |
| # - Jambe B (this PR): the pull_request leg leaves the shared GitHub- | |
| # hosted queue AND the self-hosted work pool, and waits on the waiter | |
| # pool. Forks stay on ubuntu-latest (fork code never reaches cluster | |
| # runners -- the reason for the same-repo guard #13874), and so do | |
| # workflow_dispatch runs (github.event.pull_request.head is null -> | |
| # the guard is false -> fallback). Semantics unchanged: | |
| # unsettled = FAIL = BLOCKED (#13363 acceptance). | |
| # The form is audited by scripts/ci/check_self_hosted_runner_policy.py: | |
| # exactly this pattern (same-repo guard -> fromJSON coursia-waiter, | |
| # fallback ubuntu-latest); any other expression remains a fail-closed | |
| # DYNAMIC_RUNS_ON violation. Rollback of this leg = revert of this PR. | |
| # Un gate ne depend pas du parc qu'il mesure (#17397). Ce job est un | |
| # agregateur pur -- aucun secret, docker, GPU, Lean, .NET, notebook, conda | |
| # ni WSL -- et il decide si une PR est mergeable. Tant qu'il tournait sur | |
| # `coursia-waiter`, il degradait exactement quand la file qu'il doit | |
| # debloquer grossissait : sur le cycle du 2026-09-22, `PR gate` figure | |
| # parmi les checks fautifs d'une vingtaine des 27 candidates refusees pour | |
| # rouge CI, alors que la cause etait la saturation du parc local. | |
| # Les PRs de fork y allaient deja : la condition ne faisait que priver les | |
| # PRs internes de cette immunite. | |
| runs-on: ubuntu-latest | |
| # Above the script's own budget, so the script prints its verdict | |
| # instead of the runner killing it mid-poll (a runner-killed job reports | |
| # `cancelled`, which is far less legible than "timed out waiting for X"). | |
| # #11405: was 100 min while the script polled 90 -- under runner | |
| # starvation (11+/14 runners held by PR gate) the queue wait alone | |
| # exceeded that budget. The pull_request leg now polls short; when a slow | |
| # guard settles after this leg concluded, pr-gate-rerun.yml re-runs this | |
| # workflow for the PR head SHA (#11519: a rerun, never a same-named | |
| # POSTed check-run -- GitHub ANDs every check-run bearing the required | |
| # name, so the POSTed duplicate could only add failures). Semantics | |
| # unchanged: unsettled = FAIL = BLOCKED. | |
| # #11770: `--timeout-min 28` raises the bounded wait above the p75 of | |
| # Quarto Pages Deploy (measured 2026-08-20: median 1217s p75 1478s, | |
| # 94% of PR runs > 12min). Without the raise, the pull_request leg | |
| # expires while every constituent is still in flight, misclassifies as | |
| # FAIL, and relies on pr-gate-rerun.yml to correct on the same SHA -- | |
| # that works but burns a runner-aggregate cycle on every Quarto-touched | |
| # PR. Workflow timeout raised in lockstep to keep the script's budget | |
| # below the runner's ceiling (28 vs the prior 12). | |
| # #13510: since the STARVED verdict, a self-chosen cancellation is no | |
| # longer the illegible outcome the first comment guards against: the | |
| # script prints "STARVED -- timed out waiting for: X" BEFORE cancelling | |
| # its own run, so the LOG keeps the named constituents while the LEG | |
| # concludes CANCELLED (sweep-recoverable) instead of FAILURE (a red | |
| # lie). The runner-killed case this ceiling prevents is different: no | |
| # verdict is printed at all, which stays worth avoiding. | |
| # #14283/#14412: re-measured 2026-09-03 over the 116 completed Quarto | |
| # Pages Deploy runs since the self-hosted pool switch. The #11770 | |
| # calibration is stale -- it was taken on ubuntu-latest, and the | |
| # self-hosted pool sits a tier slower: 30 of those 116 runs (26%) exceed | |
| # 28 min from run creation, so the bounded wait now expires BELOW the | |
| # distribution it was sized to clear. The numbers are right-censored: | |
| # Quarto's own 30-min ceiling killed 27 of the 69 runs that were not | |
| # concurrency-cancelled (39%), so their true durations are unknown and | |
| # any observed p75 is a floor, not a measurement -- the 42 successes | |
| # (median 24.9 min, p75 26.4 min) are conditional on surviving that | |
| # ceiling, hence biased low. #14412 raises Quarto's ceiling to 60 min, | |
| # and raising it ALONE does nothing while this aggregator self-cancels at | |
| # 28 waiting for it. Measured on this very PR, both runs from the same | |
| # push at 02:34:55Z: PR gate cancelled at 29m23s (03:04:18Z) while its | |
| # own Quarto run went on to SUCCEED at 33m10s (03:08:05Z). That is the | |
| # whole defect in one pair of timestamps -- the raised Quarto ceiling | |
| # worked (under the old 30-min cut that run would have been killed), and | |
| # the aggregator threw the PR away 3m47s before the evidence arrived, | |
| # because the gate that waits for Quarto carried the same stale ceiling | |
| # as the job it waits on. 45 covers the censored mass that sat just above | |
| # the old 30-min cut -- and the one uncensored post-fix observation we | |
| # have, 33m10s, sits ~12 min inside it -- without widening the budget to | |
| # Quarto's full 60; the genuine tail stays on the STARVED -> self-cancel | |
| # path (#13510). Worth re-measuring once more uncensored data exists | |
| # under the 60-min ceiling. | |
| timeout-minutes: 52 | |
| steps: | |
| # #15091 : sparse-checkout en mode cone. Ce job est le SEUL route sur le | |
| # label coursia-waiter, et ce pool n a deliberement aucun volume (ni | |
| # _work, ni toolcache, conteneurs --rm) sous la premisse "un slot qui | |
| # attend ne coute rien" (#13363). La premisse tombe pendant les ~2 | |
| # premieres minutes : un checkout nu materialise 10 387 fichiers / | |
| # 1,14 GiB, puis les detruit -- ~291 runs/jour, soit de l ordre de | |
| # 330 GiB ecrits par jour, sans jamais rien amortir. Le cone rend | |
| # 2 460 fichiers / 16,71 MiB (facteur 70). | |
| # | |
| # Pourquoi le sparse est sur CE pool, et sur lui seul. #14385 a etabli | |
| # que le sparse-checkout empoisonne un _work PERSISTANT : une config | |
| # sparse survivant entre deux jobs tronque l arbre du job suivant, et | |
| # entrypoint.sh porte depuis une boucle de purge pour ca. Mot exact de | |
| # #14385 : "Condition habilitante : le volume _work persistant par slot | |
| # (#14285/#14288). Sans lui, chaque job repartait d un _work vide." | |
| # Le pool d attente n a aucun volume persistant : le mode de defaillance | |
| # y est structurellement impossible. Sur la branche de repli | |
| # ubuntu-latest (PRs de forks), la VM est neuve a chaque job -- meme | |
| # immunite, autre raison. | |
| # | |
| # Cone et non pas non-cone, malgre un facteur 15x moins bon (149 | |
| # fichiers / 1,09 MiB) : le mode non-cone est EXACTEMENT celui qui a | |
| # empoisonne les slots dans #14385, et un cone sur scripts/ ne peut pas | |
| # casser au premier import voisin ajoute a pr_gate.py. Le cone inclut | |
| # aussi les fichiers de la racine, ce qui suffit au reste du job. | |
| # | |
| # Perimetre requis, mesure : pr_gate.py n importe que la stdlib plus | |
| # yaml en import paresseux et scripts/gh_identity.py (#17418 Phase A, | |
| # epinglage du jeton machine — in-come par le cone), et son seul | |
| # chemin est DEFAULT_WORKFLOWS_DIR = <repo>/.github/workflows, que | |
| # derive_always_on_jobs et derive_advisory_jobs globent (canari regle 8). | |
| - uses: actions/checkout@v4 | |
| with: | |
| sparse-checkout: | | |
| scripts | |
| .github/workflows | |
| - uses: actions/setup-python@v5 | |
| with: | |
| python-version: '3.11' | |
| - name: Install canary dependency | |
| # PyYAML drives the rule-8 delivery canary (derive_always_on_jobs reads | |
| # .github/workflows to find jobs that run on every pull_request). If this | |
| # install failed, the script's import guard self-disables the canary -- | |
| # safe (no block) but the #9858 hole would stay open, so install it. | |
| run: pip install pyyaml | |
| - name: Aggregate check verdicts | |
| env: | |
| GH_TOKEN: ${{ github.token }} | |
| # Issue #10072 -- student PRs from forks must remain mergeable under | |
| # the benevolent-policy rule of .claude/rules/student-pr-reviews.md | |
| # ("Template vide + CI rouges = OK. Merge admin via gh auth switch -u | |
| # jsboige"). `enforce_admins: true` on main's required checks would | |
| # block that admin merge, and the gate would then deadlock PRs from | |
| # the ~95 student forks. The same exemption already exists in | |
| # variation-tag-guard.yml (L73-78) and translation-sync.yml (analog); | |
| # this script exposes --is-fork so the verdict is reported as PASS | |
| # without ever polling, keeping the "verdict on every PR" invariant. | |
| IS_FORK: ${{ github.event.pull_request.head.repo.fork }} | |
| run: | | |
| # Pass --is-fork only when IS_FORK is the literal string "true". | |
| # GitHub serialises booleans as "true"/"false" (always set), so the | |
| # `:+` default-expansion is not enough; we test the value explicitly. | |
| if [ "$IS_FORK" = "true" ]; then | |
| IS_FORK_ARG="--is-fork" | |
| else | |
| IS_FORK_ARG="" | |
| fi | |
| python scripts/pr_gate.py \ | |
| --repo "${{ github.repository }}" \ | |
| --sha "${{ github.event.pull_request.head.sha || github.sha }}" \ | |
| --self-name "PR gate" \ | |
| --timeout-min 45 \ | |
| --poll-sec 30 \ | |
| --settle-polls 2 \ | |
| --pr "${{ github.event.pull_request.number }}" \ | |
| --dwell-min 120 \ | |
| $IS_FORK_ARG |