Architecture

MLTTDB is organized around a small HTTP store and multiple validation clients.

proof-assistant source
        |
        | schema / tables / data mode
        v
native Agda or preprocessor
        |
        | GET ordered records
        v
term store API
        |
        | opaque record bodies
        v
proof-assistant validation

Runtime Components

Component Role
SQLite store Persistent databases, table definitions, records, admin API, webapp, discovery, and verification orchestration.
CRUD webapp Human editing interface for databases, tables, records, UUID display, and validation previews.
Preprocessors Generate ordinary Agda, Lean, or Rocq source from MLTTDB-flavoured source.
Native Agda Agda executable that understands MLTTDB modes directly.

Language Paths

Language Available path
Agda Native Agda mode and Agda preprocessor.
Lean Lean preprocessor.
Rocq Rocq preprocessor.

Lean and Rocq currently use preprocessors. Native Lean and native Rocq modes are not part of the implemented runtime.

Client-Side Validation

Client-side validation is useful when your project build should own validation:

  1. Start a term store.
  2. Run native Agda or a preprocessor in data mode.
  3. The validator fetches records from /term-store/v1.
  4. The generated or native proof-assistant process checks the records.

This path fits editor workflows, local proof-assistant commands, and build systems that already know how to run Agda, Lean, or Rocq.

Server-Side Verification

Server-side verification is useful when the store owns the validation trigger:

  1. Store a database language and proof-assistant source path.
  2. Call POST /admin-api/v1/databases/{databaseName}/verify.
  3. The SQLite store selects a configured backend.
  4. The backend runs native Agda or a preprocessor subprocess.
  5. The API returns ok, process output, timing, and generated-file metadata when applicable.

The store remains an orchestrator in this path. It still does not type-check record bodies itself.

Schema Flow

Table definitions can be discovered before records exist:

  1. Run table discovery against proof-assistant source.
  2. Persist discovered table definitions in a database.
  3. Add records through the webapp or admin API.
  4. Verify the database when records change.

This lets an application expose available tables to users without requiring them to type qualified table names manually.