Data Formats¶

Fixture Format¶

Loader fixtures use:

{
  "database": "demo",
  "language": "agda",
  "proofAssistantPath": "examples/agda/DemoStep1Numbers.agda",
  "tables": {
    "Demo.Basic.someData": [
      {
        "uuid": "f3dd124c-b2d0-471b-9c7b-4b4f913567be",
        "body": "record body"
      }
    ]
  }
}

proofAssistantPath is optional in fixtures that only preload records.

Bundled fixtures live in:

shared/example-records.json
shared/lean-example-records.json
shared/rocq-example-records.json
shared/procurement-records.json

Validation Record Format¶

Every returned record has:

Field	Meaning
uuid	Lowercase textual UUID.
body	Opaque source-language expression text.

The store does not include row types in validation records. Row types come from proof-assistant source table declarations.

Table Definition Format¶

Discovered table definitions contain:

Field	Meaning
name	Unqualified table name.
qualifiedName	API table identity.
rowType	Source-language row type text.
lineNumber	Source line containing the table declaration.
declarationOrder	Zero-based order among discovered tables.

Stored table definitions also include:

Field	Meaning
sourcePath	Proof-assistant source path used for discovery.

Test Report Format¶

The root test runner writes machine-readable and human-readable artifacts under artifacts/test-runs/{timestamp}/. The HTML summary is intended for browsing; the per-test logs preserve command output.