chore(runtime): purge python and deno tooling; bun validator + ban check

.github/workflows/actions.lock

@@ -32,6 +32,7 @@ workflows:
         - 'actions/checkout@v7.0.1'
     '.github/workflows/dogfood-gate.yml':
         - 'actions/checkout@v7.0.1'
+        - 'oven-sh/setup-bun@v2.2.0'
     '.github/workflows/dogfood-proofs-ci.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/formal-verification.yml':
@@ -181,6 +182,11 @@ dependencies:
         commit: 'sha1-d1434d08867e3ee9daa34448df10607b98908d29'
         owner_id: 7289241
         repo_id: 812112570
+    'oven-sh/setup-bun@v2.2.0':
+        ref: 'v2.2.0'
+        commit: 'sha1-0c5077e51419868618aeaa5fe8019c62421857d6'
+        owner_id: 108928776
+        repo_id: 512644635
     'swatinem/rust-cache@v2.9.2':
         ref: 'v2.9.2'
         commit: 'sha1-6323deb102c322ba6fcbdcafc7e3dddab59af2b6'

.github/workflows/dogfood-gate.yml

@@ -249,6 +249,11 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@v7.0.1
 
+      - name: Set up bun
+        uses: oven-sh/setup-bun@v2.2.0
+        with:
+          bun-version: 1.3.14 # matches mise.lock
+
       - name: Check and validate eclexiaiser manifest
         id: eclex
         run: |
@@ -263,34 +268,9 @@ jobs:
 
           echo "has_manifest=true" >> "$GITHUB_OUTPUT"
 
-          # Validate TOML structure using Python 3.11+ tomllib.
-          # The Python heredoc body sits at the YAML block-scalar base
-          # indentation, so after GitHub strips the block's common indent
-          # the interpreter receives it column-aligned (no sed dedent —
-          # a sed-based dedent breaks because YAML removes the block's
-          # leading indent before the script ever reaches the shell).
-          if ! python3 - <<'PY'
-          import tomllib, sys
-          with open('eclexiaiser.toml', 'rb') as f:
-              data = tomllib.load(f)
-          project = data.get('project', {})
-          if not project.get('name', '').strip():
-              print('ERROR: project.name is required', file=sys.stderr)
-              sys.exit(1)
-          functions = data.get('functions', [])
-          if not functions:
-              print('ERROR: at least one [[functions]] entry is required', file=sys.stderr)
-              sys.exit(1)
-          for fn in functions:
-              if not fn.get('name', '').strip():
-                  print('ERROR: function name cannot be empty', file=sys.stderr)
-                  sys.exit(1)
-              if not fn.get('source', '').strip():
-                  print(f'ERROR: function {fn["name"]} has no source path', file=sys.stderr)
-                  sys.exit(1)
-          print(f'Valid: {project["name"]} ({len(functions)} function(s))')
-          PY
-          then
+          # Structural checks live in scripts/validate-eclexiaiser.js (tested by
+          # scripts/validate-eclexiaiser.test.js); bun parses the TOML.
+          if ! bun scripts/validate-eclexiaiser.js eclexiaiser.toml; then
             echo "::error file=eclexiaiser.toml::Invalid eclexiaiser.toml — see step output for details"
             exit 1
           fi
@@ -308,13 +288,36 @@ jobs:
           fi
 
   # ---------------------------------------------------------------------------
-  # Job 6: Dogfooding summary
+  # Job 6: Banned-runtime check (no npm or deno artefacts; bun is the runtime)
+  # ---------------------------------------------------------------------------
+  runtime-ban:
+    name: Banned-runtime check
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@v7.0.1
+
+      - name: Set up bun
+        uses: oven-sh/setup-bun@v2.2.0
+        with:
+          bun-version: 1.3.14 # matches mise.lock
+
+      - name: Test the repo bun scripts
+        run: bun test scripts/
+
+      - name: No npm or deno artefacts
+        run: bash scripts/ban-npm.sh
+
+  # ---------------------------------------------------------------------------
+  # Job 7: Dogfooding summary
   # ---------------------------------------------------------------------------
   dogfood-summary:
     name: Dogfooding compliance summary
     runs-on: ubuntu-latest
     timeout-minutes: 10
-    needs: [a2ml-validate, k9-validate, empty-lint, groove-check, eclexiaiser-validate]
+    needs: [a2ml-validate, k9-validate, empty-lint, groove-check, eclexiaiser-validate, runtime-ban]
     if: always()
 
     steps:

NOTICE

@@ -81,7 +81,7 @@ own licences. See the respective component directories and files for details.
 
 Rust dependencies:    Cargo.toml + `cargo license`
 Julia packages:       Project.toml + Manifest.toml
