From 1ddfdf583a5a32226396f2e8716d84fbfea7d6e9 Mon Sep 17 00:00:00 2001 From: Codex Bot Date: Tue, 22 Sep 2026 21:34:22 +0800 Subject: [PATCH] chore: remove CI/CD workflows --- .gitea/workflows/ci.yml | 57 ------- .gitea/workflows/docker.yml | 312 ------------------------------------ .gitea/workflows/ingest.yml | 129 --------------- 3 files changed, 498 deletions(-) delete mode 100644 .gitea/workflows/ci.yml delete mode 100644 .gitea/workflows/docker.yml delete mode 100644 .gitea/workflows/ingest.yml diff --git a/.gitea/workflows/ci.yml b/.gitea/workflows/ci.yml deleted file mode 100644 index 5dba081..0000000 --- a/.gitea/workflows/ci.yml +++ /dev/null @@ -1,57 +0,0 @@ -name: ci - -on: - push: - branches: [main] - pull_request: - workflow_dispatch: - -jobs: - test: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - - # The runner image ships a Debian-managed Python (PEP 668), so installing - # into it is refused and `pip install --upgrade pip` cannot replace the - # distro pip. A venv sidesteps both, and costs a couple of seconds. - - name: Set up a virtualenv - run: | - set -eu - python3 --version - python3 -m venv .venv || { - apt-get update -qq - apt-get install -y -qq python3-venv - python3 -m venv .venv - } - .venv/bin/python -m pip install --quiet --upgrade pip - - - name: Install - run: .venv/bin/python -m pip install --quiet -e ".[dev]" - - - name: Lint - run: .venv/bin/python -m ruff check . - - - name: Test - run: .venv/bin/python -m pytest -q - - - name: CLI is wired up - run: | - set -eu - .venv/bin/lean-bench --help > /dev/null - .venv/bin/lean-bench doctor --skip-llm --env /dev/null - - lean-project: - # Cheap guard: the Lean project's pins must at least resolve. - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v4 - - name: Resolve the Mathlib / toolchain pair - run: | - set -eu - command -v curl >/dev/null || (apt-get update -qq && apt-get install -y -qq curl) - command -v git >/dev/null || (apt-get update -qq && apt-get install -y -qq git) - chmod +x docker/resolve-mathlib.sh - docker/resolve-mathlib.sh lean "${MATHLIB_REV:-auto}" - echo "toolchain: $(cat lean/lean-toolchain)" - grep -E '^rev' lean/lakefile.toml diff --git a/.gitea/workflows/docker.yml b/.gitea/workflows/docker.yml deleted file mode 100644 index cf1a243..0000000 --- a/.gitea/workflows/docker.yml +++ /dev/null @@ -1,312 +0,0 @@ -name: docker - -# Builds the Lean 4 + Mathlib image and LEAVES IT IN PLACE on the runner host. -# -# This is not a throwaway test build. When the job finishes, the runner still has: -# * the image, tagged lean-bench:latest and lean-bench:sha- -# * the Docker layer cache, so the next build reuses Mathlib instead of -# re-downloading it (nothing here ever calls `docker system prune`) -# * a long-lived container `lean-bench`, idle and ready for `docker exec` -# * named volumes `lean-bench-data` (the item database) and `lean-bench-books` -# -# so you can submit a book straight afterwards: -# docker exec -e DASHSCOPE_API_KEY=sk-... lean-bench \ -# lean-bench ingest /books/your-book.pdf --pages 30-60 -# -# Pushing to the registry is optional and never fails the build: the built-in -# Actions token is not accepted by Gitea's container registry, so add a personal -# access token with write:package as the REGISTRY_TOKEN secret to enable it. - -on: - push: - branches: [main] - tags: ["v*"] - workflow_dispatch: - inputs: - mathlib_rev: - description: "Mathlib revision (tag, branch, commit, or 'auto')" - required: false - default: "auto" - push_image: - description: "Push to the registry if a token is configured" - required: false - default: "true" - refresh_service: - description: "Recreate the long-lived lean-bench container even if one is running" - required: false - default: "false" - no_cache: - description: "Build without the layer cache (slow: refetches Mathlib)" - required: false - default: "false" - skip_size_check: - description: "Build even if the host looks too small (RAM or disk)" - required: false - default: "false" - -env: - REGISTRY: gitea.entroia.com - IMAGE_NAME: lean-bench - LOCAL_IMAGE: lean-bench - SERVICE_CONTAINER: lean-bench - DATA_VOLUME: lean-bench-data - BOOKS_VOLUME: lean-bench-books - -jobs: - image: - runs-on: ubuntu-latest - timeout-minutes: 150 - steps: - - uses: actions/checkout@v4 - - - name: Check the runner can build images - run: | - set -eu - if ! command -v docker >/dev/null; then - echo "::error::No docker CLI on this runner. Give the act_runner the host" - echo "::error::docker socket (-v /var/run/docker.sock:/var/run/docker.sock)" - echo "::error::or run it with the docker-in-docker image." - exit 1 - fi - docker version --format 'client {{.Client.Version}} / server {{.Server.Version}}' - # Worth recording: a Lean build wants several GB of RAM, and a silent stall - # in `lake` is almost always memory or disk rather than a real hang. - echo "docker host: $(docker info --format '{{.NCPU}} cpu, {{.MemTotal}} bytes ram, storage {{.Driver}}')" - echo "disk on the docker host:" - docker system df || true - df -h / 2>/dev/null || true - - # Mathlib is the constraint, not the pipeline. Finding that out 40 minutes - # into a build, from silence, is how an afternoon disappears -- so check first. - - name: Check the host is big enough for Mathlib - run: | - set -eu - bytes="$(docker info --format '{{.MemTotal}}')" - gib=$(( bytes / 1073741824 )) - need=4 - echo "docker host memory: ${gib} GiB" - if [ "$gib" -lt "$need" ]; then - echo "::error::This host has ${gib} GiB of RAM. Loading Mathlib's environment" - echo "::error::needs roughly 4-8 GB, and below that Lean does not fail -- it" - echo "::error::thrashes silently until something kills it. Give the runner host" - echo "::error::at least ${need} GB (8 GB is comfortable), or build elsewhere." - echo "::error::Verification needs this memory at RUN time too, not just to build." - if [ '${{ inputs.skip_size_check }}' = 'true' ]; then - echo "::warning::skip_size_check is set; building anyway." - else - exit 1 - fi - elif [ "$gib" -lt 8 ]; then - echo "::warning::${gib} GiB will work but is tight for Mathlib; 8 GB is comfortable." - fi - - # Disk, measured where images actually land. Exporting the image unpacks it - # a second time next to the copy the build already wrote, so the peak is - # roughly twice the image size on top of whatever the layer cache holds. - # An 18 GB margin was not enough: the export died on the last Mathlib olean. - root="$(docker info --format '{{.DockerRootDir}}')" - echo "docker root dir: ${root}" - free_kb="$(docker run --rm -v "${root}":/probe:ro busybox df -P /probe 2>/dev/null \ - | awk 'NR==2{print $4}')" || true - [ -n "${free_kb:-}" ] || free_kb="$(df -P / | awk 'NR==2{print $4}')" - free_gb=$(( free_kb / 1048576 )) - echo "free where images land: ${free_gb} GiB" - if [ "$free_gb" -lt 25 ]; then - echo "::error::Only ${free_gb} GiB free under ${root}. The Lean + Mathlib image" - echo "::error::needs ~25 GB of headroom: it is unpacked again at export time," - echo "::error::and a build that gets all the way there and then dies on ENOSPC" - echo "::error::has wasted the full 25 minutes. Free space, grow the disk, or move" - echo "::error::Docker's storage to a bigger one." - if [ '${{ inputs.skip_size_check }}' = 'true' ]; then - echo "::warning::skip_size_check is set; building anyway." - else - exit 1 - fi - elif [ "$free_gb" -lt 40 ]; then - echo "::warning::${free_gb} GiB free is workable but leaves little room for a second image version." - fi - - - name: Work out the tags - id: meta - run: | - set -eu - owner="$(echo "${{ github.repository_owner }}" | tr '[:upper:]' '[:lower:]')" - remote="${REGISTRY}/${owner}/${IMAGE_NAME}" - ref="${GITHUB_REF_NAME:-main}" - sha="$(echo "${GITHUB_SHA:-unknown}" | cut -c1-12)" - case "${GITHUB_REF:-}" in - refs/tags/*) version="${ref}" ;; - *) version="${ref//\//-}" ;; - esac - # Local tags are what stays on the runner; remote tags are for the registry. - local_tags="${LOCAL_IMAGE}:${version} ${LOCAL_IMAGE}:sha-${sha}" - remote_tags="${remote}:${version} ${remote}:sha-${sha}" - if [ "${ref}" = "main" ]; then - local_tags="${local_tags} ${LOCAL_IMAGE}:latest" - remote_tags="${remote_tags} ${remote}:latest" - fi - { - echo "remote=${remote}" - echo "primary=${LOCAL_IMAGE}:${version}" - echo "local_tags=${local_tags}" - echo "remote_tags=${remote_tags}" - } >> "$GITHUB_OUTPUT" - echo "local: ${local_tags}" - echo "remote: ${remote_tags}" - - - name: Build - run: | - set -eu - args="" - for tag in ${{ steps.meta.outputs.local_tags }} ${{ steps.meta.outputs.remote_tags }}; do - args="$args -t $tag" - done - # Reuse the previous build's layers explicitly as well as implicitly, so a - # rebuild does not refetch Mathlib. - cache="" - if [ '${{ inputs.no_cache }}' = 'true' ]; then - cache="--no-cache" - elif docker image inspect "${LOCAL_IMAGE}:latest" >/dev/null 2>&1; then - cache="--cache-from ${LOCAL_IMAGE}:latest" - fi - echo "building with: $cache" - # --progress=plain: the fancy renderer collapses long-running steps into a - # single rewritten line, which makes a stalled build indistinguishable from a - # quiet one in the Actions log. - docker build \ - --progress=plain \ - -f docker/Dockerfile \ - --build-arg "MATHLIB_REV=${{ inputs.mathlib_rev || 'auto' }}" \ - --build-arg BUILDKIT_INLINE_CACHE=1 \ - $cache $args . - - - name: Check the image actually works - run: | - set -eu - image='${{ steps.meta.outputs.primary }}' - docker run --rm "$image" doctor --skip-llm - docker run --rm --entrypoint bash "$image" -lc \ - 'cd "$LEANBENCH_LEAN_PROJECT" && printf "import Mathlib\ntheorem ci_smoke (n : Nat) : n + 0 = n := by simp\n" > /tmp/CI.lean && lake env lean /tmp/CI.lean && echo "lean + mathlib ok"' - # Whole pipeline, scripted LLM, real compiler. Piped in over stdin so the - # job container needs no bind mount into the host daemon. - docker run --rm -i --entrypoint python3 "$image" - < docker/smoke.py - - - name: Log in to the registry - id: login - if: ${{ github.event_name != 'workflow_dispatch' || inputs.push_image == 'true' }} - continue-on-error: true - run: | - set -eu - token='${{ secrets.REGISTRY_TOKEN }}' - [ -n "$token" ] || token='${{ secrets.GITEA_TOKEN }}' - [ -n "$token" ] || token='${{ secrets.GITHUB_TOKEN }}' - user='${{ vars.REGISTRY_USER }}' - [ -n "$user" ] || user='${{ github.actor }}' - if [ -z "$token" ]; then - echo "::warning::No registry token; keeping the image on the runner only." - exit 1 - fi - echo "$token" | docker login "${REGISTRY}" -u "$user" --password-stdin - - - name: Push - id: push - if: ${{ steps.login.outcome == 'success' }} - continue-on-error: true - run: | - set -eu - for tag in ${{ steps.meta.outputs.remote_tags }}; do - echo "pushing $tag" - docker push "$tag" - done - - - name: Leave the environment ready for use - run: | - set -eu - image='${{ steps.meta.outputs.primary }}' - docker volume create "${DATA_VOLUME}" >/dev/null - docker volume create "${BOOKS_VOLUME}" >/dev/null - - running="" - if docker ps --format '{{.Names}}' | grep -qx "${SERVICE_CONTAINER}"; then - running="yes" - fi - if [ -n "$running" ] && [ '${{ inputs.refresh_service }}' != 'true' ]; then - echo "${SERVICE_CONTAINER} is already running; leaving it alone so nothing" - echo "in flight is interrupted. Re-run with refresh_service=true to move it" - echo "onto the image just built." - # ...but say so loudly, because "left alone" and "up to date" look - # identical from outside and the gap only widens. This cost a whole - # debugging session once: the container had been up for six hours on - # the previous build, so the feature added in between simply was not - # there, and every symptom pointed at the new code instead. - built=$(docker image inspect "$image" --format '{{.Id}}') - current=$(docker inspect "${SERVICE_CONTAINER}" --format '{{.Image}}') - if [ "$built" != "$current" ]; then - echo "::warning::${SERVICE_CONTAINER} is running ${current#sha256:} but the" - echo "::warning::image just built is ${built#sha256:} -- it is STALE." - echo "STALE=yes" >> "$GITHUB_ENV" - echo "STALE_RUNNING=${current#sha256:}" >> "$GITHUB_ENV" - echo "STALE_BUILT=${built#sha256:}" >> "$GITHUB_ENV" - else - echo "${SERVICE_CONTAINER} is already on the image just built." - fi - else - docker rm -f "${SERVICE_CONTAINER}" >/dev/null 2>&1 || true - docker run -d \ - --name "${SERVICE_CONTAINER}" \ - --restart unless-stopped \ - -v "${DATA_VOLUME}:/data" \ - -v "${BOOKS_VOLUME}:/books" \ - -e DASHSCOPE_API_KEY \ - --entrypoint sleep \ - "$image" infinity - echo "${SERVICE_CONTAINER} is up on $image" - fi - docker exec "${SERVICE_CONTAINER}" lean-bench doctor --skip-llm || true - - echo "images kept on this runner:" - docker images "${LOCAL_IMAGE}" --format ' {{.Repository}}:{{.Tag}} {{.Size}} {{.CreatedSince}}' - env: - DASHSCOPE_API_KEY: ${{ secrets.DASHSCOPE_API_KEY }} - - - name: Summary - if: always() - run: | - { - echo "### lean-bench image" - echo "" - if [ "${STALE:-}" = "yes" ]; then - echo "> **The \`${SERVICE_CONTAINER}\` container is stale.** It is still" - echo "> running \`${STALE_RUNNING:0:12}\`; this build produced" - echo "> \`${STALE_BUILT:0:12}\`. It was left alone on purpose so that" - echo "> nothing in flight was interrupted, so anything you exec into it" - echo "> runs the OLD code. Re-run this workflow with" - echo "> \`refresh_service=true\` once the runner is idle, or:" - echo "> \`\`\`" - echo "> docker rm -f ${SERVICE_CONTAINER}" - echo "> \`\`\`" - echo "> and re-run to have it recreated." - echo "" - fi - echo "Kept on the runner (not cleaned up):" - for tag in ${{ steps.meta.outputs.local_tags }}; do echo "- \`$tag\`"; done - echo "" - if [ '${{ steps.push.outcome }}' = 'success' ]; then - echo "Pushed to the registry:" - for tag in ${{ steps.meta.outputs.remote_tags }}; do echo "- \`$tag\`"; done - else - echo "**Not pushed.** Gitea's container registry rejects the built-in" - echo "Actions token. Create a personal access token with \`write:package\`" - echo "and add it as the \`REGISTRY_TOKEN\` secret (and \`REGISTRY_USER\`" - echo "as a variable if it is not \`${{ github.actor }}\`). The image is on" - echo "the runner either way." - fi - echo "" - echo "Submit a book to the container that is already running:" - echo '```' - echo "docker cp your-book.pdf lean-bench:/books/" - echo "docker exec -e DASHSCOPE_API_KEY=sk-... lean-bench \\" - echo " lean-bench ingest /books/your-book.pdf --pages 30-60" - echo "docker exec lean-bench lean-bench stats" - echo '```' - } >> "$GITHUB_STEP_SUMMARY" diff --git a/.gitea/workflows/ingest.yml b/.gitea/workflows/ingest.yml deleted file mode 100644 index fcb640d..0000000 --- a/.gitea/workflows/ingest.yml +++ /dev/null @@ -1,129 +0,0 @@ -name: ingest - -# Submit a book and run the whole pipeline, inside the long-lived `lean-bench` -# container the docker workflow leaves running on this runner. The book is copied -# into the `lean-bench-books` volume and the items land in `lean-bench-data`, so -# everything survives the job and is there for the next one -- `--pages` of the -# same book can be redone later without re-ingesting the rest. -# -# The source can be a path inside the repository or a URL the runner can reach. -# Set the DASHSCOPE_API_KEY secret (or whichever key your provider uses) first. - -on: - workflow_dispatch: - inputs: - source: - description: "Path in the repo, or a URL, of the book to ingest" - required: true - pages: - description: "Page range, e.g. 30-60 (blank = the whole book)" - required: false - default: "" - title: - description: "Human title for this source" - required: false - default: "" - verify: - description: "Run Lean verification (slow, but the point)" - required: false - default: "true" - image: - description: "Image to use if the lean-bench container is not running" - required: false - default: "lean-bench:latest" - -env: - SERVICE_CONTAINER: lean-bench - DATA_VOLUME: lean-bench-data - BOOKS_VOLUME: lean-bench-books - -jobs: - ingest: - runs-on: ubuntu-latest - timeout-minutes: 720 - steps: - - uses: actions/checkout@v4 - - - name: Fetch the source - id: source - run: | - set -eu - mkdir -p books out - src='${{ inputs.source }}' - case "$src" in - http://*|https://*) - name="$(basename "${src%%\?*}")" - curl -fsSL --retry 3 -o "books/$name" "$src" - ;; - *) - [ -f "$src" ] || { echo "::error::$src is not in the repository"; exit 1; } - name="$(basename "$src")" - cp "$src" "books/$name" - ;; - esac - ls -l "books/$name" - echo "name=$name" >> "$GITHUB_OUTPUT" - - - name: Make sure the lean-bench container is up - run: | - set -eu - docker volume create "${DATA_VOLUME}" >/dev/null - docker volume create "${BOOKS_VOLUME}" >/dev/null - if ! docker ps --format '{{.Names}}' | grep -qx "${SERVICE_CONTAINER}"; then - image='${{ inputs.image }}' - if ! docker image inspect "$image" >/dev/null 2>&1; then - echo "::error::No $image on this runner. Run the docker workflow first." - exit 1 - fi - docker rm -f "${SERVICE_CONTAINER}" >/dev/null 2>&1 || true - docker run -d --name "${SERVICE_CONTAINER}" --restart unless-stopped \ - -v "${DATA_VOLUME}:/data" -v "${BOOKS_VOLUME}:/books" \ - --entrypoint sleep "$image" infinity - fi - docker exec "${SERVICE_CONTAINER}" lean-bench doctor --skip-llm - - - name: Ingest - env: - DASHSCOPE_API_KEY: ${{ secrets.DASHSCOPE_API_KEY }} - LEANBENCH_LLM_MODEL: ${{ vars.LEANBENCH_LLM_MODEL }} - LEANBENCH_LLM_BASE_URL: ${{ vars.LEANBENCH_LLM_BASE_URL }} - run: | - set -eu - [ -n "${DASHSCOPE_API_KEY:-}" ] || { echo "::error::Set the DASHSCOPE_API_KEY secret"; exit 1; } - name='${{ steps.source.outputs.name }}' - docker cp "books/$name" "${SERVICE_CONTAINER}:/books/$name" - - set -- ingest "/books/$name" \ - --export "/data/${name%.*}.items.jsonl" \ - --detections "/data/${name%.*}.detections.jsonl" - # `cond && set -- ...` would abort the step under `set -e` whenever the - # condition is false, so these are spelled out. - if [ -n '${{ inputs.pages }}' ]; then set -- "$@" --pages '${{ inputs.pages }}'; fi - if [ -n '${{ inputs.title }}' ]; then set -- "$@" --title '${{ inputs.title }}'; fi - if [ '${{ inputs.verify }}' != 'true' ]; then set -- "$@" --no-verify; fi - - docker exec \ - -e DASHSCOPE_API_KEY \ - -e LEANBENCH_LLM_MODEL \ - -e LEANBENCH_LLM_BASE_URL \ - "${SERVICE_CONTAINER}" lean-bench "$@" - docker exec "${SERVICE_CONTAINER}" lean-bench stats - - - name: Collect a copy of the results - if: always() - run: | - set -eu - # The originals stay in the lean-bench-data volume; these are just copies - # for the artifact. - docker exec "${SERVICE_CONTAINER}" sh -c 'ls -1 /data' || true - for f in $(docker exec "${SERVICE_CONTAINER}" sh -c 'ls -1 /data' 2>/dev/null || true); do - docker cp "${SERVICE_CONTAINER}:/data/$f" "out/$f" || true - done - ls -l out || true - - - uses: actions/upload-artifact@v3 - if: always() - with: - name: leanbench-${{ steps.source.outputs.name }} - path: out/ - retention-days: 30