Configuration Reference¶

SQLite Store CLI¶

--host HOST
--port PORT
--db-file PATH
--preload-example-data
--preload-lean-example-data
--preload-rocq-example-data
--preload-procurement-data
--preload-fixture PATH
--verification-backend NAME
--verification-timeout SECS
--evaluation-backend NAME
--evaluation-timeout SECS
--initialization-timeout SECS
--disable-initialization-checks
--table-discovery-backend NAME
--table-discovery-timeout SECS
--ff-generics-web-dir PATH
--quiet
--help

Defaults:

Option	Default
--host	127.0.0.1
--port	8080
--db-file	term-store.sqlite3
--verification-backend	auto
--verification-timeout	900
--evaluation-backend	auto
--evaluation-timeout	900
--initialization-timeout	900
--disable-initialization-checks	false
--table-discovery-backend	auto
--table-discovery-timeout	900
--ff-generics-web-dir	$FF_GENERICS_WEB_DIR or /Users/marcin/agdaLibs/ff-generics/unsafe/web

Verification Backends¶

Allowed values:

auto
agda-native
lean-preprocessor
rocq-preprocessor
preprocessor

Language support:

Backend	Languages
agda-native	agda
lean-preprocessor	lean
rocq-preprocessor	rocq
preprocessor	lean, rocq
auto	agda through native Agda, Lean/Rocq through preprocessors

Table Discovery Backends¶

Allowed values:

auto
agda-native
agda-preprocessor
lean-preprocessor
rocq-preprocessor
preprocessor

preprocessor is valid for Agda, Lean, and Rocq discovery.

Row Evaluation Backends¶

Allowed values:

auto
agda-native

The current row-evaluation and structured-editor workflow is implemented only for Agda through the modified native compiler.

Environment Variables¶

Variable	Used By	Meaning
AGDA_BIN	Native Agda scripts and server-side Agda verification	Path to Agda executable.
AGDA_DATA	Native Agda tests	Agda data directory override.
AGDA_INSTALL_DIR	Native Agda installer	Destination directory for installed agda.
FF_GENERICS_WEB_DIR	SQLite store webapp	Directory containing ff-generics editor JavaScript and CSS assets.
MLTTDB_AUTO_INSTALL_AGDA	Local setup checker	When 1, install or refresh native Agda before selected native checks.

Preprocessor CLI Options¶

Agda:

--tdb-mode schema|data|tables
--tdb-host HOST
--tdb-port PORT
--tdb-name DATABASE
--out PATH
INPUT

Lean and Rocq:

--tdb-mode schema|data|tables
--tdb-host HOST
--tdb-port PORT
--tdb-name DATABASE
--input PATH
--output PATH

schema and data require an output path. tables writes JSON to stdout when no output path is provided.