{"data":{"kind":"file","path":"README.md","version_id":"lygd90bh4154po02g8f5gs5t","entry":{"name":"README.md","path":"README.md","is_directory":false,"size":3953,"modified_at":"2026-06-01T19:55:35.064000","content_hash":"5dbc4c25c425413dba77752b574558d4808bc31dc09566dfb9d73375b44a150b"},"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\n| Preset | Dataset |\n|--------|---------|\n| `deepseek-prover-v1` | DeepSeek-Prover-V1 |\n| `minif2f` | MiniF2F |\n| `goedel-pset` | Goedel PSet |\n\n### Changelog\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":3953},"status":null}