{"data":{"kind":"file","path":"README.md","version_id":"k5u7twzklld29w2mrhsgzgvt","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":7086,"modified_at":"2026-06-12T21:17:47.773000","content_hash":"8716644e26878e2f54af4eb4d18d8cc08be91662b85fa1fe85147ae29aa49c07"},"entries":[],"content":"# opencode-lean\n\nOpenCode Lean 4 theorem proving environment via ComposableEnv.\n\n### Overview\n- **Environment ID**: `opencode-lean`\n- **Tags**: lean, theorem-proving, multi-turn, sandbox\n\n### Quickstart\n\n```bash\nuv run vf-eval opencode-lean -n1 -r1 -d -v\n```\n\n### Architecture\n\nUses `ComposableEnv` with `LeanTaskSet` + `opencode_harness`:\n- Agent gets `bash` and `edit` tools\n- Proof file at `/tmp/proof.lean` with `sorry` placeholder\n- System prompt instructs compile-iterate workflow\n- Scoring by `LeanRubric` (checks `state[\"lean_compiled\"]`)\n\n### Dataset Presets\n\nEach 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.\n\n| Preset | Dataset | Image |\n|--------|---------|-------|\n| `deepseek-prover-v1` | DeepSeek-Prover-V1 | `lean-tactic:mathlib-v4.7.0-rc2-v1` |\n| `goedel-pset` | Goedel PSet | `lean-tactic:mathlib-v4.9.0-v1` |\n| `deepseek-proverbench` | DeepSeek-ProverBench | `lean-tactic:mathlib-v4.9.0-v1` |\n| `numina-lean` | NuminaMath-LEAN | `lean-tactic:mathlib-v4.15.0-v1` |\n| `minif2f` | MiniF2F | `lean-tactic:mathlib-v4.24.0-v1` |\n| `kimina` | Kimina-Prover-Promptset | `lean-tactic:mathlib-v4.26.0-v1` |\n\n### Changelog\n\n### v0.3.16\n- 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` v`1.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](https://github.com/PrimeIntellect-ai/verifiers/pull/1480)), closing the reward-bypass trade-off documented in v0.3.14.\n- 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.\n- 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).\n\n### v0.3.15\n- Bound `verifiers` to `>=0.1.15.dev17,<0.1.15.dev150`.\n\n### v0.3.14\n- 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).\n\n### v0.3.11\n- 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).\n\n### v0.3.10\n- Bump `verifiers` to `>=0.1.15.dev2` for the OpenCode harness config that disables title-generation calls while preserving the `small_model` pin.\n\n### v0.3.9\n- Harden sandbox image bootstrap against transient Ubuntu archive mirror sync flakes by adding apt acquire retries.\n\n### v0.3.8\n- 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`.\n\n### v0.3.7\n- 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.\n\n### v0.3.5\n- Add `sandbox_docker_image` argument (default `team-clyvldofb0000gg1kx39rgzjq/opencode-lean:rl2`), threaded through to `LeanTaskSet` ([#305](https://github.com/PrimeIntellect-ai/research-environments/pull/305)). Companion to #303 which handled math/cp/science.\n\n### v0.3.4\n- Bump opencode fork release from `1.1.63-rl1` to `1.1.63-rl2` ([PrimeIntellect-ai/opencode#3](https://github.com/PrimeIntellect-ai/opencode/pull/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](https://github.com/PrimeIntellect-ai/verifiers/pull/1184).\n\n### v0.3.3\n- Bump verifiers to stable `>=0.1.12`.\n\n### v0.3.2\n- Unpin `prime-sandboxes` git source override; use PyPI release `>=0.2.19`.\n- Bump verifiers to `>=0.1.13.dev1`.\n\n### v0.2.1\n- 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).\n\n### v0.2.0\n- Rewrite to composable architecture. Uses `ComposableEnv` + `LeanTaskSet` + `opencode_harness`. Replaces `lean_code` environment.\n\n### v0.1.0\n- Initial release\n","encoding":"utf-8","truncated":false,"total_bytes":7086},"status":null}