Zayden-Jung/lean-bench
2
1
Fork 0
Code Issues 2 Pull Requests Actions Packages Projects Releases Wiki Activity

CI: run jobs on label ubuntu24.04-x64-lean4.35 and keep the built image permanently #1

New Issue
Open
opened 2026-10-21 13:23:56 +00:00 by yilin-codex-bot · 0 comments
yilin-codex-bot commented 2026-10-21 13:23:56 +00:00
Collaborator
Copy Link
Copy Source

@codex-bot please take this task.

Request

  1. Switch the CI/CD runner label. Use ubuntu24.04-x64-lean4.35 as the runs-on label for this project's Gitea Actions jobs, replacing the current gitea-cicd-server-for-CODEX label in .gitea/workflows/ (ci.yml, runner-probe.yml, and any workflows you add).

  2. Permanent image after CI/CD tests. When the CI/CD pipeline builds the Docker image, the image must be kept permanently on the runner host after the tests finish — do not prune it. Keep it tagged (e.g. lean-bench:latest and lean-bench:sha-<commit>) so it can be used directly afterwards without a rebuild, as described in the README section "The build is not a throwaway".

Context

  • Target runner host is an Ubuntu 24.04 x64 machine with the Lean 4.35 toolchain pre-installed (hence the label ubuntu24.04-x64-lean4.35).
  • Projects pin leanprover/lean4:v4.33.1; elan on the runner resolves per-project toolchains automatically.
  • Runner resource budget per README: 4 GB RAM minimum (8 GB comfortable), ~25 GB free disk for Docker image storage (40 GB comfortable).

Please update the workflows and verify with a CI run.

@codex-bot please take this task. ## Request 1. **Switch the CI/CD runner label.** Use `ubuntu24.04-x64-lean4.35` as the `runs-on` label for this project's Gitea Actions jobs, replacing the current `gitea-cicd-server-for-CODEX` label in `.gitea/workflows/` (ci.yml, runner-probe.yml, and any workflows you add). 2. **Permanent image after CI/CD tests.** When the CI/CD pipeline builds the Docker image, the image must be kept permanently on the runner host after the tests finish — do not prune it. Keep it tagged (e.g. `lean-bench:latest` and `lean-bench:sha-<commit>`) so it can be used directly afterwards without a rebuild, as described in the README section "The build is not a throwaway". ## Context - Target runner host is an Ubuntu 24.04 x64 machine with the Lean 4.35 toolchain pre-installed (hence the label `ubuntu24.04-x64-lean4.35`). - Projects pin `leanprover/lean4:v4.33.1`; elan on the runner resolves per-project toolchains automatically. - Runner resource budget per README: 4 GB RAM minimum (8 GB comfortable), ~25 GB free disk for Docker image storage (40 GB comfortable). Please update the workflows and verify with a CI run.
codex-bot was assigned by yilin-codex-bot 2026-10-21 13:23:56 +00:00
Sign in to join this conversation.
No Branch/Tag Specified
Branches Tags
Labels
No items
No Label
Milestone
No items
No Milestone
Projects
Clear projects
No project
Assignees
Clear assignees
claude-bot codex-bot yilin-codex-bot Zayden-Jung
No Assignees codex-bot
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: Zayden-Jung/lean-bench#1
Delete Branch "%!s()"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?