run-experiments

Run the experiments

Needs a clone with committed experiment code that passes local sanity (built to the write-experiment-code contract, uv.lock committed). A sanity run needs no declaration — its outputs are never imported — and is how write-experiment-code checks the code on the platform before the freeze. Every pilot or full run you dispatch must already be declared in .research/record.json in a commit the run will execute — results for an undeclared run_id fail verification, and a claim is verified once every run under it has results — but declare before you dispatch: the record cannot yet tell a preregistered claim from a post-hoc one. Declare late additions with append_to_record (it commits the append itself) and push before dispatching.

1. Resolve the platform. It should already be settled — the code was written against its architecture and environment constraints. Read its reference in full; it is the procedure for steps 2-3. This file states only what every platform must deliver, so a platform is added by adding a reference that answers the same three questions — how the contract CLI is launched, how the run's identifier and commit are obtained, and how its outputs reach the repository.

   Platform	Reference
   GitHub Actions	_shared/references/github-actions.md
   Seyval	_shared/references/seyval.md

2. Run it by the reference's procedure, then fix, commit on top and re-run as needed. However the run starts, record two things when it ends: the platform's run identifier and the commit hash it executed. Step 3 cannot be done without them.

3. Make the run produce what verification reads. Every run starts through the repository's one entry point, make run RUN_ID=<run_id> MODE=<stage> — both platforms call it, and dispatch_experiment builds it for you. The Makefile reads the run's kind from config/run/<run_id>.yaml:

   • An experiment (no kind): the contract CLI (src.main) writes only eval_inputs/ — the raw predictions. The numbers the record is checked against live in metrics.json, which the evaluation step writes, and provenance byte-compares that file against the platform's stored copy. So make run carries the chain through to the end — src.main, make evaluate, src.evaluate — and a command_args of your own must too. Keep eval_inputs/ in the results: it is what the metrics can be re-derived from, and the record anchors it by hash. make evaluate scores the task types named by tasks: in the run config, else every task type in .research/evaluation.json; a run that writes inputs for only some of them (a small and a large split, say) must name its own.
   • A proof (kind: lean): lake build of the named module, then lake exe airas-report writes lean.json — the file the record is checked against. Stages are sanity (the statement type-checks, sorry allowed) and full (a sorry-free proof); there is no pilot. See _shared/references/lean.md.

   On a platform that gives each run a fresh working directory, a later run cannot see an earlier one's output, so either chain the steps in one dispatch or stage the earlier runs into it (Seyval: inputs_from_runs).

4. Bring the results back under .research/results/, committed, with .research/results/.provenance.json declaring per results directory the execution_id and commit_hash from step 2. verify_paper_values pins its provenance cross-check to that file and treats a missing declaration as a mismatch, so results that arrive any other way fail verification. If the same experiment ran more than once, declare the run that should be reported and tell the user the others exist (the selection is reviewable at verification).

Output: committed results under .research/results/ — eval_inputs/, metrics.json and the evaluation report for an experiment, lean.json and the build log for a proof — with their provenance manifest.