MLTTDB

MLTTDB is a local term-store system for proof-assistant projects. It lets a source file declare typed tables, keeps table records in an external store, and then asks a proof assistant or generated proof-assistant code to validate those records on demand.

Use MLTTDB when you want proof-assistant-checked data without embedding all data directly in the proof-assistant source tree.

What You Can Do

Task Where to start
Run the SQLite term store and webapp Getting Started
Declare tables in Agda, Lean, or Rocq-flavoured source Paradigm
Populate or edit records in a browser Term Store
Discover tables from proof-assistant source Table Discovery
Validate records from the server side Verification
Generate ordinary proof-assistant source Preprocessors
Use native Agda support Native Agda
Embed MLTTDB in another project Use In A Project

Runtime Pieces

Piece Purpose
SQLite store Persistent HTTP store, CRUD webapp, table discovery, and verification orchestration.
CRUD webapp Browser interface for databases, tables, records, validation previews, and UUID display.
Preprocessors Convert MLTTDB-flavoured Agda, Lean, and Rocq source into ordinary source.
Native Agda Agda executable with direct --tdb-mode support.

The validation API returns ordered records as opaque source text:

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

The store does not type-check the record body. Validation happens in native Agda or in generated ordinary Agda, Lean, or Rocq code.

Typical Loop

  1. Write proof-assistant source that declares tables.
  2. Discover table definitions from that source.
  3. Create or update a database schema in the store.
  4. Add records through the webapp or admin API.
  5. Run verification from the store, or run a preprocessor/native command from your own project.

Build These Docs

Build the HTML site:

make -C docs html

Build a PDF:

make -C docs pdf

The outputs are generated under artifacts/docs/.