Surfaced by the Wave-1 MRR baseline (PR #148, docs/bench/2026-05-30-chapel-mrr-baseline.md).
Problem
`idris2 --check /tmp/echidna-chapel/goal_Idris2_.idr` fails with `Module Prelude not found` because Idris2 looks for its prelude under `IDRIS2_DATA_DIR` (or the install prefix) and requires the source file to be inside the configured source directory. The current `tryProver` in `src/chapel/parallel_proof_search.chpl` spawns each prover from the parent's CWD with no per-prover env propagation, so Idris2 is non-functional in the metalayer regardless of what fixture content we feed it.
Acceptance
- `tryProver` supports an optional per-prover `cwd` and `env` hook (or equivalent ProverInfo extension).
- The registry entry for Idris2 sets `cwd = /tmp/echidna-chapel` and propagates `IDRIS2_PREFIX` / `IDRIS2_DATA_DIR` from the parent.
- `just bench-chapel-mrr` shows `idris2_trivial → success` for at least one of the three strategies.
Surfaced by the Wave-1 MRR baseline (PR #148, docs/bench/2026-05-30-chapel-mrr-baseline.md).
Problem
`idris2 --check /tmp/echidna-chapel/goal_Idris2_.idr` fails with `Module Prelude not found` because Idris2 looks for its prelude under `IDRIS2_DATA_DIR` (or the install prefix) and requires the source file to be inside the configured source directory. The current `tryProver` in `src/chapel/parallel_proof_search.chpl` spawns each prover from the parent's CWD with no per-prover env propagation, so Idris2 is non-functional in the metalayer regardless of what fixture content we feed it.
Acceptance