From 9531649bb817e1c2cb49f8e2734f04b1d1307cf4 Mon Sep 17 00:00:00 2001 From: tannevaled Date: Mon, 31 Aug 2026 23:57:15 +0200 Subject: [PATCH] ci: split the docs job so only deploy holds contents: write Build and deploy shared one job, gated at the step level with `if: github.event_name != 'pull_request'`. Step gating decides which steps RUN; it does not change the token the job holds. So the pull request build really did run with `contents: write` -- which is exactly where third-party code runs, a dependency resolved during the build or an action at a floating tag, and it has no use for a token that can push to gh-pages. The job is split in two. `build` keeps `contents: read` and runs on every event, proving `mkdocs build --strict` still passes. `deploy` carries `contents: write` alone and is gated on the same condition that used to sit on the "Configure git" step, so what publishes and when is unchanged. No artifact crosses between the jobs, and none needs to: `mike deploy` runs `mkdocs build` itself and commits its own output to gh-pages, so the site/ the build job produces was already discarded before this split. The build job is the gate, the deploy job publishes -- the same division of labour the single job had, now with a permission boundary between them. The site is built twice on a push, which is the price of publishing byte-for-byte what was published before. The deploy job also takes a concurrency group. `mike deploy --push` pushes gh-pages, and pushing main and a tag together triggers two runs that would race, the loser failing with "! [rejected] gh-pages -> gh-pages (fetch first)". cancel-in-progress stays false: making a publish wait beats killing one part way through. Co-authored-by: Claude Opus 5 --- .github/workflows/docs.yml | 45 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 43 insertions(+), 2 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 4641cd8..949be08 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -6,10 +6,17 @@ on: tags: ["v*"] pull_request: +# The build needs nothing beyond the source it checks out. Write access to the +# repository is granted to the deploy job alone, below, so a pull request build +# cannot push to gh-pages even if a step in it misbehaves. Before this split, +# build and deploy shared ONE job gated only at the step level, which meant the +# pull request build really did run holding `contents: write`. permissions: - contents: write + contents: read jobs: + # Runs on every pull request as well as on main, so a change to the docs or to + # requirements.txt has to prove the site still builds before it lands. build: runs-on: ubuntu-latest steps: @@ -20,9 +27,43 @@ jobs: with: python-version: "3.x" - run: pip install -r requirements.txt + # --strict turns a broken link or an unknown config key into a failure + # rather than a warning nobody reads. - run: mkdocs build --strict + + deploy: + # Only a push publishes; a pull request stops after the build above. This is + # the same condition that used to sit on the "Configure git" step, lifted to + # the job, so WHAT publishes and WHEN is unchanged -- only the token the + # pull request build holds is. + if: github.event_name != 'pull_request' + needs: build + runs-on: ubuntu-latest + permissions: + contents: write + # `mike deploy --push` pushes gh-pages, and two of them at once make the + # second fail outright with "! [rejected] gh-pages -> gh-pages (fetch + # first)". Pushing main and a tag together triggers exactly two runs here. + # cancel-in-progress stays FALSE deliberately: making a publish wait is + # better than killing one half way through. + concurrency: + group: gh-pages-deploy + cancel-in-progress: false + steps: + - uses: actions/checkout@v7 + with: + fetch-depth: 0 + - uses: actions/setup-python@v7 + with: + python-version: "3.x" + - run: pip install -r requirements.txt + # No artifact crosses from the build job on purpose: `mike deploy` runs + # `mkdocs build` itself and commits ITS OWN output to gh-pages, so the + # site/ the build job produced was already thrown away before this split. + # The build job is the gate; this job publishes, exactly as it did when + # both lived in one job. The site is therefore built twice on a push, and + # that is the price of publishing byte-for-byte the same thing as before. - name: Configure git - if: github.event_name != 'pull_request' run: | git config user.name "github-actions[bot]" git config user.email "41898282+github-actions[bot]@users.noreply.github.com"