Native Agda¶

Native Agda support is an Agda executable with MLTTDB modes built in. Use it when you want Agda itself to read table declarations, fetch store records, and validate data.

Install¶

Build and install the MLTTDB Agda executable into the user Cabal bin:

tools/install_agda_native_mlttdb.sh

The default install directory is:

$HOME/.cabal/bin

Override it when needed:

AGDA_INSTALL_DIR=/path/to/bin tools/install_agda_native_mlttdb.sh

The installer uses standard cabal install for agda and agda-mode. After installation, make sure the install directory is on PATH:

which agda
agda --version

Emacs¶

Install the matching Agda mode files after installing the executable:

agda-mode setup

This keeps Emacs using the same Agda package that provides MLTTDB support.

Modes¶

Schema mode checks table declarations without contacting the store:

agda --tdb-mode=schema examples/agda/DemoStep1Numbers.agda

Data mode fetches records and validates them:

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

Table mode emits discovered table definitions as JSON:

agda --tdb-mode=tables examples/agda/DemoStep1Numbers.agda

Row-evaluation mode evaluates one expression in the context immediately before a selected database row is introduced:

agda \
  --tdb-mode=eval \
  --tdb-host 127.0.0.1 \
  --tdb-port 8080 \
  --tdb-name demo \
  --tdb-module Demo.Step1Numbers \
  --tdb-row c1000000-0000-4000-8000-000000000003 \
  --tdb-expr "suc b1000000-0000-4000-8000-000000000002" \
  examples/agda/DemoStep1Numbers.agda

The command emits JSON with the expression type and normal form. The selected row itself is not available to the expression; earlier rows are available by UUID using the same order rule as data mode.

Runtime Request¶

In data mode, Agda requests:

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

Each returned record body is checked at the row type declared by the corresponding :T: table declaration.

Use Existing Agda Libraries¶

The installed executable is a normal Agda executable. Existing libraries should continue to work through the usual Agda library configuration:

agda -l cubical your-file.agda

If Agda cannot find a library, check the same files you would check for a standard Agda installation, such as ~/.agda/libraries and ~/.agda/defaults.

Verify The Installed Executable¶

For a quick smoke check:

agda --help | grep tdb-mode

For the repository’s bundled native examples:

sh tools/run_agda_native_mlttdb.sh

That script expects the installed executable to support MLTTDB modes and to match the current MLTTDB Agda build inputs.