Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 14 additions & 4 deletions .github/workflows/benchmark-regressions.yml
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,14 @@ jobs:
# label from the event is what lets one job be both without the
# scheduled run reaching a paid runner.
# A pull request from a fork cannot obtain an Ubicloud runner, so it
# falls back to GitHub's hosted pool. Estate rule, 2026-09-15.
# falls back to GitHub's hosted pool. Estate rule, 2026-09-15. So does a
# Dependabot pull request, which hosted runners serve at no charge on a
# public repository; the author is tested, not the actor.
runs-on: >-
${{ github.event_name == 'pull_request' && !github.event.pull_request.head.repo.fork && 'ubicloud-standard-2' || 'ubuntu-latest' }}
${{ github.event_name == 'pull_request'
&& !github.event.pull_request.head.repo.fork
&& github.event.pull_request.user.login != 'dependabot[bot]'
&& 'ubicloud-standard-2' || 'ubuntu-latest' }}
# Thirty-three seconds of work on GitHub's four cores. The ceiling is a
# runaway guard, not a budget, and is set well clear of a cold cargo
# build of chutoro-test-support on two.
Expand Down Expand Up @@ -70,9 +75,14 @@ jobs:
# Paid on the feedback path only, for the same reason as
# benchmark-policy above: the weekly run of this matrix blocks nobody.
# A pull request from a fork cannot obtain an Ubicloud runner, so it
# falls back to GitHub's hosted pool. Estate rule, 2026-09-15.
# falls back to GitHub's hosted pool. Estate rule, 2026-09-15. So does a
# Dependabot pull request, which hosted runners serve at no charge on a
# public repository; the author is tested, not the actor.
runs-on: >-
${{ github.event_name == 'pull_request' && !github.event.pull_request.head.repo.fork && 'ubicloud-standard-2' || 'ubuntu-latest' }}
${{ github.event_name == 'pull_request'
&& !github.event.pull_request.head.repo.fork
&& github.event.pull_request.user.login != 'dependabot[bot]'
&& 'ubicloud-standard-2' || 'ubuntu-latest' }}
timeout-minutes: 30
strategy:
fail-fast: false
Expand Down
11 changes: 9 additions & 2 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,13 @@ jobs:
build-test:
# A pull request from a fork cannot obtain an Ubicloud runner, so it
# falls back to GitHub's hosted pool. Estate rule, 2026-09-15.
# Dependabot pull requests run on the hosted pool too (free on a public
# repository). The author is tested, not the actor, which changes when
# someone else pushes to the branch.
runs-on: >-
${{ github.event.pull_request.head.repo.fork && 'ubuntu-latest' || 'ubicloud-standard-4' }}
${{ (github.event.pull_request.head.repo.fork
|| github.event.pull_request.user.login == 'dependabot[bot]')
&& 'ubuntu-latest' || 'ubicloud-standard-4' }}
# Above the 4,200 s cargo watchdog on the coverage step plus the 900 s
# of work either side of it, and fifteen minutes above that sum rather
# than equal to it. A ceiling sitting on its requirement cancels the
Expand Down Expand Up @@ -224,7 +229,9 @@ jobs:
# A pull request from a fork cannot obtain an Ubicloud runner, so it
# falls back to GitHub's hosted pool. Estate rule, 2026-09-15.
runs-on: >-
${{ github.event.pull_request.head.repo.fork && 'ubuntu-latest' || 'ubicloud-standard-2' }}
${{ (github.event.pull_request.head.repo.fork
|| github.event.pull_request.user.login == 'dependabot[bot]')
&& 'ubuntu-latest' || 'ubicloud-standard-2' }}
timeout-minutes: 30
permissions:
contents: read
Expand Down
7 changes: 6 additions & 1 deletion .github/workflows/kani-pr.yml
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,13 @@ jobs:
# that moves the critical path.
# A pull request from a fork cannot obtain an Ubicloud runner, so it
# falls back to GitHub's hosted pool. Estate rule, 2026-09-15.
# Dependabot pull requests run on the hosted pool too (free on a public
# repository). The author is tested, not the actor, which changes when
# someone else pushes to the branch.
runs-on: >-
${{ github.event.pull_request.head.repo.fork && 'ubuntu-latest' || 'ubicloud-standard-2' }}
${{ (github.event.pull_request.head.repo.fork
|| github.event.pull_request.user.login == 'dependabot[bot]')
&& 'ubuntu-latest' || 'ubicloud-standard-2' }}
timeout-minutes: 30
steps:
- uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
Expand Down
7 changes: 6 additions & 1 deletion .github/workflows/property-tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -32,8 +32,13 @@ jobs:
# recorded in the developers guide.
# A pull request from a fork cannot obtain an Ubicloud runner, so it
# falls back to GitHub's hosted pool. Estate rule, 2026-09-15.
# Dependabot pull requests run on the hosted pool too (free on a public
# repository). The author is tested, not the actor, which changes when
# someone else pushes to the branch.
runs-on: >-
${{ github.event.pull_request.head.repo.fork && 'ubuntu-latest' || 'ubicloud-standard-2' }}
${{ (github.event.pull_request.head.repo.fork
|| github.event.pull_request.user.login == 'dependabot[bot]')
&& 'ubuntu-latest' || 'ubicloud-standard-2' }}
# Keep this above the 600-second HNSW idempotency nextest timeout so setup
# and the earlier property tests do not consume the whole job budget.
timeout-minutes: 20
Expand Down
50 changes: 29 additions & 21 deletions docs/developers-guide.md
Original file line number Diff line number Diff line change
Expand Up @@ -27,22 +27,29 @@ No paid lane names its label outright, because a pull request from a fork
cannot obtain an Ubicloud runner at all. Without a fallback such a job is not
slow, it is unassignable: it sits forever and the pull request never reports.
So every paid lane tests for the fork and falls back to GitHub's pool for that
case alone:
case. It falls back for a pull request Dependabot opened too: hosted minutes
cost nothing on a public repository, and Dependabot opens many pull requests,
which therefore build cold on the hosted pool. The test reads the pull
request's author, not `github.actor`, because the actor is whoever triggered
the run, so a person pushing to a Dependabot branch would flip the runner:

