lean-bench

2. Result schema🔗

lean-bench emits machine-readable results as JSONL — one JSON object per line — written to the child process's stdout and consumed by the parent. Downstream tooling (baseline diffs, CI dashboards, exporters) also reads these rows. This document pins the schema and spells out the evolution rules so producers and consumers can rely on it.

The single source of truth in the code is LeanBench/Schema.lean: the schemaVersion constant, the canonical key sets, and the parser shared by Run.parseChildRow and Run.parseFixedChildRow.

  1. 2.1. Row kinds
  2. 2.2. Versioning
  3. 2.3. Required vs optional fields
  4. 2.4. Environment metadata
  5. 2.5. Memory metrics
  6. 2.6. Compatibility
  7. 2.7. Export format
  8. 2.8. Migration
  9. 2.9. Test enforcement