Use In A Project¶

This page is for building a project that uses MLTTDB as a term-store and validation layer.

Choose A Validation Path¶

Situation	Recommended path
Your project is Agda-first and can use the MLTTDB Agda executable	Native Agda
You need ordinary Agda output for an existing toolchain	Agda preprocessor
You are validating Lean source	Lean preprocessor
You are validating Rocq source	Rocq preprocessor
You want users to trigger validation from the webapp/API	Server-side verification

Native Agda gives the tightest Agda workflow. Preprocessors are easier to integrate into existing proof-assistant builds because they emit ordinary source files.

Model Your Tables¶

Keep table declarations close to the row types they validate. Prefer qualified names that are stable across source reorganizations, because the qualified table name is what records use in the store.

For Agda:

module Demo.Basic where

someData :T: MyRowType

The store table name is:

Demo.Basic.someData

Use one database per language or project boundary. Avoid mixing unrelated source trees in a single database unless they share a validation lifecycle.

Create The Database Schema¶

Use table discovery when you want the store to know table definitions before records are inserted:

curl -s \
  -X POST \
  -H 'Content-Type: application/json' \
  -d '{"language":"agda","proofAssistantPath":"examples/agda/DemoStep1Numbers.agda"}' \
  'http://127.0.0.1:8080/admin-api/v1/databases/demo/create-from-source'

The store records the database language, proof-assistant source path, and table definitions. The webapp can then show tables even if they have no records yet.

Add And Edit Records¶

For manual work, open the webapp:

http://127.0.0.1:8080/

For application integration, use the admin API to create records. Let the store generate UUIDs unless your application already owns stable IDs.

curl -s \
  -X POST \
  -H 'Content-Type: application/json' \
  -d '{"body":"myNat zero"}' \
  'http://127.0.0.1:8080/admin-api/v1/databases/demo/tables/Demo.Basic.someData/records'

Treat record order as meaningful. If your application imports records from another source, preserve the order expected by the proof-assistant code.

Validate From Your Build¶

For a generated-source workflow, run a preprocessor in data mode and then run your normal proof-assistant command on the generated file:

python3 preproc/agda_tdb_preprocess.py \
  --tdb-mode=data \
  --tdb-host 127.0.0.1 \
  --tdb-port 8080 \
  --tdb-name demo \
  --out artifacts/generated/demo-data.agda \
  examples/agda/DemoStep1Numbers.agda

For native Agda:

agda \
  --tdb-mode=data \
  --tdb-host 127.0.0.1 \
  --tdb-port 8080 \
  --tdb-name demo \
  examples/agda/DemoStep1Numbers.agda

Validate From The Store¶

Use server-side verification when the store should run validation on demand:

curl -s \
  -X POST \
  'http://127.0.0.1:8080/admin-api/v1/databases/demo/verify'

This is useful for UI buttons, CI-like checks, and applications where users edit records through the store rather than through proof-assistant tooling.

Operational Checklist¶

• Run the SQLite store on a local or trusted network.
• Set the database language and proof-assistant path.
• Discover table definitions after source tables change.
• Add records through the webapp or admin API.
• Run verification after record edits.
• Keep generated preprocessor output under an ignored build/artifact directory.

The current demo server is unauthenticated. Put it behind your own access control if you expose it beyond a local development machine.