[codex] Simplify getting started examples docs

examples/getting_started/01_minif2f_local_llamacpp/README.md

@@ -1,15 +1,14 @@
 # MiniF2F With Local llama.cpp
 
-Run three MiniF2F Lean proof tasks with a managed local llama.cpp server and the
-E2B Lean sandbox.
+Run three MiniF2F Lean proof tasks with llama.cpp and the E2B Lean sandbox.
 
 ## Prerequisites
 
 - Python 3.13 and `uv`
-- The Ergon stack installed and configured
-- `E2B_API_KEY` configured in Ergon's `.env` file or process environment
+- Ergon installed from this repository
+- `E2B_API_KEY` in `.env` or your shell environment
 - The MiniF2F Lean E2B template available to your E2B account
-- `llama-server` installed and available on `PATH`
+- `llama-server` on `PATH`
 - A local GGUF model path or Hugging Face GGUF model reference
 
 On macOS, install the llama.cpp server binary with:
@@ -21,30 +20,18 @@ brew install llama.cpp
 If `llama-server` is installed somewhere else, pass its path with
 `--llama-server-bin`.
 
-## Run
+## Recommended Run
 
 From the repository root, pass a Hugging Face GGUF reference in
-`<repo-id>:<filename.gguf>` form. The example downloads the file into the model
-cache, starts `llama-server`, waits for `/v1/models`, launches the MiniF2F run,
-and cleans up the model server when the run command exits.
+`<repo-id>:<filename.gguf>` form. The command downloads the model if needed,
+starts `llama-server`, launches the run, and cleans up the server when it exits.
 
 ```bash
 uv run ergon examples run minif2f-local-llamacpp \
   --base-model unsloth/DeepSeek-Prover-V2-7B-GGUF:Q4_K_M.gguf \
   --limit 3
 ```
 
-Downloaded models use `~/.cache/ergon/examples/models` by default. Use
-`--model-cache-dir` or `ERGON_EXAMPLE_MODEL_CACHE_DIR` when you want a temporary
-or shared cache location.
-
-```bash
-uv run ergon examples run minif2f-local-llamacpp \
-  --base-model unsloth/DeepSeek-Prover-V2-7B-GGUF:Q4_K_M.gguf \
-  --model-cache-dir /tmp/ergon-models \
-  --limit 3
-```
-
 A local GGUF path also works:
 
 ```bash
@@ -53,21 +40,16 @@ uv run ergon examples run minif2f-local-llamacpp \
   --limit 3
 ```
 
-Use `--llama-server-bin` if the command is not on `PATH`, and
-`--keep-llama-server` if you want to inspect or reuse the model server after the
-example command exits.
+Useful options:
 
-```bash
-uv run ergon examples run minif2f-local-llamacpp \
-  --base-model /path/to/model.gguf \
-  --llama-server-bin /path/to/llama-server \
-  --keep-llama-server
-```
+- `--model-cache-dir /tmp/ergon-models` changes the download cache.
+- `--llama-server-bin /path/to/llama-server` uses a non-`PATH` server binary.
+- `--keep-llama-server` leaves the managed server running after the command.
 
 ## Already Running Server
 
 If you already have a llama.cpp OpenAI-compatible server listening locally, use
-the advanced path:
+`--base-url` instead:
 
 ```bash
 llama-server --model /path/to/model.gguf --host 127.0.0.1 --port 8080
@@ -77,14 +59,16 @@ uv run ergon examples run minif2f-local-llamacpp \
   --limit 3
 ```
 
-The plain Python script remains the source of benchmark behavior and is useful
-when you want to read or edit the example directly:
+## Read Or Edit The Script
+
+The CLI is a wrapper around the Python script. Run it directly when you want to
+read or modify the benchmark authoring path:
 
 ```bash
 uv run --project examples python examples/getting_started/01_minif2f_local_llamacpp/run.py
 ```
 
