API Reference¶

This page documents the SQLite store API exposed by the current MLTTDB implementation.

Validation API¶

GET /term-store/v1/databases/{databaseName}/records?table={qualifiedTableName}&language={language}

Success:

{
  "database": "demo",
  "language": "agda",
  "table": "Demo.Basic.someData",
  "records": [
    {
      "uuid": "f3dd124c-b2d0-471b-9c7b-4b4f913567be",
      "body": "record body"
    }
  ]
}

The language query is required and must match the database language annotation.

Admin Databases¶

GET /admin-api/v1/databases
PUT /admin-api/v1/databases/{databaseName}
GET /admin-api/v1/initialization

PUT body:

{
  "language": "agda",
  "proofAssistantPath": "examples/agda/DemoStep1Numbers.agda"
}

GET /admin-api/v1/initialization reports whether configured proof-assistant sources have passed the server's initial typecheck gate. The webapp uses this endpoint before opening the normal interface.

{
  "enabled": true,
  "ready": false,
  "statuses": [
    {
      "database": "demo",
      "language": "agda",
      "state": "running",
      "proofAssistantPath": "examples/agda/Demo/GenericRows.agda",
      "message": "Initial proof-assistant typecheck is running."
    }
  ],
  "blocking": []
}

Admin Tables And Records¶

GET    /admin-api/v1/databases/{databaseName}/tables
GET    /admin-api/v1/databases/{databaseName}/tables/{tableName}/records
POST   /admin-api/v1/databases/{databaseName}/tables/{tableName}/records
PUT    /admin-api/v1/databases/{databaseName}/records/{uuid}
DELETE /admin-api/v1/databases/{databaseName}/records/{uuid}
DELETE /admin-api/v1/databases/{databaseName}/tables/{tableName}
POST   /admin-api/v1/databases/{databaseName}/preload-example-data

Create record body:

{
  "body": "source-language expression"
}

Applications may pass an explicit uuid when importing records that already have stable external identities. Otherwise, omit it and let the store generate one.

Table Definitions¶

POST /admin-api/v1/table-definitions/discover
POST /admin-api/v1/databases/{databaseName}/create-from-source
GET  /admin-api/v1/databases/{databaseName}/table-definitions

Discovery and create-from-source body:

{
  "language": "lean",
  "proofAssistantPath": "examples/lean/DemoLeanExamples.lean"
}

Discovery response:

{
  "language": "lean",
  "backend": "lean-preprocessor",
  "proofAssistantPath": "examples/lean/DemoLeanExamples.lean",
  "tables": []
}

Verification¶

POST /admin-api/v1/databases/{databaseName}/verify

Verification response:

{
  "database": "demo",
  "language": "agda",
  "backend": "agda-native",
  "proofAssistantPath": "examples/agda/DemoStep1Numbers.agda",
  "ok": true,
  "exitCode": 0,
  "signal": null,
  "durationSeconds": 0.42,
  "stdout": "",
  "stderr": ""
}

For preprocessor backends, the response may include generatedPath.

Row Evaluation¶

POST /admin-api/v1/databases/{databaseName}/records/{uuid}/eval

Body:

{
  "expression": "editorValueJSON genericRow ({body})",
  "module": "Demo.GenericRows"
}

module is optional for Agda tables whose qualified table name contains a module prefix. The store uses the database's proofAssistantPath and a language-compatible row-evaluation backend. In the current implementation this is native modified Agda only.

The store passes MLTTDB control arguments to Agda. Proof-assistant semantic flags such as Cubical mode belong in source files or .agda-lib configuration, not in the store command.

Structured Editors¶

Per-table editor configuration:

PUT    /admin-api/v1/databases/{databaseName}/tables/{tableName}/editor
GET    /admin-api/v1/databases/{databaseName}/tables/{tableName}/editor
DELETE /admin-api/v1/databases/{databaseName}/tables/{tableName}/editor

PUT body:

{
  "kind": "agda-string-atom-generic",
  "specExpression": "editorSpecificationJSON genericRow",
  "valueExpression": "editorValueJSON genericRow ({body})",
  "sourceExpression": "editorSourceFromJSONOr {bodyString} genericRow {json}",
  "maxDepth": 8
}

{body} is replaced with the current record body as raw source. {bodyString} is replaced with an Agda string literal containing the current record body. {json} is replaced with an Agda string literal containing edited generic JSON.

Load a configured editor for a record:

GET /admin-api/v1/databases/{databaseName}/records/{uuid}/editor

Render an edited generic value back to source:

POST /admin-api/v1/databases/{databaseName}/records/{uuid}/editor/source

Body:

{
  "value": []
}

The response includes body, which the webapp places into the record body textarea before saving.

Error Shape¶

Errors use:

{
  "error": {
    "code": "unknown-database",
    "message": "Database does not exist."
  }
}

Validation failures from proof assistants are represented as verification results with ok: false, not as API errors.