Known Limits

MLTTDB is currently a local-first demonstration profile, not a production database service.

Security And Deployment

The SQLite store currently provides unauthenticated HTTP APIs. Use it on a local machine or a trusted development network.

Before exposing it to untrusted users, add the deployment controls your environment needs, such as authentication, authorization, TLS, request limits, and backup policy.

Validation Consistency

For the current profile, avoid mutating a database during one validation run. The store returns deterministic record order for a fixed database state, but it does not hold a validation transaction open while a proof-assistant process is running.

For reliable workflows, treat verification as a check of a snapshot you do not edit until the command finishes.

Language Coverage

Language Current path
Agda Native Agda and Agda preprocessor
Lean Lean preprocessor
Rocq Rocq preprocessor

Native Lean and native Rocq executables are not implemented in the current runtime. Use preprocessors for those languages.

Native Agda Portability

Native Agda is installed through the helper script:

tools/install_agda_native_mlttdb.sh

The installed executable is intended to behave like a normal user Agda installation, including ordinary library lookup and agda-mode setup.

If a native Agda check fails on another machine, first confirm:

  • agda on PATH is the MLTTDB-enabled executable.
  • agda --help lists --tdb-mode.
  • Existing libraries are configured through normal Agda library files.
  • The executable was rebuilt after MLTTDB Agda source changes.

Schema Replacement With Existing Records

Creating a database from source replaces stored table definitions. Existing records are not automatically deleted just because their table definition is no longer discovered.

As a result, admin table listings can include:

  • tables from the current source schema;
  • tables that still have records from earlier schema versions.

Delete obsolete tables explicitly when you want old records removed from the database.