From 3cfd03a1f70c8a4d027889acdaee4ad94d313bd2 Mon Sep 17 00:00:00 2001
From: Aleksei Rybnikov <14005836+arkh-node@users.noreply.github.com>
Date: Sun, 30 Aug 2026 22:03:48 +0200
Subject: [PATCH] CI: run the full battery on every push and PR

The g-meet regression (d731e5d, fixed in #17) survived 11 days on main
because the landing claimed only the smoke suite green and the repo has
no CI. This workflow runs the unmodified battery (./run_tests.sh) in a
debian:trixie container - the same distribution and apt versions as the
dev machine (SBCL 2.5.2, Agda 2.6.4.3, agda-stdlib 2.1, GHC 9.6.6).

The battery treats a skipped check as a failure by design, so the job
installs the full toolchain instead of weakening the battery. The oracle
builds itself on a cold runner (MAlonzo via GHC); 45-minute cap covers
the first compile.

Fixes #20
---
 .github/workflows/battery.yml | 41 +++++++++++++++++++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 .github/workflows/battery.yml

diff --git a/.github/workflows/battery.yml b/.github/workflows/battery.yml
new file mode 100644
index 0000000..cb74360
--- /dev/null
+++ b/.github/workflows/battery.yml
@@ -0,0 +1,41 @@
+# nolang CI — the full battery, unmodified (issue #20).
+#
+# Why the dev-machine toolchain, not a leaner job: run_tests.sh treats a skipped
+# check as a failure by design. The battery needs sbcl (lisp + mutants), agda
+# (formal section), ghc (the oracle builds itself via MAlonzo), python3
+# (formal/count.sh). Installing the same distribution as the dev machine
+# (Debian 13, trixie) keeps apt package versions identical to local.
+name: battery
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+concurrency:
+  group: battery-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  battery:
+    runs-on: ubuntu-24.04
+    container: debian:trixie
+    timeout-minutes: 45
+    env:
+      LANG: C.UTF-8
+    steps:
+      - name: Install toolchain (same apt versions as the dev machine)
+        run: |
+          apt-get update -qq
+          env DEBIAN_FRONTEND=noninteractive apt-get install -y -qq git sbcl agda ghc python3
+
+      - uses: actions/checkout@v4
+
+      - name: Register the Agda standard library (apt lands it in /usr/share/agda-stdlib)
+        run: |
+          mkdir -p "$HOME/.agda"
+          echo /usr/share/agda-stdlib/standard-library.agda-lib > "$HOME/.agda/libraries"
+          echo standard-library > "$HOME/.agda/defaults"
+
+      - name: Full battery — skips are failures, by design
+        run: ./run_tests.sh