|
| 1 | +<!-- SPDX-License-Identifier: MPL-2.0 --> |
| 2 | + |
| 3 | +# 2026-05-31 — Per-prover spawn hooks: cwd + filenameOverride |
| 4 | + |
| 5 | +ADR-style record of the mechanism added to `ProverInfo` and |
| 6 | +`tryProver` (`src/chapel/parallel_proof_search.chpl`) to handle |
| 7 | +provers whose CLI invocation requires per-prover state at spawn |
| 8 | +time. Closes issues #158 (Idris2 env hook) and #159 (Agda |
| 9 | +filename hook), both surfaced by the Wave-1 MRR baseline |
| 10 | +(`docs/bench/2026-05-30-chapel-mrr-baseline.md`). |
| 11 | + |
| 12 | +## Status |
| 13 | + |
| 14 | +Accepted. Implemented in the PR that introduces this ADR. |
| 15 | + |
| 16 | +## Context |
| 17 | + |
| 18 | +The L2.2 rehabilitation arc (#133 → PR #146) shipped the Chapel |
| 19 | +metalayer with a single uniform `tryProver(info, goal, …)` |
| 20 | +contract: every prover gets a temp file named |
| 21 | +`goal_<ProverName>_<nodeId>.<fileExt>`, spawned from the parent's |
| 22 | +CWD with the parent's environment. That contract held for ~22 of |
| 23 | +the 30 registered backends (Coq, Lean, the SMT row, ATPs, etc.) |
| 24 | +but two of the 30 — Idris2 and Agda — broke at spawn time: |
| 25 | + |
| 26 | +- **Idris2** (`idris2 --check`) resolves its prelude relative to |
| 27 | + `IDRIS2_PREFIX` (or the install root) AND requires the source |
| 28 | + file to live inside the configured source directory. The |
| 29 | + Wave-1 invocation `idris2 --check /tmp/echidna-chapel/goal_Idris2_0.idr` |
| 30 | + failed with `Module Prelude not found` even when the parent |
| 31 | + shell had `IDRIS2_PREFIX` set, because the source file wasn't |
| 32 | + in the cwd Idris2 used as its source dir (the parent's cwd, |
| 33 | + not the temp dir). |
| 34 | +- **Agda** (`agda --safe`) requires the source-file basename |
| 35 | + to be a valid Agda identifier AND the module declaration |
| 36 | + inside the file to match the basename. `goal_Agda_0.agda` |
| 37 | + is rejected by the lexer (`in the name 0, the part 0 is not |
| 38 | + valid because it is a literal`); even after fixing the |
| 39 | + lexer issue, Agda then enforces module-name = file-name and |
| 40 | + rejects mismatched module declarations. |
| 41 | + |
| 42 | +The Wave-1 baseline (`docs/bench/2026-05-30-chapel-mrr-baseline.md`) |
| 43 | +explicitly tracked these as caveats 1 + 2, deferred as Wave-2 |
| 44 | +follow-up issues (`#158`/`#159`). |
| 45 | + |
| 46 | +## Decision |
| 47 | + |
| 48 | +**Two new optional fields on `ProverInfo`** with empty-string |
| 49 | +defaults that preserve the prior contract for the 28 provers |
| 50 | +that don't need per-prover spawn state: |
| 51 | + |
| 52 | +```chapel |
| 53 | +record ProverInfo { |
| 54 | + var id: int; |
| 55 | + var name: string; |
| 56 | + // … existing fields … |
| 57 | + var cwd: string; // "" = inherit parent CWD |
| 58 | + var filenameOverride: string; // "" = goal_<name>_<nodeId>.<ext> |
| 59 | +} |
| 60 | +``` |
| 61 | + |
| 62 | +A custom `proc init(…, cwd = "", filenameOverride = "")` keeps |
| 63 | +all 30 existing registry call-sites compiling unchanged |
| 64 | +(default arguments fill the new fields). A zero-arg `proc init()` |
| 65 | +is also defined so `var provers: [0..29] ProverInfo` continues |
| 66 | +to default-construct each slot — without it the custom positional |
| 67 | +init would shadow Chapel's auto-generated zero-arg init and the |
| 68 | +array declaration would fail to compile. |
| 69 | + |
| 70 | +`tryProver` consumes both fields: |
| 71 | + |
| 72 | +- **`filenameOverride`** swaps the generic |
| 73 | + `goal_<name>_<nodeId>.<fileExt>` for a literal basename (with |
| 74 | + extension) when set. The default form remains locale-id-suffixed |
| 75 | + so non-overriding provers stay collision-free across locales in |
| 76 | + multi-locale runs. |
| 77 | +- **`cwd`** is implemented as a shell wrapper around the spawn: |
| 78 | + `sh -c "cd <cwd> && exec <executable> <args>"`. This is the |
| 79 | + thread-safe equivalent of `chdir()` — process-global `chdir` |
| 80 | + would race against other parallel spawn calls inside a |
| 81 | + `coforall`, but a per-subprocess `sh -c` keeps the directory |
| 82 | + change local. The parent's full environment (including |
| 83 | + `IDRIS2_PREFIX`, `IDRIS2_DATA_DIR`) is inherited regardless, |
| 84 | + per POSIX spawn defaults. |
| 85 | + |
| 86 | +Registry entries updated: |
| 87 | + |
| 88 | +- `provers[0]` (Agda) sets `cwd = "/tmp/echidna-chapel"` and |
| 89 | + `filenameOverride = "Trivial.agda"`. The fixture |
| 90 | + `tests/chapel_fixtures/agda_trivial.agda` declares |
| 91 | + `module Trivial where` to match. |
| 92 | +- `provers[4]` (Idris2) sets `cwd = "/tmp/echidna-chapel"` and |
| 93 | + `filenameOverride = "Trivial.idr"`. The fixture |
| 94 | + `tests/chapel_fixtures/idris2_trivial.idr` already declared |
| 95 | + `module Trivial`, so its content is unchanged. |
| 96 | + |
| 97 | +The Justfile `bench-chapel-mrr` recipe gained a derived |
| 98 | +`IDRIS2_PREFIX` step: if the env var isn't set and `which idris2` |
| 99 | +resolves, the recipe sets it to `dirname(dirname(realpath(which idris2)))`. |
| 100 | +This means a user with idris2 on PATH no longer needs to remember |
| 101 | +to export the prefix manually for `just bench-chapel-mrr` to |
| 102 | +work end-to-end. |
| 103 | + |
| 104 | +## Alternatives considered |
| 105 | + |
| 106 | +1. **Per-prover env-extra list (key=value pairs)** — rejected as |
| 107 | + over-engineered. Chapel `spawn` inherits parent env by default; |
| 108 | + the only env hole was Idris2's `IDRIS2_PREFIX`, which the |
| 109 | + Justfile recipe now derives and exports parent-side. No prover |
| 110 | + in the current registry needs a per-spawn env override that |
| 111 | + isn't already in the parent. |
| 112 | +2. **Auto-extract module name from goal content** (regex |
| 113 | + `^module\s+(\w+)`) — rejected as fragile. Works for clean |
| 114 | + fixtures but breaks on goals containing comments-before-module, |
| 115 | + pragmas, or multi-module files. The explicit |
| 116 | + `filenameOverride` field keeps the registry honest about which |
| 117 | + provers have basename constraints. |
| 118 | +3. **Per-prover spawn callback (function pointer in the record)** — |
| 119 | + rejected for now: Chapel records with function fields are |
| 120 | + awkward to construct in a literal-initialiser-heavy registry, |
| 121 | + and the two-field mechanism handles every concrete need |
| 122 | + surfaced by Wave-1. Revisit if a third spawn-time wart appears. |
| 123 | +4. **`POSIX_spawn`-style explicit cwd in Chapel `spawn`** — Chapel |
| 124 | + 2.x `Subprocess.spawn` does not expose a `cwd` parameter at |
| 125 | + the time of writing (verified against the apt-shipped 2.3.0 and |
| 126 | + the source-built 2.8.0). The shell-wrapper workaround sidesteps |
| 127 | + the gap with no Chapel-version dependency. |
| 128 | + |
| 129 | +## Consequences |
| 130 | + |
| 131 | +**Positive.** |
| 132 | + |
| 133 | +- `just bench-chapel-mrr` now shows `idris2_trivial → true` and |
| 134 | + `agda_trivial → true` across all three strategies, satisfying |
| 135 | + the explicit acceptance criteria for both #158 and #159. |
| 136 | +- The hook pattern is general — future provers with similar |
| 137 | + module-name or working-directory requirements (Lean 4 already |
| 138 | + works out-of-the-box but a future fixture might trigger its |
| 139 | + `Lake` workspace check; Isabelle has session-name resolution) |
| 140 | + can be wired by adding two field values to their registry |
| 141 | + entry, no `tryProver` changes. |
| 142 | +- The Wave-1 baseline document's caveats 1 + 2 (formerly tracked |
| 143 | + as Wave-2 follow-ups) are closed, leaving only caveat 3 |
| 144 | + (sub-second wall-clock jitter, which is a measurement-method |
| 145 | + issue, not a metalayer defect). |
| 146 | + |
| 147 | +**Negative.** |
| 148 | + |
| 149 | +- Shell-wrapping every `cwd`-using prover costs one `fork+exec` |
| 150 | + for the `sh` itself per invocation. For 0.1-second prover runs |
| 151 | + this is ~5% overhead; for the 10-30 s real-corpus benchmark |
| 152 | + target (#161), it's negligible. If this becomes a hot path, |
| 153 | + switching to a direct-spawn cwd implementation (when Chapel |
| 154 | + exposes it) would remove the overhead. |
| 155 | +- `filenameOverride` couples the registry entry to fixture |
| 156 | + content (the fixture's `module X where` declaration must match |
| 157 | + the override). This is acceptable because the fixture corpus |
| 158 | + is small and version-controlled together with the registry; |
| 159 | + a real-corpus runner would need a different convention (or |
| 160 | + the auto-extract approach from "Alternatives" above). |
| 161 | + |
| 162 | +**Net.** Two scoped one-line additions to `ProverInfo` close |
| 163 | +both acceptance-criterion-driven Wave-3 issues with no churn |
| 164 | +to the 28 unaffected provers; the shell-wrapper approach buys |
| 165 | +portability across Chapel 2.x runtimes; the Justfile derivation |
| 166 | +of `IDRIS2_PREFIX` removes the last user-side env-export |
| 167 | +ceremony. |
| 168 | + |
| 169 | +## Toolchain version pinning |
| 170 | + |
| 171 | +- `chpl 2.3.0` (CI) and `chpl 2.8.0` (local). The custom |
| 172 | + `proc init` syntax + `init this` invariant used here is |
| 173 | + stable across both. |
| 174 | +- `idris2 0.8.0` (local). `IDRIS2_PREFIX`-based prelude |
| 175 | + resolution is the documented mechanism; the source-directory |
| 176 | + check is `idris2 --check`-specific (a `package`-driven build |
| 177 | + doesn't have the same constraint). |
| 178 | +- `agda 2.6.3`. The module-name = filename rule is permanent |
| 179 | + Agda design (`Issue #1062` upstream). |
| 180 | + |
| 181 | +These pins are re-stated in `chapel-ci.yml`, `Justfile`, and |
| 182 | +`docs/decisions/2026-05-30-chapel-rehabilitation.md`. |
0 commit comments