feat(chapel): per-prover cwd + filenameOverride hooks (closes #158, closes #159)#164
Merged
Merged
Conversation
…uccess in bench (closes #158, closes #159) Wave-1 MRR baseline (docs/bench/2026-05-30-chapel-mrr-baseline.md) caveats 1 + 2: Idris2 and Agda fixtures failed across all three strategies because tryProver's uniform spawn contract (parent CWD, generic `goal_<name>_<nodeId>.<ext>` basename) violates each prover's module-name + source-directory constraints. ProverInfo gains two optional fields with empty-string defaults that preserve the prior contract for the 28 unaffected provers: - cwd: shell-wrapped `sh -c "cd <cwd> && exec ..."` to be coforall- safe (process-global chdir would race against parallel spawn calls). - filenameOverride: literal basename for provers that enforce module-name = filename. Registry: Agda gets cwd=/tmp/echidna-chapel + filenameOverride= "Trivial.agda" (matches new fixture's `module Trivial where`); Idris2 gets cwd + filenameOverride="Trivial.idr" (existing fixture already declares `module Trivial`). Justfile bench-chapel-mrr derives IDRIS2_PREFIX from `which idris2` so the recipe is self-contained. Verified: `just bench-chapel-mrr` shows agda_trivial → true and idris2_trivial → true across sequential/best-of/speculative (0.101-1.970s, full results updated in the baseline doc). ADR: docs/decisions/2026-05-31-chapel-prover-spawn-hooks.md. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
ProverInfogains two optional fields (cwd,filenameOverride) with empty-string defaults; preserves prior contract for the 28 unaffected provers.agda_trivial.agdafixture and a refreshedidris2_trivial.idr(already correctly shaped).tryProvershell-wraps the spawn whencwdis set (sh -c \"cd <cwd> && exec ...\") for coforall-safety;filenameOverrideswaps the generic basename when set.bench-chapel-mrrderivesIDRIS2_PREFIXfromwhich idris2— the recipe is now self-contained, no parent-shell ceremony.Result
just bench-chapel-mrr(single-run, full table in updated baseline doc):Both acceptance criteria (Idris2 success in ≥1 strategy, Agda fixture round-trip) satisfied across all three strategies.
Wave-1 baseline caveats resolved
Test plan
just chapel-build— green (only known main()-in-library-mode warning)just chapel-smoke—parallel-CAS winner: 3 (expected 3)just bench-chapel-mrr— Idris2 + Agda → true across all 3 strategiesADR:
docs/decisions/2026-05-31-chapel-prover-spawn-hooks.mdcovers mechanism + alternatives considered (env-extra list, regex extraction, function-pointer callback, native Chapel cwd param).🤖 Generated with Claude Code