Checking Your Setup¶

MLTTDB includes a local validation command that checks the bundled store, preprocessor, and native Agda examples on your machine.

Run:

python3 tools/mlttdb_test.py

or:

npm test

The command is useful after installing dependencies, changing local configuration, or upgrading the native Agda executable.

HTML Report¶

Each run writes a timestamped report under:

artifacts/test-runs/

The rolling HTML summary is:

artifacts/test-runs/index.html

Open that file in a browser to see pass, fail, and skip status for the local setup.

Native Agda Setup¶

If the native Agda check reports that the executable is missing or stale, install the MLTTDB Agda executable first:

tools/install_agda_native_mlttdb.sh

Then rerun:

python3 tools/mlttdb_test.py

To ask the checker to install or refresh native Agda before running:

python3 tools/mlttdb_test.py --ensure-native-agda

What The Check Covers¶

Area	What is exercised
SQLite store	Validation API, admin API, webapp static assets, table definitions, discovery, verification, and fixtures.
Preprocessors	Agda, Lean, and Rocq schema, data, and table-discovery modes.
Native Agda	Data-mode and table-discovery examples when a matching MLTTDB Agda executable is available.

This checker is for confirming that your local MLTTDB installation works. It is not required for using the HTTP API or webapp directly.