opencode-lean

OpenCode Lean 4 theorem proving environment via ComposableEnv.

Overview

• Environment ID: opencode-lean
• Tags: lean, theorem-proving, multi-turn, sandbox

Quickstart

uv run vf-eval opencode-lean -n1 -r1 -d -v

Architecture

Uses ComposableEnv with LeanTaskSet + opencode_harness:

• Agent gets bash and edit tools
• Proof file at /tmp/proof.lean with sorry placeholder
• System prompt instructs compile-iterate workflow
• Scoring by LeanRubric (checks state["lean_compiled"])

Dataset Presets

Changelog

v0.3.14

• Pin verifiers>=0.1.14 (stable) and drop the [tool.uv.sources] git rev override. The previous >=0.1.15.dev11 pin was a pre-release marker; the hub installer (prime env install) doesn't enable pre-releases by default, so any consumer pinning to a .devN verifiers couldn't resolve dependencies. Stable v0.1.14 has the composable env stack (ComposableEnv, LeanTaskSet, opencode harness) we need. Trade-off: opencode-lean now uses upstream LeanTaskSet's reward path, which still has the first-match EXIT_CODE:N bypass (fix landed on verifiers main in PR #1480 but isn't in any stable release yet).

v0.3.11

• Align signature with the other opencode-* envs (sandbox_cpu_cores, sandbox_memory_gb, sandbox_disk_size_gb, sandbox_labels; new sandbox_client_max_workers; drop **kwargs catch-all; gate system_prompt injection so a caller can pass None to fall back to opencode's default).

v0.3.10

• Bump verifiers to >=0.1.15.dev2 for the OpenCode harness config that disables title-generation calls while preserving the small_model pin.

v0.3.9

• Harden sandbox image bootstrap against transient Ubuntu archive mirror sync flakes by adding apt acquire retries.

v0.3.8

• Fix sandbox_docker_image prefix. The cme8364tg000o1139v84cu0cv/... prefix carried over from v0.3.7 is a user-scoped ID that the cluster cannot pull from, causing ImagePullBackOff on every sandbox creation. Swap to the team-scoped team-clyvldofb0000gg1kx39rgzjq/opencode-lean:rl2.

v0.3.7

• Pin sandbox_docker_image default to team-clyvldofb0000gg1kx39rgzjq/opencode-lean:rl2. The new image bakes the opencode v1.1.63-rl2 binary into the sandbox so cold sandboxes no longer need to install it at rollout time. README updated to document the change.

v0.3.5

• Add sandbox_docker_image argument (default team-clyvldofb0000gg1kx39rgzjq/opencode-lean:rl2), threaded through to LeanTaskSet (#305). Companion to #303 which handled math/cp/science.

v0.3.4

• Bump opencode fork release from 1.1.63-rl1 to 1.1.63-rl2 (PrimeIntellect-ai/opencode#3), explicitly pinned via the opencode_release_version override. Fork release surfaces session-level retry exhaustion as a non-zero exit with a structured stderr dump, so hosted RL rollouts that previously returned silent empty trajectories now produce real AgentError entries. Companion default bump in verifiers: PrimeIntellect-ai/verifiers#1184.

v0.3.3

• Bump verifiers to stable >=0.1.12.

v0.3.2

• Unpin prime-sandboxes git source override; use PyPI release >=0.2.19.
• Bump verifiers to >=0.1.13.dev1.

v0.2.1

• Migrate OpenCode fork from rasdani/opencode to PrimeIntellect-ai/opencode. Bump release from 1.1.63-swe8 to 1.1.63-rl1 via shared opencode_harness defaults (trimmed system prompt for RL training efficiency).

v0.2.0

• Rewrite to composable architecture. Uses ComposableEnv + LeanTaskSet + opencode_harness. Replaces lean_code environment.

v0.1.0

• Initial release