diff --git a/.github/ci-plan.sh b/.github/ci-plan.sh new file mode 100755 index 000000000..7f996443f --- /dev/null +++ b/.github/ci-plan.sh @@ -0,0 +1,91 @@ +#!/usr/bin/env bash +# What a run of ci.yml is (SPEC.md §9.4), decided from the event and the +# repository alone, before any job that costs a runner starts. +# +# pull request, draft the `rest` leg only: a development signal +# pull request, ready the whole gate +# workflow_dispatch the whole gate +# push to main the whole gate, unless the push is a merge whose +# tree is the tree of its second parent and the +# whole gate passed on that parent as a pull +# request run: then nothing, and the run says +# which run verified the tree +# +# Why: a pull request is pushed to several times before its head is final, a +# merge of a head that already contains main lands that head's tree +# unchanged, and each of those runs started the whole gate (about 500 +# runner-minutes on a pool of 20 shared jobs) for a tree whose verdict was +# known or was not going to be read. +# +# Inputs, all from the environment: EVENT, DRAFT, REPO. The jobs read `full` +# and `rows` from GITHUB_OUTPUT. `LEXLEAN_CI_ROWS` and `LEXLEAN_CI_WORKFLOW` +# name the legs file and the workflow when a test runs the script elsewhere. +set -euo pipefail + +rows_file=${LEXLEAN_CI_ROWS:-.github/vv-rows.json} +workflow=${LEXLEAN_CI_WORKFLOW:-.github/workflows/ci.yml} +event=${EVENT:?EVENT names the workflow event} +draft=${DRAFT:-} +repo=${REPO:?REPO names owner/name} +out=${GITHUB_OUTPUT:-/dev/stdout} +summary=${GITHUB_STEP_SUMMARY:-/dev/null} + +emit() { + printf 'full=%s\nrows=%s\n' "$1" "$2" >> "$out" +} + +whole_gate() { + emit true "$(jq -c . "$rows_file")" + printf '%s\n' "$1" >> "$summary" +} + +# The id of a pull request run of this workflow on the second parent of HEAD +# that ran every job of the gate and passed every one, when HEAD is a merge of +# that parent with the same tree. A draft run has only the `rest` leg, so it is +# never one: the run must hold the join of Atlas, every host of the matrix, and +# every leg of the rows file, and no job that did not conclude `success`. +verified_parent_run() { + local parent head_tree hosts runs id names part + parent=$(git rev-parse --verify --quiet 'HEAD^2') || return 1 + head_tree=$(git rev-parse 'HEAD^{tree}') + [ "$head_tree" = "$(git rev-parse "$parent^{tree}")" ] || return 1 + hosts=$(grep -c '^ - { os: ' "$workflow") + runs=$(gh api "repos/$repo/actions/workflows/ci.yml/runs?head_sha=$parent&event=pull_request&status=success&per_page=30" \ + --jq ".workflow_runs[] | select(.head_repository.full_name == \"$repo\") | .id") || return 1 + for id in $runs; do + names=$(gh api "repos/$repo/actions/runs/$id/jobs?per_page=100" --paginate \ + --jq '.jobs[] | "\(.name)\t\(.conclusion)"') || continue + if printf '%s\n' "$names" | awk -F'\t' '$2 != "success" { bad = 1 } END { exit bad }' \ + && printf '%s\n' "$names" | grep -qxF $'atlas (join)\tsuccess' \ + && [ "$(printf '%s\n' "$names" | grep -c '^build and non-Lean tests (')" -eq "$hosts" ]; then + for part in $(jq -r '.[].part' "$rows_file"); do + printf '%s\n' "$names" | grep -qxF "just vv ($part)"$'\tsuccess' || continue 2 + done + printf '%s\n' "$id" + return 0 + fi + done + return 1 +} + +case "$event" in + pull_request) + if [ "$draft" = true ]; then + emit false "$(jq -c '[.[] | select(.part == "rest")]' "$rows_file")" + printf '%s\n' 'Draft pull request: the `rest` leg only. This run is not the gate; marking the pull request ready runs the whole gate.' >> "$summary" + else + whole_gate 'Pull request ready for review: the whole gate.' + fi + ;; + push) + if run=$(verified_parent_run); then + emit false '[]' + printf 'This push merges a head whose tree it equals, and the whole gate passed on that head: run %s of %s. Nothing is run again.\n' "$run" "$repo" >> "$summary" + else + whole_gate 'Push: the whole gate.' + fi + ;; + *) + whole_gate 'Run on request: the whole gate.' + ;; +esac diff --git a/.github/vv-rows.json b/.github/vv-rows.json new file mode 100644 index 000000000..d38e8852d --- /dev/null +++ b/.github/vv-rows.json @@ -0,0 +1,56 @@ +[ + { + "part": "examples", + "recipes": "examples", + "examples_part": "without:uor-atlas", + "bdd_part": "", + "width": "2", + "memory_kib": "12582912", + "hints": ".github/verify-hints.json" + }, + { + "part": "rest", + "recipes": "fmt-check model spec-links lint test features bdd inventory golden repro deny", + "examples_part": "", + "bdd_part": "rest", + "width": "", + "memory_kib": "", + "hints": "" + }, + { + "part": "bdd-compiler", + "recipes": "bdd", + "examples_part": "", + "bdd_part": "compiler", + "width": "", + "memory_kib": "", + "hints": "" + }, + { + "part": "bdd-preservation", + "recipes": "bdd", + "examples_part": "", + "bdd_part": "preservation", + "width": "", + "memory_kib": "", + "hints": "" + }, + { + "part": "bdd-production", + "recipes": "bdd", + "examples_part": "", + "bdd_part": "production", + "width": "", + "memory_kib": "", + "hints": "" + }, + { + "part": "bdd-verification", + "recipes": "bdd", + "examples_part": "", + "bdd_part": "verification", + "width": "", + "memory_kib": "", + "hints": "" + } +] diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e29f6ed8a..30118bd36 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -4,10 +4,11 @@ # `just vv` is the single gate, run from a clean checkout on Linux x86-64 with # the exact pinned toolchains and no build cache: §9.4 says "from a clean # checkout", and a restored target directory is not one. CI runs its twelve -# recipes as legs at once, each its own clean checkout: `examples`, which here -# verifies every example but UOR Atlas, and `rest`, the other eleven in the -# order of `vv`. Together they run every recipe of `vv` exactly once, so the -# gate is the same and the wall time is the longest leg rather than the sum. +# recipes as the legs of `.github/vv-rows.json` at once, each its own clean +# checkout: `examples`, which here verifies every example but UOR Atlas, and +# `rest`, the other eleven in the order of `vv`, with the `bdd` rows below. +# Together they run every recipe of `vv` exactly once, so the gate is the same +# and the wall time is the longest leg rather than the sum. # # `bdd`, the conformance suite, was most of the `rest` leg's time, and it runs # as the parts of `.github/bdd-parts.json` (§9.4): each `bdd-` row runs @@ -28,11 +29,20 @@ # with `expected/verify` as the leg did. Every process of the verification runs # exactly once per run; the executable the shards run is the one the `prefix` # shard built from the clean checkout, carried between the jobs of the run as -# an artifact with the shards' output, and nothing crosses runs. The Atlas -# jobs do not run while a pull request is a draft; they run when it is marked -# ready, which the `pull_request` types below include. `honesty` is split out -# so a claim that has drifted from its evidence reads differently from broken -# code. +# an artifact with the shards' output, and nothing crosses runs. `honesty` is +# split out so a claim that has drifted from its evidence reads differently +# from broken code. +# +# Which runs are the gate (§9.4): the `plan` job decides from the event alone. +# A pull request that is a draft runs the `rest` leg and nothing else, because +# a head pushed again before it is final should cost one job and not the whole +# gate; it is a development signal and the pull request is not mergeable on it. +# Marking it ready, which the `pull_request` types below include, a push to a +# ready pull request, a request, and a push to `main` run every job. One push +# to `main` runs none: a merge whose tree is the tree of its second parent, a +# pull request head that already contained `main`, when the whole gate passed +# on that head as a pull request run; the tree is the one that run verified, +# and the plan records the run. `release.yml` runs `just vv` whole regardless. # # The gate runs on the standard GitHub-hosted runner (SPEC.md §9.4); no larger # runner is part of it. The `examples` leg and every Atlas shard verify at the @@ -78,19 +88,47 @@ env: CARGO_INCREMENTAL: "0" jobs: + # What this run is (SPEC.md §9.4), decided from the event before any job that + # costs a runner starts: a draft pull request runs the `rest` leg and nothing + # else; a ready pull request, a request, and a push to `main` run the whole + # gate, except a push that merges a head whose tree it equals and whose whole + # gate passed (it runs nothing and names the run). `.github/ci-plan.sh` is the + # decision, and RP-14 runs it against planted events. + plan: + name: plan + runs-on: ubuntu-24.04 + timeout-minutes: 10 + permissions: + contents: read + actions: read + outputs: + full: ${{ steps.plan.outputs.full }} + rows: ${{ steps.plan.outputs.rows }} + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + fetch-depth: 2 + - name: Decide what this run is + id: plan + shell: bash + env: + GH_TOKEN: ${{ github.token }} + EVENT: ${{ github.event_name }} + DRAFT: ${{ github.event.pull_request.draft }} + REPO: ${{ github.repository }} + run: .github/ci-plan.sh + vv: name: just vv (${{ matrix.part }}) + needs: [plan] + if: ${{ needs.plan.outputs.rows != '[]' }} # A failing leg does not cancel the others: each leg's evidence is complete. + # The legs are the rows of `.github/vv-rows.json`, or only its `rest` row + # while the pull request is a draft. strategy: fail-fast: false matrix: - include: - - { part: examples, recipes: "examples", examples_part: "without:uor-atlas", bdd_part: "", width: "2", memory_kib: "12582912", hints: ".github/verify-hints.json" } - - { part: rest, recipes: "fmt-check model spec-links lint test features bdd inventory golden repro deny", examples_part: "", bdd_part: "rest", width: "", memory_kib: "", hints: "" } - - { part: bdd-compiler, recipes: "bdd", examples_part: "", bdd_part: "compiler", width: "", memory_kib: "", hints: "" } - - { part: bdd-preservation, recipes: "bdd", examples_part: "", bdd_part: "preservation", width: "", memory_kib: "", hints: "" } - - { part: bdd-production, recipes: "bdd", examples_part: "", bdd_part: "production", width: "", memory_kib: "", hints: "" } - - { part: bdd-verification, recipes: "bdd", examples_part: "", bdd_part: "verification", width: "", memory_kib: "", hints: "" } + include: ${{ fromJSON(needs.plan.outputs.rows) }} runs-on: ubuntu-24.04 # Complete proof coverage is intentionally the long pole. GitHub-hosted # jobs permit six hours; a shorter local-style timeout would turn complete @@ -211,7 +249,8 @@ jobs: # `CensusCert4`, the module that dominates the verification. atlas-prefix: name: atlas (prefix) - if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} + if: ${{ needs.plan.outputs.full == 'true' }} + needs: [plan] runs-on: ubuntu-24.04 timeout-minutes: 360 env: @@ -297,8 +336,8 @@ jobs: # `CensusCert*` modules, and the replays of the prefix. atlas-l1: name: atlas (${{ matrix.shard }}) - if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} - needs: [atlas-prefix] + if: ${{ needs.plan.outputs.full == 'true' }} + needs: [plan, atlas-prefix] strategy: { fail-fast: false, matrix: { shard: [cert4, census-a, census-b, census-c, census-d] } } runs-on: ubuntu-24.04 timeout-minutes: 360 @@ -386,8 +425,8 @@ jobs: # The replay of `CensusCert4`, which needs its `.olean` and nothing after it. atlas-cert4-replay: name: atlas (cert4-replay) - if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} - needs: [atlas-prefix, atlas-l1] + if: ${{ needs.plan.outputs.full == 'true' }} + needs: [plan, atlas-prefix, atlas-l1] runs-on: ubuntu-24.04 timeout-minutes: 360 env: @@ -475,8 +514,8 @@ jobs: # them imports. atlas-closure: name: atlas (closure) - if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} - needs: [atlas-prefix, atlas-l1] + if: ${{ needs.plan.outputs.full == 'true' }} + needs: [plan, atlas-prefix, atlas-l1] runs-on: ubuntu-24.04 timeout-minutes: 360 env: @@ -564,8 +603,8 @@ jobs: # closure modules, and the `ClosurePairCert*` modules in four bins. atlas-l3: name: atlas (${{ matrix.shard }}) - if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} - needs: [atlas-closure] + if: ${{ needs.plan.outputs.full == 'true' }} + needs: [plan, atlas-closure] strategy: { fail-fast: false, matrix: { shard: [orbit, pairs-a, pairs-b, pairs-c, pairs-d] } } runs-on: ubuntu-24.04 timeout-minutes: 360 @@ -655,8 +694,8 @@ jobs: # `expected/verify`. atlas-join: name: atlas (join) - if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }} - needs: [atlas-prefix, atlas-l1, atlas-cert4-replay, atlas-closure, atlas-l3] + if: ${{ needs.plan.outputs.full == 'true' }} + needs: [plan, atlas-prefix, atlas-l1, atlas-cert4-replay, atlas-closure, atlas-l3] runs-on: ubuntu-24.04 timeout-minutes: 360 env: @@ -759,6 +798,8 @@ jobs: # own `xtask` and `repo-conformance`, which no host in this job runs. host-matrix: name: build and non-Lean tests (${{ matrix.target }}) + needs: [plan] + if: ${{ needs.plan.outputs.full == 'true' }} strategy: fail-fast: false matrix: diff --git a/CHANGELOG.md b/CHANGELOG.md index 4d667a4b9..777a7d6bb 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,16 @@ versions, and the entries below say what each tag does and does not claim. ## Unreleased +- CI cost, #131 (SPEC.md §8.3, §9.4, `RP-14`): `ci.yml` begins with a `plan` + job (`.github/ci-plan.sh`) that decides what a run is from the event alone. + A draft pull request runs the `rest` leg and no other job (about 23 runner + minutes instead of about 300); a ready pull request, a request, and a push to + `main` run the whole gate; a push to `main` that merges a head whose tree it + equals runs nothing when a pull request run of that head passed every job, + the join of Atlas, every host, and every leg, and says which run. The legs of + the gate are the rows of `.github/vv-rows.json`, the matrix the plan hands + to `vv`. `release.yml` still runs `just vv` whole and reads no earlier run. + The register is unchanged: the statement of `RP-14` is extended. - The decoder of a version 2 core module no longer takes a derived row from the data (`SM-33`, SPEC.md §17.10, part 1 of #91 stage 2): a row whose name the pinned Lean reserves (matcher equations and splitters, definition diff --git a/CONFORMANCE.md b/CONFORMANCE.md index c7753adb1..a625d5d43 100644 --- a/CONFORMANCE.md +++ b/CONFORMANCE.md @@ -459,7 +459,7 @@ the error registry does not sanction (R5, `ERRORS.md`). | `RP-11` | `build` | Every public README capability claim is tied to a registered model ID and honesty level. | | `RP-12` | `build` | A release is refused unless the complete release criterion and all required artifacts are satisfied. | | `RP-13` | `build` | The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice, and that the parts of the committed bdd plan together equal the bdd phase with every test in exactly one part. | -| `RP-14` | `build` | The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence. | +| `RP-14` | `build` | The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence; a plan job decides what a run is from the event alone: a draft pull request runs the rest leg and no other job, a ready pull request, a request, and a push to main run every job, and a push to main that merges a head whose tree it equals runs none when the whole gate passed on that head, and runs the whole gate when any job of that run did not pass, was skipped, or is missing. | ## runtime diff --git a/SPEC.md b/SPEC.md index bd320a1e2..cfaaf8a6c 100644 --- a/SPEC.md +++ b/SPEC.md @@ -555,7 +555,7 @@ The Rust crate MUST build and its non-Lean tests MUST pass on: - macOS AArch64; - Windows x86-64. -`ci.yml` checks this on each of them with one `cargo test --locked --workspace --all-features --no-fail-fast`, which reports every failing test of the host in one run and not the first failing test binary's (a host with two independent failures would otherwise cost one run for each), and which builds the library and the binary of the crate in the same profile, with the same locking and features, before it runs any test; there is no separate build step, because it would build nothing that run does not. The normative full verification and reproducibility gate runs on Linux x86-64. Other hosts produce platform-bound attestations and MUST obey the same source, manifest, and policy formats. +`ci.yml` checks this on each of them, in every run that is the whole gate (§9.4), with one `cargo test --locked --workspace --all-features --no-fail-fast`, which reports every failing test of the host in one run and not the first failing test binary's (a host with two independent failures would otherwise cost one run for each), and which builds the library and the binary of the crate in the same profile, with the same locking and features, before it runs any test; there is no separate build step, because it would build nothing that run does not. The normative full verification and reproducibility gate runs on Linux x86-64. Other hosts produce platform-bound attestations and MUST obey the same source, manifest, and policy formats. Non-UTF-8 project paths are outside language 1.0 and produce a registered environment diagnostic. @@ -679,13 +679,15 @@ Its post-create command MUST install the pinned Lean toolchain explicitly and MU `ci.yml` MUST run every recipe of `just vv` from a clean checkout on Linux x86-64. It MUST install the exact Rust toolchain, Lean 4.32.1 through `elan`, `just`, and `cargo-deny`. -The job runs the recipes as legs of one matrix, at once, each from its own clean checkout: `examples`, which verifies every example but UOR Atlas; `rest`, the other eleven recipes in the order of `vv`; and one `bdd-` row for each named part of the `bdd` plan below, which runs `bdd` alone. Each leg runs `just` with its recipes, which stops at the first that fails, as `vv` does. The part of `examples` a job runs is named by its matrix row through `LEXLEAN_EXAMPLES_PART` and by nothing else: `without:uor-atlas` on the leg, `shard:uor-atlas:` and `join:uor-atlas` on the Atlas jobs below; unset or empty, which is what `just vv` and `release.yml` run, the recipe verifies every example whole. Together the legs and the Atlas jobs run every recipe of `vv`, every example, and every test of `bdd` exactly once, and the gate passes only when every job passes, so it proves what one run of `just vv` proves; no recipe depends on another having run, and every recipe owns the files it builds. Its wall time is the longest path through the jobs rather than the sum. `just vv` remains the acceptance recipe of §9.2 for every other run, and `release.yml` runs it whole. +**What a run is.** `ci.yml` starts with the job `plan`, which decides from the event and the repository alone, through `.github/ci-plan.sh`, what the run is before any job that costs a runner starts. A pull request that is a draft is the `rest` leg and nothing else: a head pushed again before it is final costs one job and not the gate, the run is a development signal, and a draft is not mergeable on it; marking the pull request ready, and every push to it after, run the whole gate. A ready pull request, a `workflow_dispatch`, and a push to `main` are the whole gate, every job below. One push to `main` is not: when it is a merge commit whose tree is the tree of its second parent (a pull request head that already contained `main`) and a run of this workflow for that parent as a pull request of this repository passed every job, with none skipped, the join of Atlas, every host of §8.3, and every leg of `.github/vv-rows.json` among them, the push runs no job but the plan, which records the run: the tree it lands is byte for byte the tree that run verified, on the same runners and with the same pins. Any other push to `main`, including one the plan cannot decide (a failed query, no run, a run of a draft, a merge that changed the tree, a push that is no merge), is the whole gate. `release.yml` runs `just vv` whole and reads no earlier run. `RP-14` runs the script against planted events and a plant in it fails the case. -UOR Atlas is verified as the parts of one run. `.github/verify-shards.json` partitions its verification into shards, each naming the shards it needs, the modules it elaborates, and the modules it replays and audits, one of them named `join`; `cargo xtask ci-shards` checks, as the verifier would when a part ran, that every module is elaborated by exactly one shard and replayed by exactly one, that every import of a module a shard elaborates or replays is elaborated by that shard or by one it needs, directly or through another, and that `join` needs every other shard. Each shard is a job of its own clean checkout that runs the verifier's prelude whole (certificate generation, the preflights, staging, the generated-source audit, the probe), then elaborates, replays, and audits only the modules of its plan, reading the `.olean` files of the modules it imports from the output the jobs of the shards it needs uploaded in the same run, and uploads its own `.olean` files and process records as its output. The join runs the modules of its plan, reads every shard's records, requires each to name the executable the join itself hashed for the tool that produced it (`lean` for an elaboration or an audit member, `leanchecker` for a replay), judges each as the stage that produced it judges its own, and continues through policy, the attestation over every record in the canonical order of §22.11, publication, and the comparison of every normalized record with `expected/verify` (§29.5): what it publishes is what the whole verification publishes, record for record and attestation identity included (`VR-23`). A module without a record from any part, a record of a process no module owns, a record whose `executable_sha256` is not the join's digest of its tool (`LLI9001`, naming the record and both digests), or a shard whose plan leaves a module without the `.olean` it imports fails the run. Every process of the verification runs exactly once per run. The executable the Atlas jobs run is the one the `prefix` job built from its clean checkout, carried to the other jobs of the run as an artifact beside the shards' output; it, the output, and the records cross no run, and a job reads the artifacts of its own run only. The Atlas jobs run after the jobs of the shards they need, at the profile of the `examples` leg, and not while a pull request is a draft: they run when it is opened, pushed to, reopened, or marked ready. +In a run that is the whole gate, the job runs the recipes as the legs of one matrix, the rows of `.github/vv-rows.json`, at once, each from its own clean checkout: `examples`, which verifies every example but UOR Atlas; `rest`, the other eleven recipes in the order of `vv`; and one `bdd-` row for each named part of the `bdd` plan below, which runs `bdd` alone. Each leg runs `just` with its recipes, which stops at the first that fails, as `vv` does. The part of `examples` a job runs is named by its matrix row through `LEXLEAN_EXAMPLES_PART` and by nothing else: `without:uor-atlas` on the leg, `shard:uor-atlas:` and `join:uor-atlas` on the Atlas jobs below; unset or empty, which is what `just vv` and `release.yml` run, the recipe verifies every example whole. Together the legs and the Atlas jobs run every recipe of `vv`, every example, and every test of `bdd` exactly once, and the run passes only when every job passes, so it proves what one run of `just vv` proves; no recipe depends on another having run, and every recipe owns the files it builds. Its wall time is the longest path through the jobs rather than the sum. `just vv` remains the acceptance recipe of §9.2 for every other run, and `release.yml` runs it whole. + +UOR Atlas is verified as the parts of one run. `.github/verify-shards.json` partitions its verification into shards, each naming the shards it needs, the modules it elaborates, and the modules it replays and audits, one of them named `join`; `cargo xtask ci-shards` checks, as the verifier would when a part ran, that every module is elaborated by exactly one shard and replayed by exactly one, that every import of a module a shard elaborates or replays is elaborated by that shard or by one it needs, directly or through another, and that `join` needs every other shard. Each shard is a job of its own clean checkout that runs the verifier's prelude whole (certificate generation, the preflights, staging, the generated-source audit, the probe), then elaborates, replays, and audits only the modules of its plan, reading the `.olean` files of the modules it imports from the output the jobs of the shards it needs uploaded in the same run, and uploads its own `.olean` files and process records as its output. The join runs the modules of its plan, reads every shard's records, requires each to name the executable the join itself hashed for the tool that produced it (`lean` for an elaboration or an audit member, `leanchecker` for a replay), judges each as the stage that produced it judges its own, and continues through policy, the attestation over every record in the canonical order of §22.11, publication, and the comparison of every normalized record with `expected/verify` (§29.5): what it publishes is what the whole verification publishes, record for record and attestation identity included (`VR-23`). A module without a record from any part, a record of a process no module owns, a record whose `executable_sha256` is not the join's digest of its tool (`LLI9001`, naming the record and both digests), or a shard whose plan leaves a module without the `.olean` it imports fails the run. Every process of the verification runs exactly once per run. The executable the Atlas jobs run is the one the `prefix` job built from its clean checkout, carried to the other jobs of the run as an artifact beside the shards' output; it, the output, and the records cross no run, and a job reads the artifacts of its own run only. The Atlas jobs run after the jobs of the shards they need, at the profile of the `examples` leg, and only in a run that is the whole gate. The `bdd` recipe runs as the parts of one run as well. `.github/bdd-parts.json` names parts of the `repo-conformance` suite by conformance ID, and a remainder, `rest`, that names none; the cases that share a fixture built once per test process, such as a verified project, an exported package set, or a compiled environment, are named by one part, so that a fixture is built in one part and not once per part. `cargo xtask bdd` runs `cargo test -p repo-conformance --all-features` with the harness filters of the part `LEXLEAN_BDD_PART` names: `--exact` and the test of every ID the part names, or for the remainder `--exact` and a `--skip` of every test another part names, so that the remainder runs the library tests, the doctests, the meta-gate target, and every conformance test no other part names, an ID added to the register included. The part a job runs is named by its matrix row and by nothing else: a `bdd-` row names its part, the `rest` leg names the remainder, and the `examples` leg runs no `bdd` and names none; unset or empty, which is what `just vv` and `release.yml` run, the recipe runs the whole suite. The harness selects the tests, and no case decides whether it runs. `inventory` proves from the harness's own lists that the parts are disjoint and together are `bdd` (§9.2), and every part, the remainder included, is run by exactly one row. Each row builds from its own clean checkout; nothing passes between rows, and nothing crosses runs. -Every gate job runs on the standard GitHub-hosted runner, `ubuntu-24.04`; no larger runner is part of the gate. The verification resource profile (§22.11) of a job is named by its matrix row, or on an Atlas job by the job itself, and by nothing else, no repository or workflow variable and no input: the `examples` leg and every Atlas job verify at width 2, with the scheduling hints committed in `.github/verify-hints.json` (derived from a run's telemetry by `cargo xtask ci-hints`) and a memory budget of 12 GiB (12582912 KiB) for the summed expected peaks of the proof processes running at once; the other legs name no profile and run at the default. A profile is a schedule and never a verdict: every elaboration, replay, and audit member still runs on the pinned toolchain, the directory each project publishes is byte for byte the one of width 1 without hints or a budget (§22.11), and the leg and the join still require every example's normalized verification records to equal `expected/verify` (§29.5), so a profile that changed a byte would fail the gate rather than pass a different one. A stale hint reorders processes and never skips one. Width 1 is still verified whole on UOR Atlas by `release.yml`, which runs `just vv` with no profile. The budget is below the runner's 16 GB, with the 4 GiB swap file of the job as overflow, so two processes run together only when their expected peaks fit, and a process whose expected peak alone passes the budget runs alone. The gate has no path filter, no cache of a build directory, object, verification tree, attestation, or proof result, and no condition that skips a recipe of `just vv`; the artifacts the jobs of one run exchange are read by that run alone, and every job starts from a clean checkout with the exact pinned toolchains. Each job writes its performance telemetry (§22.12) to `ci-evidence/` and uploads that directory as the artifact named after it, `acceptance-gate-evidence-` or `acceptance-gate-evidence-atlas-`: the gate log (`just --timestamp` stamps each recipe's first command on a leg, which is how a recipe is timed without changing it; an Atlas job's log is the recipe's own output), the host's memory and swap sampled every five seconds, the verifier's telemetry, and a summary of the wall time of each recipe and verification stage, the slowest modules and audit members, and the peak resident set and swap of the proof processes. The summary step also prints that summary to the job log and appends it to the step summary, and runs when the job failed, because an uploaded artifact cannot be read from the log; each table lists only its slowest rows and the part appended to the step summary is cut at 512 KiB, half of what GitHub accepts. None of it is an input of any recipe, and a timing is never a claim about a semantic property. +Every gate job runs on the standard GitHub-hosted runner, `ubuntu-24.04`; no larger runner is part of the gate. The verification resource profile (§22.11) of a job is named by its matrix row, or on an Atlas job by the job itself, and by nothing else, no repository or workflow variable and no input: the `examples` leg and every Atlas job verify at width 2, with the scheduling hints committed in `.github/verify-hints.json` (derived from a run's telemetry by `cargo xtask ci-hints`) and a memory budget of 12 GiB (12582912 KiB) for the summed expected peaks of the proof processes running at once; the other legs name no profile and run at the default. A profile is a schedule and never a verdict: every elaboration, replay, and audit member still runs on the pinned toolchain, the directory each project publishes is byte for byte the one of width 1 without hints or a budget (§22.11), and the leg and the join still require every example's normalized verification records to equal `expected/verify` (§29.5), so a profile that changed a byte would fail the gate rather than pass a different one. A stale hint reorders processes and never skips one. Width 1 is still verified whole on UOR Atlas by `release.yml`, which runs `just vv` with no profile. The budget is below the runner's 16 GB, with the 4 GiB swap file of the job as overflow, so two processes run together only when their expected peaks fit, and a process whose expected peak alone passes the budget runs alone. The gate has no path filter, no cache of a build directory, object, verification tree, attestation, or proof result, and no condition that skips a recipe of `just vv` but the plan's, which decides only what a run is, as above; the artifacts the jobs of one run exchange are read by that run alone, and every job starts from a clean checkout with the exact pinned toolchains. Each job writes its performance telemetry (§22.12) to `ci-evidence/` and uploads that directory as the artifact named after it, `acceptance-gate-evidence-` or `acceptance-gate-evidence-atlas-`: the gate log (`just --timestamp` stamps each recipe's first command on a leg, which is how a recipe is timed without changing it; an Atlas job's log is the recipe's own output), the host's memory and swap sampled every five seconds, the verifier's telemetry, and a summary of the wall time of each recipe and verification stage, the slowest modules and audit members, and the peak resident set and swap of the proof processes. The summary step also prints that summary to the job log and appends it to the step summary, and runs when the job failed, because an uploaded artifact cannot be read from the log; each table lists only its slowest rows and the part appended to the step summary is cut at 512 KiB, half of what GitHub accepts. None of it is an input of any recipe, and a timing is never a claim about a semantic property. `honesty.yml` MUST run the model/honesty gate separately so claim drift is distinguishable from code failure. @@ -9188,7 +9190,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte | `RP-11` | `repository` | Every public README capability claim is tied to a registered model ID and honesty level. | §27 | | `RP-12` | `repository` | A release is refused unless the complete release criterion and all required artifacts are satisfied. | §30 | | `RP-13` | `repository` | The ordinary workspace test phase excludes repo-conformance, the bdd phase alone runs its complete suite, and a test inventory proves that the two phases together equal the whole workspace test set with no test lost and none run twice, and that the parts of the committed bdd plan together equal the bdd phase with every test in exactly one part. | §9.2 | -| `RP-14` | `repository` | The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence. | §9.4 | +| `RP-14` | `repository` | The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence; a plan job decides what a run is from the event alone: a draft pull request runs the rest leg and no other job, a ready pull request, a request, and a push to main run every job, and a push to main that merges a head whose tree it equals runs none when the whole gate passed on that head, and runs the whole gate when any job of that run did not pass, was skipped, or is missing. | §9.4 | | `CF-01` | `configuration-lock` | Project configuration accepts exactly the project/1 schema and rejects unknown or missing fields. | §10.1 | | `CF-02` | `configuration-lock` | Every operational limit is explicit, positive, parsed with checked arithmetic, and has no hidden default. | §10.2 | | `CF-03` | `configuration-lock` | Configured paths resolve within the project under the specified UTF-8 and nonsymlink rules. | §10.1, §25.1 | diff --git a/VERIFICATION.md b/VERIFICATION.md index 8e6eea0a9..73179df60 100644 --- a/VERIFICATION.md +++ b/VERIFICATION.md @@ -8457,3 +8457,38 @@ derived from them alone (the compiler-semantics, source, semantic, and build IDs, and the digests of its lock and its source map); the committed language-1.2 records are regenerated in the wave the maintainer names, not by this change. + +## The plan of a CI run can fail (RP-14, #131) + +`.github/ci-plan.sh` decides what a run of `ci.yml` is: the `rest` leg for a +draft pull request, the whole gate for a ready pull request, a request, and a +push, and nothing for a push that merges a head whose tree it equals when the +whole gate passed on that head. A decision that skips jobs is a gate that can +pass without evidence, so `RP-14` runs the script in a scratch repository with a +stand-in for `gh` against planted events (a draft, a ready pull request, a +request, a push, a merge that lands its head's tree with a run that passed +every job, and each way that evidence can fall short) and requires the whole +gate everywhere the evidence is not complete. Each defect below was planted, +`cargo test -p repo-conformance --test conformance conformance_rp_14 -- --exact` +run, and the defect removed. The observed lines are the case's own. + +| Planted defect | Observed | +| --- | --- | +| the tree of the merge is not compared with the tree of its second parent | `ci-plan.sh` returns no job for a merge that changed the tree (`repository.rs:381`, left: nothing, right: the whole gate) | +| a job that did not conclude `success` is accepted | `§9.4: a skipped job is not the whole gate passing` | +| the join of Atlas is not required of the run | `§9.4: no Atlas join is not the whole gate passing` | +| the number of hosts is not compared with the host matrix | `§9.4: no host is not the whole gate passing` | +| a draft pull request runs the whole gate | `repository.rs:322`, the draft is not the `rest` leg alone | +| a failed query of the runs is read as a pass | `repository.rs:336`, a failed call is not the whole gate | +| the `rest` row of `.github/vv-rows.json` is renamed | `§9.4: the leg a draft pull request runs is the one named `rest`` | +| the host matrix does not wait for the plan | `repository.rs:1792`, `§8.3: the hosts are checked when the plan says the run is the whole gate` | +| an Atlas job decides by the event itself | ``§9.4: `atlas-prefix` runs only when the plan says the run is the whole gate`` | +| `.github/ci-plan.sh` is not executable (the mode it first had in git: the plan failed on a runner with `Permission denied` and skipped every job) | `§9.4: .github/ci-plan.sh is executable` | + +The script's decisions are run on Linux, where the gate runs; on another host of the matrix the case reads the files and skips them. (The first full run of this change failed on Windows for that reason: the stand-in for `gh` was put on a `PATH` written with `:`, so the script found no run and, failing closed, chose the whole gate, which the case refused.) + +Against the previous `ci.yml` the case fails at the missing plan, as R3 requires +(the case was changed before the workflow). The two defects that a stand-in `gh` +cannot show, a run of another repository's pull request and a run that did not +pass, are pinned by the script's own query (`event=pull_request&status=success`, +`head_repository.full_name`), which the case reads. diff --git a/crates/conformance/src/cases/repository.rs b/crates/conformance/src/cases/repository.rs index feb2b4908..1261e26ca 100644 --- a/crates/conformance/src/cases/repository.rs +++ b/crates/conformance/src/cases/repository.rs @@ -129,6 +129,277 @@ fn spec_table() -> Vec<(String, String, String)> { rows } +/// What `.github/ci-plan.sh` decides for planted events (§9.4, RP-14): the +/// script runs in a scratch repository with a stand-in for the `gh` command, +/// so that each decision is shown, and each way of being wrong is refused. +fn plan_decisions() { + use std::process::Command; + // The script is bash with `git`, `jq`, and a stand-in for `gh` on `PATH`, + // run where the gate runs (§8.3, §9.4: the normative host is Linux). The + // other hosts of the matrix run the case's reading of the files and skip + // this part: a Windows `PATH` is not a `:`-separated list, and no + // decision of the plan depends on the host. + if !cfg!(target_os = "linux") { + return; + } + let root = support::repo_root(); + let script = root.join(".github/ci-plan.sh"); + let rows_file = root.join(".github/vv-rows.json"); + let workflow = root.join(".github/workflows/ci.yml"); + let rows: Vec = + serde_json::from_str(&root_file(".github/vv-rows.json")).expect("the legs"); + let parts: Vec = rows + .iter() + .map(|row| row["part"].as_str().expect("a part").to_owned()) + .collect(); + let ci = root_file(".github/workflows/ci.yml"); + let hosts: Vec = ci + .lines() + .filter(|line| line.starts_with(" - { os: ")) + .map(|line| { + let target = line.split("target: ").nth(1).expect("a target"); + format!( + "build and non-Lean tests ({})", + target.trim_end_matches(" }") + ) + }) + .collect(); + assert_eq!(hosts.len(), 4, "§8.3: the four hosts of the matrix"); + // The jobs of a run of the whole gate that passed: the plan, every leg, + // the Atlas join, and every host. The shards do not matter to the plan: + // the join needs them all. + let mut green: Vec = vec!["plan\tsuccess".to_owned()]; + green.extend( + parts + .iter() + .map(|part| format!("just vv ({part})\tsuccess")), + ); + green.push("atlas (prefix)\tsuccess".to_owned()); + green.push("atlas (join)\tsuccess".to_owned()); + green.extend(hosts.iter().map(|host| format!("{host}\tsuccess"))); + + let scratch = tempfile::tempdir().expect("tempdir"); + let dir = scratch.path(); + let git = |args: &[&str]| -> String { + let output = Command::new("git") + .current_dir(dir) + .args([ + "-c", + "user.name=t", + "-c", + "user.email=t@t", + "-c", + "commit.gpgsign=false", + ]) + .args(args) + .output() + .expect("git runs"); + assert!( + output.status.success(), + "git {args:?}: {}", + String::from_utf8_lossy(&output.stderr) + ); + String::from_utf8(output.stdout) + .expect("utf8") + .trim() + .to_owned() + }; + let write = |name: &str, text: &str| std::fs::write(dir.join(name), text).expect("write"); + git(&["init", "-q", "-b", "main"]); + write("a", "a\n"); + git(&["add", "."]); + git(&["commit", "-q", "-m", "base"]); + let base = git(&["rev-parse", "HEAD"]); + // A pull request head that contains main's tip, merged: the merge has the + // tree of the head. + git(&["checkout", "-q", "-b", "head-contains-main"]); + write("b", "b\n"); + git(&["add", "."]); + git(&["commit", "-q", "-m", "change"]); + git(&["checkout", "-q", "main"]); + git(&[ + "merge", + "-q", + "--no-ff", + "-m", + "merge", + "head-contains-main", + ]); + let merge_equal = git(&["rev-parse", "HEAD"]); + assert_eq!( + git(&["rev-parse", "HEAD^{tree}"]), + git(&["rev-parse", "HEAD^2^{tree}"]), + "the planted merge lands its head's tree" + ); + // A pull request head that does not contain main's tip: main moved, so + // the merge has a tree no pull request run verified. + git(&["checkout", "-q", "-b", "head-behind-main", &base]); + write("c", "c\n"); + git(&["add", "."]); + git(&["commit", "-q", "-m", "change"]); + git(&["checkout", "-q", "main"]); + write("d", "d\n"); + git(&["add", "."]); + git(&["commit", "-q", "-m", "main moves"]); + git(&["merge", "-q", "--no-ff", "-m", "merge", "head-behind-main"]); + let merge_different = git(&["rev-parse", "HEAD"]); + assert_ne!( + git(&["rev-parse", "HEAD^{tree}"]), + git(&["rev-parse", "HEAD^2^{tree}"]), + "the planted merge changes the tree of its head" + ); + // A push that is no merge. + write("e", "e\n"); + git(&["add", "."]); + git(&["commit", "-q", "-m", "direct"]); + let direct = git(&["rev-parse", "HEAD"]); + + // `gh`: the runs of the second parent, and the jobs of a run, as the + // environment names them; `STUB_FAIL` makes the call fail. + let bin = dir.join("bin"); + std::fs::create_dir(&bin).expect("bin"); + let stub = bin.join("gh"); + std::fs::write( + &stub, + "#!/usr/bin/env bash\n\ + [ -z \"${STUB_FAIL:-}\" ] || exit 1\n\ + case \"$2\" in\n\ + */workflows/ci.yml/runs\\?*) printf '%s\\n' \"${STUB_RUNS:-}\" ;;\n\ + */runs/*/jobs\\?*) printf '%s\\n' \"${STUB_JOBS:-}\" ;;\n\ + *) exit 2 ;;\n\ + esac\n", + ) + .expect("stub"); + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + std::fs::set_permissions(&stub, std::fs::Permissions::from_mode(0o755)).expect("chmod"); + } + let path = format!("{}:{}", bin.display(), std::env::var("PATH").expect("PATH")); + // (full, rows' parts) for one planted event. + let decide = + |event: &str, draft: &str, commit: &str, runs: &str, jobs: &[String], fail: bool| { + git(&["checkout", "-q", "--detach", commit]); + let out = dir.join("out"); + let _ = std::fs::remove_file(&out); + let mut command = Command::new("bash"); + command + .current_dir(dir) + .arg(script.as_std_path()) + .env("PATH", &path) + .env("EVENT", event) + .env("DRAFT", draft) + .env("REPO", "owner/repo") + .env("LEXLEAN_CI_ROWS", rows_file.as_std_path()) + .env("LEXLEAN_CI_WORKFLOW", workflow.as_std_path()) + .env("GITHUB_OUTPUT", &out) + .env("GITHUB_STEP_SUMMARY", dir.join("summary")) + .env("STUB_RUNS", runs) + .env("STUB_JOBS", jobs.join("\n")); + if fail { + command.env("STUB_FAIL", "1"); + } + let output = command.output().expect("the plan script runs"); + assert!( + output.status.success(), + "the plan script fails closed to the whole gate and never itself: {}", + String::from_utf8_lossy(&output.stderr) + ); + let text = std::fs::read_to_string(&out).expect("outputs"); + let value = |name: &str| -> String { + text.lines() + .find_map(|line| line.strip_prefix(&format!("{name}="))) + .unwrap_or_else(|| panic!("the plan writes `{name}`: {text}")) + .to_owned() + }; + let planned: Vec = + serde_json::from_str(&value("rows")).expect("rows are JSON"); + ( + value("full"), + planned + .iter() + .map(|row| row["part"].as_str().expect("a part").to_owned()) + .collect::>(), + ) + }; + let whole = ("true".to_owned(), parts.clone()); + let draft = ("false".to_owned(), vec!["rest".to_owned()]); + let nothing = ("false".to_owned(), Vec::::new()); + // A draft pull request is the `rest` leg; a ready one, a request, and a + // push are the whole gate when no run is known. + assert_eq!( + decide("pull_request", "true", &direct, "", &[], false), + draft + ); + assert_eq!( + decide("pull_request", "false", &direct, "", &[], false), + whole + ); + assert_eq!( + decide("workflow_dispatch", "", &direct, "", &[], false), + whole + ); + assert_eq!(decide("push", "", &direct, "", &[], false), whole); + // A merge of its head's tree whose whole gate passed runs nothing. + assert_eq!( + decide("push", "", &merge_equal, "4242", &green, false), + nothing + ); + // Every way the evidence can fall short runs the whole gate: no run, a + // run that skipped or failed a job, a run without the Atlas join, one + // host or one leg missing, the gate unreadable, and a merge that changed + // the tree, however good the run of its head. + assert_eq!(decide("push", "", &merge_equal, "", &green, false), whole); + let without = |name: &str| -> Vec { + green + .iter() + .filter(|job| !job.starts_with(name)) + .cloned() + .collect() + }; + let with = |job: &str| -> Vec { + let mut jobs = green.clone(); + jobs.push(job.to_owned()); + jobs + }; + for (what, jobs) in [ + ("a skipped job", with("atlas (closure)\tskipped")), + ("a failed job", with("atlas (closure)\tfailure")), + ("no Atlas join", without("atlas (join)")), + ("no host", without(&hosts[0])), + ("no leg", without("just vv (rest)")), + ( + "a draft run", + vec![ + "plan\tsuccess".to_owned(), + "just vv (rest)\tsuccess".to_owned(), + ], + ), + ] { + assert_eq!( + decide("push", "", &merge_equal, "4242", &jobs, false), + whole, + "§9.4: {what} is not the whole gate passing" + ); + } + assert_eq!( + decide("push", "", &merge_equal, "4242", &green, true), + whole + ); + assert_eq!( + decide("push", "", &merge_different, "4242", &green, false), + whole + ); + assert_eq!(decide("push", "", &direct, "4242", &green, false), whole); + // A run of another repository's pull request is not one of this one's. + let script_text = root_file(".github/ci-plan.sh"); + assert!( + script_text.contains(".head_repository.full_name == \\\"$repo\\\"") + && script_text.contains("event=pull_request&status=success"), + "§9.4: only a passed pull request run of this repository counts" + ); +} + pub(crate) fn run(id: &str) { let root = support::repo_root(); match id { @@ -1033,9 +1304,12 @@ pub(crate) fn run(id: &str) { body.contains("\n runs-on: ubuntu-24.04\n"), "§9.4: the job `{key}` runs on the standard runner" ); + // The plan decides what the run is and runs no recipe: it has + // ten minutes, not the six hours of the proof jobs. + let limit = if key == "plan" { 10 } else { 360 }; assert!( - body.contains("\n timeout-minutes: 360\n"), - "§9.4: the job `{key}` has the six-hour limit" + body.contains(&format!("\n timeout-minutes: {limit}\n")), + "§9.4: the job `{key}` has its limit of {limit} minutes" ); } // The resource profile (§22.11) is chosen by the leg's matrix row @@ -1092,17 +1366,43 @@ pub(crate) fn run(id: &str) { .split_whitespace() .map(str::to_owned) .collect(); - // A matrix row: `- { part: , recipes: "...", examples_part: - // "...", bdd_part: "...", width: "...", memory_kib: "...", hints: - // "..." }`. - let field = |row: &str, name: &str| -> Option { - let start = row.find(&format!(" {name}: \""))? + name.len() + 4; - Some(row[start..start + row[start..].find('"')?].to_owned()) + // A leg, a row of `.github/vv-rows.json`, which the plan job turns + // into the matrix: `{ part, recipes, examples_part, bdd_part, + // width, memory_kib, hints }`, every value a string. A draft pull + // request runs the row whose part is `rest` and no other. + let field = |row: &serde_json::Value, name: &str| -> Option { + row.get(name)?.as_str().map(str::to_owned) }; - let rows: Vec<&str> = vv - .lines() - .filter(|line| line.trim().starts_with("- { part: ")) - .collect(); + let rows: Vec = + serde_json::from_str(&root_file(".github/vv-rows.json")) + .expect("§9.4: the legs file is a JSON array"); + for row in &rows { + assert_eq!( + row.as_object() + .map(|keys| keys.keys().cloned().collect::>()), + Some( + [ + "bdd_part", + "examples_part", + "hints", + "memory_kib", + "part", + "recipes", + "width" + ] + .map(str::to_owned) + .to_vec() + ), + "§9.4: a leg names exactly its part, recipes, and profile: {row}" + ); + } + assert_eq!( + rows.iter() + .filter(|row| field(row, "part").as_deref() == Some("rest")) + .count(), + 1, + "§9.4: the leg a draft pull request runs is the one named `rest`" + ); let legs: Vec> = rows .iter() .filter_map(|row| { @@ -1186,13 +1486,14 @@ pub(crate) fn run(id: &str) { crate::bdd_parts::PLAN_FILE ); if leg.len() == 1 { - assert!( - row.starts_with(&format!(" - {{ part: bdd-{part}, ")), + assert_eq!( + field(row, "part").as_deref(), + Some(format!("bdd-{part}").as_str()), "§9.4: a row that runs bdd alone is named `bdd-{part}`: {row}" ); } assert!( - bdd_rows.insert(part.clone(), (*row).to_owned()).is_none(), + bdd_rows.insert(part.clone(), row.to_string()).is_none(), "§9.4: the part `{part}` of bdd is run by two rows" ); } @@ -1342,10 +1643,11 @@ pub(crate) fn run(id: &str) { ); } assert!( - body.contains( - " if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }}\n" - ), - "§9.4: `{key}` waits only for a pull request to leave draft" + body.contains(" if: ${{ needs.plan.outputs.full == 'true' }}\n") + && needs + .get(key) + .is_some_and(|list| list.iter().any(|need| need == "plan")), + "§9.4: `{key}` runs only when the plan says the run is the whole gate" ); assert!( body.contains("name: acceptance-gate-evidence-atlas-") @@ -1453,7 +1755,7 @@ pub(crate) fn run(id: &str) { ); assert!( ci.contains(" pull_request:\n types: [opened, synchronize, reopened, ready_for_review]\n"), - "§9.4: a pull request marked ready runs the jobs that waited for it" + "§9.4: a pull request marked ready runs the jobs the draft did not" ); for forbidden in [ "actions/cache", @@ -1465,23 +1767,26 @@ pub(crate) fn run(id: &str) { ] { assert!(!ci.contains(forbidden), "ci.yml has no `{forbidden}`"); } - // A condition appears in two forms and nowhere else: a step's + // A condition appears in three forms and nowhere else: a step's // `if: ${{ !cancelled() }}` on the summary and evidence steps, so - // that a failed run still reports, and a job's draft condition on - // the Atlas jobs. Never on the gate step, and never one narrower - // than those (a gate skipped on pull requests is the weaker - // PR-only gate). + // that a failed run still reports; a job's `full` condition on the + // Atlas jobs and the host matrix, which run only when the plan says + // the run is the whole gate; and the legs' condition on `vv`, which + // runs when the plan names a leg. Never on the gate step, and never + // a condition on the event or the pull request itself: what a run + // is, is decided once, by the plan (a gate skipped by a condition + // written elsewhere is the weaker PR-only gate). let mut step_conditions = 0; - let mut draft_conditions = 0; + let mut full_conditions = 0; + let mut rows_conditions = 0; for (index, line) in ci.lines().enumerate() { if line.trim_start().starts_with("if:") { match line { " if: ${{ !cancelled() }}" => step_conditions += 1, - " if: ${{ github.event_name != 'pull_request' || !github.event.pull_request.draft }}" => { - draft_conditions += 1; - } + " if: ${{ needs.plan.outputs.full == 'true' }}" => full_conditions += 1, + " if: ${{ needs.plan.outputs.rows != '[]' }}" => rows_conditions += 1, other => panic!( - "ci.yml:{}: a condition other than a step's `!cancelled()` or an Atlas job's draft condition: {other}", + "ci.yml:{}: a condition other than a step's `!cancelled()` or a job's condition on the plan: {other}", index + 1 ), } @@ -1493,10 +1798,50 @@ pub(crate) fn run(id: &str) { "the summary step and the evidence upload of every gate job carry it" ); assert_eq!( - draft_conditions, - atlas_jobs.len(), - "every Atlas job and no other waits for a pull request to leave draft" + full_conditions, + atlas_jobs.len() + 1, + "every Atlas job and the host matrix, and no other job, wait for the plan to name the whole gate" ); + assert_eq!(rows_conditions, 1, "the legs run when the plan names a leg"); + assert!( + job("host-matrix").contains(" needs: [plan]\n") + && job("host-matrix") + .contains(" if: ${{ needs.plan.outputs.full == 'true' }}\n"), + "§8.3: the hosts are checked when the plan says the run is the whole gate" + ); + assert!( + vv.contains(" needs: [plan]\n") + && vv.contains(" include: ${{ fromJSON(needs.plan.outputs.rows) }}\n"), + "§9.4: the legs of vv are the rows the plan names" + ); + // The plan: one job, no recipe, ten minutes, reading the event and + // the repository and nothing else, through the one script whose + // decisions are run here against planted events. + let plan_job = job("plan"); + assert!( + plan_job.contains(" actions: read\n") + && plan_job.contains(" fetch-depth: 2\n") + && plan_job.contains(" run: .github/ci-plan.sh\n") + && plan_job.contains(" DRAFT: ${{ github.event.pull_request.draft }}\n") + && plan_job.contains(" EVENT: ${{ github.event_name }}\n"), + "§9.4: the plan runs the script on the event and may read the runs of the repository" + ); + // The workflow runs the file as a command: a mode that is not + // executable fails the plan, and with it every job that needs it. + #[cfg(unix)] + { + use std::os::unix::fs::PermissionsExt; + let mode = std::fs::metadata( + support::repo_root() + .join(".github/ci-plan.sh") + .as_std_path(), + ) + .expect("the plan script") + .permissions() + .mode(); + assert!(mode & 0o111 != 0, "§9.4: .github/ci-plan.sh is executable"); + } + plan_decisions(); let gate_step = &ci[ci .find(" - name: Run the normative acceptance gate") .expect("the gate step")..]; diff --git a/features/suites/repository.feature b/features/suites/repository.feature index 170501ef0..2bc850383 100644 --- a/features/suites/repository.feature +++ b/features/suites/repository.feature @@ -97,10 +97,10 @@ Feature: repository And the test lists of the parts of the bdd plan, each taken with the part's harness filters, are disjoint and their union equals the bdd recipe's list, so that a test two parts run or a test no part runs fails the inventory @RP-14 @build - Scenario: The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence. - Given .github/workflows/ci.yml, .github/verify-shards.json, and .github/bdd-parts.json - When the runner, the environment, the job steps, and the plan are read + Scenario: The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence; a plan job decides what a run is from the event alone: a draft pull request runs the rest leg and no other job, a ready pull request, a request, and a push to main run every job, and a push to main that merges a head whose tree it equals runs none when the whole gate passed on that head, and runs the whole gate when any job of that run did not pass, was skipped, or is missing. + Given .github/workflows/ci.yml, .github/vv-rows.json, .github/ci-plan.sh, .github/verify-shards.json, and .github/bdd-parts.json + When the runner, the environment, the job steps, and the plan are read, and the plan script is run against planted events Then every gate job runs on ubuntu-24.04 with the 360-minute limit, and each verification profile variable is set once per job, from the leg's matrix row or as the examples profile on an Atlas job And the leg that runs examples names width 2, a 12 GiB budget, and the committed hints, which the verifier parses, verifies every example but uor-atlas, and every other leg names no profile and no example part, and the legs run the recipes of vv, each exactly once but bdd, which runs once per part of the bdd plan on the one row that names the part, in the order of vv within a leg, through the one gate command And the Atlas jobs run every shard of the plan exactly once, each after the jobs of the shards it needs, from the one executable the prefix job built, the join asserts that Atlas verified, and the plan elaborates and replays every Atlas module exactly once with every import elaborated by the shard or by one it needs - And the vv job has no path filter, no cache action, and no condition on a recipe, the Atlas jobs wait only for a pull request to leave draft, and each job uploads its ci-evidence under a name of its own + And the vv job has no path filter, no cache action, and no condition on a recipe, the Atlas jobs and the host matrix run only when the plan names the whole gate, and each job uploads its ci-evidence under a name of its own, and the plan script names the rest leg alone for a draft pull request and the whole gate for a ready one, a request, and a push, and names no job for a merge whose tree is its second parent's only when a run of that parent passed every job, the Atlas join, every host, and every leg, and for a skipped or failed job, a missing join, host, or leg, a failed call, a changed tree, and a push that merges nothing it names the whole gate diff --git a/model/ids.toml b/model/ids.toml index b1b3edbb2..0b26900ef 100644 --- a/model/ids.toml +++ b/model/ids.toml @@ -90,7 +90,7 @@ statement = "The ordinary workspace test phase excludes repo-conformance, the bd id = "RP-14" level = "build" suite = "repository" -statement = "The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence." +statement = "The normative CI job runs every recipe of just vv in parallel legs that each start from a clean checkout on the standard ubuntu-24.04 runner, each recipe exactly once but bdd, which runs once per part of its committed plan on the row that names the part, the examples leg at the verification resource profile its matrix row names and without UOR Atlas, which the Atlas jobs of the same run verify as the shards of the committed plan and a join at that profile, every process once and nothing across runs, and the other legs at the default, with no cache, path filter, or skipped recipe, and each job uploads its CI evidence; a plan job decides what a run is from the event alone: a draft pull request runs the rest leg and no other job, a ready pull request, a request, and a push to main run every job, and a push to main that merges a head whose tree it equals runs none when the whole gate passed on that head, and runs the whole gate when any job of that run did not pass, was skipped, or is missing." [[id]] id = "CF-01"