Surfaced by the Wave-1 MRR baseline (PR #148, docs/bench/2026-05-30-chapel-mrr-baseline.md).
Problem
`tryProver` in `src/chapel/parallel_proof_search.chpl` writes temp files as `goal__.`. Agda's module-name resolution requires the source-file basename to be a valid Agda identifier, but the embedded numeric `` is parsed as a literal and Agda rejects `goal_Agda_0.agda` with `in the name 0, the part 0 is not valid because it is a literal`.
Acceptance
- Per-prover filename-generation hook (or convention that puts a letter prefix in front of the nodeId for prover-specific naming sensitivity).
- Agda fixture round-trip works through `tryProver` (success path testable in `bench_mrr`).
Adjacent
Same architectural shape as the Idris2 env-hook issue — a per-prover hook table extending ProverInfo.
Surfaced by the Wave-1 MRR baseline (PR #148, docs/bench/2026-05-30-chapel-mrr-baseline.md).
Problem
`tryProver` in `src/chapel/parallel_proof_search.chpl` writes temp files as `goal__.`. Agda's module-name resolution requires the source-file basename to be a valid Agda identifier, but the embedded numeric `` is parsed as a literal and Agda rejects `goal_Agda_0.agda` with `in the name 0, the part 0 is not valid because it is a literal`.
Acceptance
Adjacent
Same architectural shape as the Idris2 env-hook issue — a per-prover hook table extending ProverInfo.