feat(chapel): per-prover outcome telemetry for bench_mrr (#162) - #394
Closed
arena-ai-coding-agent[bot] wants to merge 3 commits into
Closed
arena-ai-coding-agent[bot] wants to merge 3 commits into
arena-ai-coding-agent[bot] wants to merge 3 commits into
Conversation
Retarget 338 stale path references across 83 files where the AsciiDoc counterpart exists at the identical path. Pure reference swap: 239 insertions / 239 deletions. No file was renamed, created or deleted to clear an alert. Load-bearing fixes beyond navigation: - .github/canonical-references/prover-counts.yml declared canonical_pointer: docs/PROVER_COUNT.md, which does not exist, so the R5a canonical-reference guardrail was pointing at nothing. It now resolves. - The Justfile er-schema-drift-check recipe ran sha256sum against docs/architecture/VERISIM-ER-SCHEMA.md and therefore failed on a missing file. It now hashes the real document. No pinned hash was invalidated: .machine_readable/er-schema.sha256 does not exist. Names that merely contain a migrated basename were left alone (FUTURE_DEVELOPMENT_ROADMAP.md, PROVER_EXPANSION_ROADMAP.md, CORRECTNESS-ARCHITECTURE.md, ECHIDNA-TODO.md). Adds docs/STALE-REFERENCE-TOMBSTONES.adoc, recording each old to new path pair, the references deliberately left in place (dated records, external and cross-repo paths, the playground sub-project) and the targets that were never renames: .machine_readable/6a2/ and src/rescript/ are absent, and all 33 .hypatia-ignore exemptions name deleted .res files. Machine-readable state files stay parseable: every touched .a2ml file has identical line count and identical TOML validity to HEAD. Dangling repository-internal doc targets: 129 -> 112. Refs #242 Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Second pass over the same structural-drift class as the previous commit. The first pass covered the 16 highest-volume targets; this one sweeps every remaining .md reference that has a verified .adoc counterpart. 151 further sites retargeted across 61 files, bringing the change to 502 references across 109 files. No file was renamed, created or deleted. The sweep is gated on target existence rather than blind rewriting, so two false-positive classes are excluded: - References to files that genuinely exist as .md are left alone. 47 references fall in this class over the 21 tracked .md files (SECURITY.md, CLAUDE.md, GEMINI.md, .github/CONTRIBUTING.md, .github/PROVEN-INTEGRATION.md, docs/wiki/*.md, GitLab templates). SECURITY.md coexists with SECURITY.adoc and is not stale. - Names that merely contain a migrated basename are left alone (FUTURE_DEVELOPMENT_ROADMAP.md, CORRECTNESS-ARCHITECTURE.md, ECHIDNA-TODO.md, PROVER_EXPANSION_ROADMAP.md). Two further guardrail fixes, same species as canonical_pointer: - .github/canonical-references/prover-counts.yml listed AUTHORS.md and CODE_OF_CONDUCT.md in scope.include. Neither exists, so the R5a guardrail was not scanning those surfaces at all. - Justfile er-schema-drift-check and the CREUSOT-SETUP path resolved to missing .md files. docs/STALE-REFERENCE-TOMBSTONES.adoc is updated with the full migration table, the deliberately-preserved sites (dated records, the echidna-playground sub-project, external and cross-repo paths, the dual-spelling fallback probes) and the 100 sites that name a path absent in both spellings, which are follow-ups rather than edits. Machine-readable state files stay parseable: zero TOML-validity regressions across the touched .a2ml files. Dangling repository-internal doc targets: 112 -> 108 (129 before the first pass). Refs #242 Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Implements #162. The L2.3 ADR introduced exitCode = -5 for preempted losers, distinct from -3 (timeout) and -4 (subprocess error), but bench_mrr only reported success/winning_prover per strategy run, so the wall-clock improvement attributable to preemption was not measurable. Outcome model (parallel_proof_search.chpl): - New ProverOutcome enum plus outcomeLabel/categoryLabel/classifyOutcome mapping the documented exit-code contract: 0 success, >0 prover rejection, -1 not on PATH, -2 temp-file write failure, -3 timeout, -4 spawn/IO error, -5 preempted. The two -2/-4 causes collapse into subprocess_error because both mean the prover never got a fair hearing. - NotAttempted is deliberately not an exit code: the sequential strategy returns at the first success, so provers after the winner are reported as not_attempted rather than silently dropped from the breakdown. - Each strategy gains a telemetry variant that fills a per-prover results/attempted table indexed by provers.domain (not ProverInfo.id, so filtered registries stay correctly indexed). The existing public procs are now thin wrappers over those variants, so what the bench measures and what it reports are the same code path. Outputs (bench_mrr.chpl): - stdout wall-clock CSV, unchanged columns. - bench_mrr_telemetry.csv: one row per prover per fixture x strategy (360 rows for the stock matrix), never omitting rows. - bench_mrr_summary.csv: per fixture x strategy plus an ALL row per strategy aggregating the corpus, with preemption_rate = preempted/attempted_total measured against provers that actually ran. - --telemetry-only=true omits the stdout wall-clock CSV. Also adds `just bench-chapel-mrr-telemetry`, gitignores the generated CSVs, and documents the column contracts in docs/bench/README.adoc. NOT VERIFIED BY EXECUTION: this environment has no Chapel toolchain, so bench_mrr could not be built or run. The acceptance criterion asking for a re-run showing preemption rates next to wall-clock is therefore not satisfied here; docs/bench/README.adoc records the re-run procedure and the baseline writeup is explicitly left un-refreshed rather than filled with estimates. Refs #162 Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
arena-ai-coding-agent
Bot
requested a review
from hyperpolymath
as a code owner
September 25, 2026 14:34
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Contributor
Author
|
Consolidating into #393. This session is pinned to a single head branch (
Each issue is reviewable commit-by-commit. |
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.
test