From 21c296113a127a5d20d492528d76e724d7b562df Mon Sep 17 00:00:00 2001
From: claude-bot <10+claude-bot@noreply.localhost>
Date: Wed, 21 Oct 2026 10:50:32 +0000
Subject: [PATCH] ci: probe the ubuntu24.04-x64-lean4.35 runner

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FYqwNMyPUHeTbFWg83GQq6
---
 .gitea/workflows/env-probe.yml | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 .gitea/workflows/env-probe.yml

diff --git a/.gitea/workflows/env-probe.yml b/.gitea/workflows/env-probe.yml
new file mode 100644
index 0000000..53db227
--- /dev/null
+++ b/.gitea/workflows/env-probe.yml
@@ -0,0 +1,31 @@
+name: env-probe
+
+on:
+  push:
+    branches: ["ci/**"]
+    paths:
+      - ".gitea/workflows/env-probe.yml"
+  workflow_dispatch:
+
+jobs:
+  probe:
+    runs-on: ubuntu24.04-x64-lean4.35
+    timeout-minutes: 15
+    steps:
+      - name: Who and where
+        run: |
+          echo "runner=${RUNNER_NAME:-unknown} labels=${RUNNER_LABELS:-unknown}"
+          uname -a; id; cat /etc/os-release | head -4
+          echo "in-container: $(test -f /.dockerenv && echo yes || echo no)"
+          nproc; free -h; df -h / /tmp 2>/dev/null
+      - name: Lean toolchain
+        run: |
+          echo "PATH=$PATH"; echo "ELAN_HOME=${ELAN_HOME:-unset} HOME=$HOME"
+          for t in elan lean lake python3 pip3 git node npm docker curl jq sqlite3 gcc; do printf '%-8s ' $t; (command -v $t && $t --version 2>&1 | head -1) || echo MISSING; done
+          ls -d "$HOME/.elan" /opt/elan /usr/local/elan 2>/dev/null || true
+          (elan toolchain list || true) 2>&1 | head
+      - name: Mathlib present anywhere?
+        run: |
+          (find / -maxdepth 4 \( -name 'lake-manifest.json' -o -name '.lake' \) -not -path '/proc/*' 2>/dev/null | head -20) || true
+          (docker images 2>&1 | head -20) || true
+          (docker ps -a 2>&1 | head -10) || true