ci: a plan job decides what a run is — draft PRs run rest, a merge of a verified head runs nothing (#131)

.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

.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": ""
+  }
+]

.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-<part>` 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:

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

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