49 lines
2.0 KiB
YAML
49 lines
2.0 KiB
YAML
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
|
|
- name: Read-only storage diagnosis
|
|
run: |
|
|
set -eu
|
|
hostname
|
|
lsblk -e 7 -o NAME,PATH,SIZE,FSTYPE,MOUNTPOINTS
|
|
findmnt -T /var/lib/docker
|
|
df -hT / /var/lib/docker
|
|
docker info --format 'storage={{.Driver}} root={{.DockerRootDir}}'
|
|
docker system df
|
|
docker builder du 2>/dev/null || true
|
|
for dir in /var/lib/docker /var/lib/containerd /opt/lean-cache /var/cache /tmp /var/log; do
|
|
if [ -d "$dir" ]; then du -xhd1 "$dir" 2>/dev/null || true; fi
|
|
done
|
|
for tool in sfdisk growpart resize2fs xfs_growfs; do command -v "$tool" || true; done
|
|
if [ "$(hostname)" = "iZ6we8b3jgd6nc2qehu06lZ" ] && command -v growpart >/dev/null; then
|
|
growpart -N /dev/nvme0n1 3 || true
|
|
fi
|