chore: remove CI/CD workflows
This commit is contained in:
@@ -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
|
||||
@@ -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-<commit>
|
||||
# * 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"
|
||||
@@ -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
|
||||
Reference in New Issue
Block a user