```yaml
runs-on: >-
${{ github.event.pull_request.head.repo.fork
${{ (github.event.pull_request.head.repo.fork
|| github.event.pull_request.user.login == 'dependabot[bot]')
&& 'ubuntu-latest' || 'ubicloud-standard-2' }}
```

Two of the paid jobs also serve a weekly cron, and neither pays for it, so they
carry both conditions at once. Written positively, the paid label is the one
taken when the lane is a pull request and its head is not a fork:
taken when the lane is a pull request, its head is not a fork and its author is
not Dependabot:

```yaml
runs-on: >-
${{ github.event_name == 'pull_request'
&& !github.event.pull_request.head.repo.fork
&& github.event.pull_request.user.login != 'dependabot[bot]'
&& 'ubicloud-standard-2' || 'ubuntu-latest' }}
```

Expand Down Expand Up @@ -77,9 +84,10 @@ test on a sibling field and report it as the guard it is not.

That narrowness is contracted rather than asserted. The mutations run against
it swap `head.repo.fork` for `head.repo.private` in an otherwise identical
expression, and drop the fork guard from a lane that keeps the event guard.
Both are rejected. A future selector on some other condition gets its own entry
in the guard table rather than a looser pattern here.
expression, drop the fork guard from a lane that keeps the event guard, and
drop the Dependabot author test or swap it for `github.actor`. Both are
rejected. A future selector on some other condition gets its own entry in the
guard table rather than a looser pattern here.

It ran on `ubicloud-standard-8` until the shape was measured. On eight cores
the whole "Run property suite" step, compilation and 250 cases together, took
Expand Down Expand Up @@ -215,21 +223,21 @@ shows no figure there.

Table: Every workflow job, the runner it uses, and what it does.

