CI: a push runs the tests, a pull request also builds the firmware
CI / build (push) Successful in 1m6s

Rebuilding both firmwares on every push was more than anyone looked at.
A push now runs the host tests with their coverage (under two minutes);
a pull request adds the release firmware and the Debug Build, and is how
changes reach main; a tag still does everything before it releases.
Pull requests from forks don't run. scripts/ci.sh takes 'tests' or
'builds' for one half; coverage.sh now fails when a test fails.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01EhqxQ49eCju4CzKYNjZzwT
This commit is contained in:
2026-10-06 14:19:56 +02:00
co-authored by Claude Opus 5.5
parent 5ecd5d003f
commit 86ddb87f54
5 changed files with 27 additions and 16 deletions
+15 -11
View File
@@ -1,7 +1,8 @@
# CI and releases (docs/milestones/R1.md).
# Any push: host tests, the release firmware and the Debug Build, then the tests'
# coverage of lib/; on main, its badge is published to the branch `badges`.
# A tag v*: the same, then a Gitea release with the signed Update File.
# A push: the host tests, with their coverage of lib/. On main, the README's badges
# are published to the branch `badges`.
# A pull request: the same, then the release firmware and the Debug Build.
# A tag v*: all of it, then a Gitea release with the signed Update File.
# Run by hand: the release of a tag that exists already (the ones from before CI).
#
# The job runs in a plain Python image, as scripts/ci.sh does on a developer's machine, with the
@@ -10,8 +11,9 @@
name: CI
on:
push:
branches: ['**', '!badges'] # badges holds what CI itself publishes: the coverage badge
branches: ['**', '!badges'] # badges holds what CI itself publishes
tags: ['v*']
pull_request:
workflow_dispatch:
inputs:
tag:
@@ -21,6 +23,8 @@ on:
jobs:
build:
runs-on: ubuntu
# A pull request from a fork would run someone else's code on our runner: not without us (Q154).
if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository
container:
image: python:3.12-slim
volumes:
@@ -42,18 +46,18 @@ jobs:
git config --global --add safe.directory '*'
git init -q .
git remote add origin "${{ github.server_url }}/${{ github.repository }}.git"
git fetch -q --tags origin '+refs/heads/*:refs/remotes/origin/*'
git fetch -q --tags origin '+refs/heads/*:refs/remotes/origin/*' '+refs/pull/*/head:refs/remotes/pull/*'
git checkout -q --detach "${{ github.sha }}"
git describe --tags --always
- name: Host tests and both builds
if: github.event_name == 'push'
run: scripts/ci.sh
- name: Coverage of lib/ by the host tests
if: github.event_name == 'push'
- name: Host tests, and their coverage of lib/
if: github.event_name != 'workflow_dispatch'
run: scripts/coverage.sh
- name: The release firmware and the Debug Build
if: github.event_name == 'pull_request' || github.ref_type == 'tag'
run: scripts/ci.sh builds
# The README's badges are files on a branch of their own, replaced at each push to main.
- name: Publish the badges
if: github.event_name == 'push' && (github.ref == 'refs/heads/main' || github.ref == 'refs/heads/coverage')