-The script defaults to:
+Defaults:
 
 - `ERGON_LLAMA_CPP_BASE_URL=http://localhost:8080`
 - `ERGON_LLAMA_CPP_MODEL` unset, so Ergon discovers the served model from `/v1/models`
@@ -109,28 +93,18 @@ you intentionally want to pass a full Ergon model target such as
 
 The script:
 
-1. Resolves `--base-model` from either a local path or Hugging Face GGUF ref.
-2. Starts `llama-server` for managed runs, then discovers the served model from `/v1/models`.
-3. Checks Ergon settings for `E2B_API_KEY` and verifies the llama.cpp endpoint.
-4. Builds `MiniF2FBenchmark(limit=3, worker_factory=make_worker)`.
-5. Binds `make_minif2f_worker(model="llamacpp:<base-url>", max_iterations=12)`.
-6. Persists the benchmark definition with `persist_benchmark`.
-7. Launches a run with `launch_run`.
-8. Prints the definition id, run id, model target, and observation commands.
+1. Resolves the model path or server URL.
+2. Checks `E2B_API_KEY` and the llama.cpp endpoint.
+3. Builds and persists a `MiniF2FBenchmark`.
+4. Launches a run.
+5. Prints the definition id, run id, model target, and observation commands.
 
 MiniF2F is a real theorem-proving benchmark. Local model quality, quantization,
 and context length strongly affect proof success. A terminal run with failed
 proofs is still an honest first-run outcome: inspect the attempts, proof files,
 tool calls, and evaluator feedback before changing models or iteration limits.
 
-## Manual Readiness Notes
-
-The automated tests for this example do not require a real llama.cpp server or
-E2B account. They cover argument parsing, preflight failures, model-target
-construction, and launch wiring with monkeypatched Ergon APIs.
-
-When running against real services, these are expected setup or integration
-failures rather than successful benchmark launches:
+## Common Setup Problems
 
 - Missing `E2B_API_KEY`: add it to Ergon's `.env` file or process environment.
 - Hugging Face download failure: check the `--base-model` repo/file ref, network
@@ -143,6 +117,6 @@ failures rather than successful benchmark launches:
   use OpenAI-compatible tool calls, or inspect the run artifacts for the failed
   attempts.
 
-Do not treat theorem failures as setup failures. A run that launches all three
-tasks and records failed proof attempts is still useful evidence about the local
-model, context length, and iteration budget.
+Do not treat theorem failures as setup failures. A run that launches all tasks
+and records failed proof attempts is still useful evidence about the model,
+context length, and iteration budget.

examples/getting_started/README.md

@@ -1,14 +1,21 @@
 # Getting Started Examples
 
-These examples are the public first steps for running Ergon locally.
+Small examples for running Ergon from a local checkout. Start here when you
+want to launch a real run before writing your own benchmark script.
 
 ## Available Examples
 
 | Example | What it runs |
 | --- | --- |
-| [`01_minif2f_local_llamacpp`](01_minif2f_local_llamacpp/) | Three MiniF2F Lean proof tasks with a local llama.cpp OpenAI-compatible server and E2B Lean sandbox |
+| [`01_minif2f_local_llamacpp`](01_minif2f_local_llamacpp/) | Three MiniF2F Lean proof tasks with llama.cpp and an E2B Lean sandbox |
 
-The examples stay as plain Python scripts, and `uv run ergon examples ...`
-provides a thin wrapper for listing, checking, and launching them. The script is
-still the source of behavior, so you can read it directly to see the benchmark
-authoring path.
+Use the CLI for the normal path:
+
+```bash
+uv run ergon examples list
+uv run ergon examples info minif2f-local-llamacpp
+uv run ergon examples check minif2f-local-llamacpp --base-url http://localhost:8080
+```
+
+The examples are still plain Python scripts. Read the script when you want to
+see the object-bound benchmark authoring path directly.