| Workflow | Job | Runner | Purpose |
| --------------------------- | ---------------------------- | --------------------------------------------------------------------------- | --------------------------------------------- |
| `benchmark-regressions.yml` | `benchmark-policy` | `ubicloud-standard-2` on a non-fork pull request, `ubuntu-latest` otherwise | Resolve the benchmark mode and matrix |
| `benchmark-regressions.yml` | `benchmark-smoke` | `ubicloud-standard-2` on a non-fork pull request, `ubuntu-latest` otherwise | Criterion discovery smoke check |
| `benchmark-regressions.yml` | `benchmark-baseline-compare` | `ubuntu-latest` | Compare against the previous commit |
| `ci.yml` | `build-test` | `ubicloud-standard-4`, `ubuntu-latest` for a fork | Format, lint, spelling, contracts, coverage |
| `ci.yml` | `verus-proofs` | `ubicloud-standard-2`, `ubuntu-latest` for a fork | Verus edge-harvest proofs |
| `coverage-main.yml` | `coverage-upload` | `ubicloud-standard-4` | Upload trunk coverage and advance the ratchet |
| `dependabot-automerge.yml` | `automerge` | callee-selected | Reusable workflow, API-bound |
| `kani-pr.yml` | `kani` | `ubicloud-standard-2`, `ubuntu-latest` for a fork | Kani practical harnesses |
| `mutation-testing.yml` | `mutation` | callee-selected | Reusable workflow, scheduled |
| `nightly-kani.yml` | `kani-full` | `ubuntu-latest` | Full Kani harness suite |
| `nightly-portable-simd.yml` | `nightly-portable-simd` | `ubuntu-latest` | Nightly portable-SIMD backend |
| `property-tests.yml` | `property-tests-pr` | `ubicloud-standard-2`, `ubuntu-latest` for a fork | Pull-request property suites |
| `property-tests.yml` | `property-tests-weekly` | `ubuntu-latest` | Weekly deep property suites |
| Workflow | Job | Runner | Purpose |
| --------------------------- | ---------------------------- | ------------------------------------------------------------------------------------------- | --------------------------------------------- |
| `benchmark-regressions.yml` | `benchmark-policy` | `ubicloud-standard-2` on a non-fork, non-Dependabot pull request, `ubuntu-latest` otherwise | Resolve the benchmark mode and matrix |
| `benchmark-regressions.yml` | `benchmark-smoke` | `ubicloud-standard-2` on a non-fork, non-Dependabot pull request, `ubuntu-latest` otherwise | Criterion discovery smoke check |
| `benchmark-regressions.yml` | `benchmark-baseline-compare` | `ubuntu-latest` | Compare against the previous commit |
| `ci.yml` | `build-test` | `ubicloud-standard-4`, `ubuntu-latest` for a fork or Dependabot | Format, lint, spelling, contracts, coverage |
| `ci.yml` | `verus-proofs` | `ubicloud-standard-2`, `ubuntu-latest` for a fork or Dependabot | Verus edge-harvest proofs |
| `coverage-main.yml` | `coverage-upload` | `ubicloud-standard-4` | Upload trunk coverage and advance the ratchet |
| `dependabot-automerge.yml` | `automerge` | callee-selected | Reusable workflow, API-bound |
| `kani-pr.yml` | `kani` | `ubicloud-standard-2`, `ubuntu-latest` for a fork or Dependabot | Kani practical harnesses |
| `mutation-testing.yml` | `mutation` | callee-selected | Reusable workflow, scheduled |
| `nightly-kani.yml` | `kani-full` | `ubuntu-latest` | Full Kani harness suite |
| `nightly-portable-simd.yml` | `nightly-portable-simd` | `ubuntu-latest` | Nightly portable-SIMD backend |
| `property-tests.yml` | `property-tests-pr` | `ubicloud-standard-2`, `ubuntu-latest` for a fork or Dependabot | Pull-request property suites |
| `property-tests.yml` | `property-tests-weekly` | `ubuntu-latest` | Weekly deep property suites |

### Tool installers

Expand Down
10 changes: 8 additions & 2 deletions tests/workflow_contracts/runner_placement_test.py
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
from workflow_support import (
ACTIONLINT_CONFIG,
GITHUB_HOSTED_LABELS,
NON_DEPENDABOT_GUARD,
NON_FORK_GUARD,
PULL_REQUEST_EVENT_GUARD,
conditional_runner,
Expand Down Expand Up @@ -90,7 +91,8 @@ def _paid_labels(job_definition: dict[str, typ.Any]) -> list[str]:
[]
>>> _paid_labels(
... {
... "runs-on": "${{ github.event.pull_request.head.repo.fork"
... "runs-on": "${{ (github.event.pull_request.head.repo.fork"
... " || github.event.pull_request.user.login == 'dependabot[bot]')"
... " && 'ubuntu-latest' || 'ubicloud-standard-2' }}"
... }
... )
Expand Down Expand Up @@ -176,7 +178,7 @@ def test_paid_pull_request_lanes_fall_back_for_forks(workflow_name: str) -> None
Without the fallback the lane does not run slowly, it does not run: the
job sits unassignable and the pull request never reports. So every paid
lane reachable from a ``pull_request`` event has to name the fork test
and fall back to GitHub's pool, and the fallback label is checked too,
and the Dependabot author test, and fall back to GitHub's pool, and the fallback label is checked too,
because falling back to another paid label would fix nothing.
"""
workflow = load_workflow(workflow_name)
Expand All @@ -195,6 +197,10 @@ def test_paid_pull_request_lanes_fall_back_for_forks(workflow_name: str) -> None
f"{workflow_name}:{job_name} chooses a runner without the "
f"{NON_FORK_GUARD} guard; found {sorted(selected.guards)}"
)
assert NON_DEPENDABOT_GUARD in selected.guards, (
f"{workflow_name}:{job_name} chooses a runner without the "
f"{NON_DEPENDABOT_GUARD} guard; found {sorted(selected.guards)}"
)
assert selected.otherwise in GITHUB_HOSTED_LABELS, (
f"{workflow_name}:{job_name} falls back to {selected.otherwise}, "
"which a fork cannot obtain either"
Expand Down
Loading
Loading