-Deno / AffineScript:  deno.json (run `deno info`)
+Bun scripts:          scripts/*.js (bun built-ins only, no third-party packages)
 
 Theorem provers (integrated, not redistributed):
   Agda            BSD-3-Clause

hooks/pre-commit

@@ -7,6 +7,9 @@
 # Enable per clone:  git config core.hooksPath hooks
 set -euo pipefail
 
+# Banned runtimes (npm, deno) — fast, needs no toolchain, so it runs before the just check.
+bash scripts/ban-npm.sh
+
 if ! command -v just >/dev/null 2>&1; then
   echo "pre-commit: 'just' not on PATH (RSR-H14 build tool); skipping gate." >&2
   exit 0

scripts/ban-npm.sh

@@ -30,19 +30,20 @@ if find . -type d -name "node_modules" 2>/dev/null | grep -q .; then
     VIOLATIONS=$((VIOLATIONS + 1))
 fi
 
+# Check for Deno manifests or lockfiles (deno is banned estate-wide; bun is the runtime)
+DENO_FILES=$(find . \( -name .git -o -name target -o -name node_modules \) -prune -o -type f \( -name deno.json -o -name deno.jsonc -o -name deno.lock \) -print 2>/dev/null)
+if [ -n "$DENO_FILES" ]; then
+    echo -e "${RED}❌ VIOLATION: Deno manifest or lockfile found${NC}"
+    echo "$DENO_FILES"
+    VIOLATIONS=$((VIOLATIONS + 1))
+fi
+
 # Check for npm/npx usage in scripts
 if grep -r "npm install\|npm i \|npx \|npm run" scripts/ 2>/dev/null | grep -v "ban-npm"; then
     echo -e "${RED}❌ VIOLATION: npm/npx commands found in scripts${NC}"
     VIOLATIONS=$((VIOLATIONS + 1))
 fi
 
-# Check for npm imports in TypeScript (should use https:// or npm: specifier)
-BAD_IMPORTS=$(grep -r "from ['\"][@a-z]" src/provers/ 2>/dev/null | grep -v "from ['\"]https://" | grep -v "from ['\"]npm:" | grep -v "from ['\"]\./" | grep -v "from ['\"]\.\./" || true)
-if [ -n "$BAD_IMPORTS" ]; then
-    echo -e "${YELLOW}⚠️  WARNING: Bare imports found (should use https:// or npm: specifier)${NC}"
-    echo "$BAD_IMPORTS"
-fi
-
 # Check Justfile for npm commands
 if [ -f "Justfile" ] && grep -q "npm\|npx" Justfile; then
     echo -e "${RED}❌ VIOLATION: npm/npx found in Justfile${NC}"
@@ -55,11 +56,10 @@ if [ $VIOLATIONS -eq 0 ]; then
     echo -e "${GREEN}✅ No npm violations found!${NC}"
     echo ""
     echo "Approved package managers:"
-    echo "  ✓ Deno (deno.json, deno task)"
-    echo "  ✓ Bun (only if Deno impossible)"
+    echo "  ✓ Bun (the estate JavaScript runtime)"
     echo ""
     echo "Banned:"
-    echo "  ✗ npm, npx, node_modules"
+    echo "  ✗ npm, npx, node_modules, deno"
     echo "  ✗ package-lock.json"
     exit 0
 else
@@ -68,7 +68,6 @@ else
     echo "To fix:"
     echo "  1. Remove package-lock.json: rm package-lock.json"
     echo "  2. Remove node_modules: rm -rf node_modules"
-    echo "  3. Use 'deno task' instead of 'npm run'"
-    echo "  4. Use https:// or npm: imports in Deno"
+    echo "  3. Use 'bun run' instead of 'npm run'"
     exit 1
 fi

scripts/ban-npm.test.js

@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+//
+// Planted-fixture tests for scripts/ban-npm.sh: each banned artefact is placed
+// in a scratch tree and the script must exit 1; the clean tree must exit 0.
+// Run: bun test scripts/
+import { afterEach, expect, test } from "bun:test";
+import { cpSync, mkdirSync, mkdtempSync, rmSync, writeFileSync } from "node:fs";
+import { tmpdir } from "node:os";
+import { dirname, join } from "node:path";
+
+const SCRIPT = new URL("./ban-npm.sh", import.meta.url).pathname;
+const trees = [];
+
+/** Builds a scratch tree holding the script plus `files` (path → content) and returns its exit code. */
+function runIn(files) {
+  const root = mkdtempSync(join(tmpdir(), "ban-npm-"));
+  trees.push(root);
+  mkdirSync(join(root, "scripts"));
+  cpSync(SCRIPT, join(root, "scripts", "ban-npm.sh"));
+  for (const [path, content] of Object.entries(files)) {
+    mkdirSync(dirname(join(root, path)), { recursive: true });
+    writeFileSync(join(root, path), content);
+  }
+  return Bun.spawnSync(["bash", "scripts/ban-npm.sh"], { cwd: root, stdout: "pipe", stderr: "pipe" }).exitCode;
+}
+
+afterEach(() => { while (trees.length) rmSync(trees.pop(), { recursive: true, force: true }); });
+
+test("a clean tree passes", () => expect(runIn({ "README.adoc": "x\n" })).toBe(0));
+test("package-lock.json fails", () => expect(runIn({ "package-lock.json": "{}" })).toBe(1));
+test("a root deno.json fails", () => expect(runIn({ "deno.json": "{}" })).toBe(1));
+test("a nested deno.lock fails", () => expect(runIn({ "sub/app/deno.lock": "{}" })).toBe(1));
+test("a deno.jsonc fails", () => expect(runIn({ "tools/deno.jsonc": "{}" })).toBe(1));