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

Each preset resolves a version-matched Mathlib sandbox image (mirroring lean-code's preset map), since each dataset's statements were formalized against a specific Lean/Mathlib version. Pass sandbox_docker_image to override. A preset without a mapped image raises unless sandbox_docker_image is passed explicitly — no silent fallback to a possibly version-mismatched default.

Changelog

v0.3.16

• Bump verifiers to >=0.1.15.dev178, lifting the <0.1.15.dev150 cap: the cap excluded the new opencode_harness API, which this version adapts to. The [packages] extra (added in v0.3.15) is dropped: it is unresolvable on dev178 (requires harnesses>=0.1.2 / tasksets>=0.1.5, neither published on PyPI yet) and unused here — this env runs on the composable stack in verifiers core, not verifiers.v1. Drop the opencode_release_repo / opencode_release_version / opencode_release_sha256 args from load_environment: opencode_harness no longer accepts them — the release (PrimeIntellect-ai/opencode v1.1.63-rl2, matching our previous pin) is now a module-level default in verifiers. dev178 also carries the last-match EXIT_CODE:N parsing in upstream LeanTaskSet (PR #1480), closing the reward-bypass trade-off documented in v0.3.14.
• Move the proof file inside the agent workdir (new proof_file_path arg, default /workspace/mathlib4/proof.lean). The upstream LeanTaskSet default /tmp/proof.lean is outside the OpenCode workdir, so the agent's very first cat /tmp/proof.lean triggered an external_directory permission request that OpenCode auto-rejects in non-interactive runs — every rollout died after one turn with reward 0 (visible in agent_logs: ! permission requested: external_directory (/tmp/*); auto-rejecting). The hardcoded path in LEAN_SYSTEM_PROMPT is rewritten to match.
• Drop the broken opencode-lean:rl2 default image: it has no mathlib4 project at /workspace/mathlib4 and no lake on PATH, so even surviving rollouts could never compile a proof (lake: command not found, unknown module prefix 'Mathlib'). sandbox_docker_image now defaults to None and resolves a version-matched team-clyvldofb0000gg1kx39rgzjq/lean-tactic image per preset (mirroring lean-code's preset map — see the Dataset Presets table); a preset without a mapped image raises rather than silently falling back to a version-mismatched default. Trade-off: the lean-tactic images don't bake the opencode binary, so cold sandboxes download it via the harness install script at setup (~few seconds; verified working). With these fixes a deepseek-v4-flash rollout solves thm_0 end-to-end (reward 1.0).

v0.3.15

• Bound verifiers to >=0.1.15.dev17,<0.1.15.dev150.

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