Getting Started¶

This workflow runs the SQLite store and validates bundled example data.

Requirements¶

• Python 3 for preprocessors and the root test runner.
• Node.js 22.5 or newer for the SQLite store.
• A browser for the CRUD webapp.
• Optional: Cabal and the Agda subrepository for native Agda validation.

The demo profile uses unauthenticated HTTP. It is intended for local demonstration and test workflows.

Run The SQLite Store¶

Start the store with Agda example data:

npm run sqlite-store -- --host 127.0.0.1 --port 8080 --db-file term-store.sqlite3 --preload-example-data

The validation base URL is:

http://127.0.0.1:8080/term-store/v1

The CRUD webapp is served from:

http://127.0.0.1:8080/

Optional Structured Editor Demo¶

The Agda fixture includes Demo.GenericRows.rows. To use the ff-generics structured editor for that table, set the Agda source path and configure the table editor:

curl -s \
  -X PUT \
  -H 'Content-Type: application/json' \
  -d '{"language":"agda","proofAssistantPath":"examples/agda/Demo/GenericRows.agda"}' \
  'http://127.0.0.1:8080/admin-api/v1/databases/demo'

curl -s \
  -X PUT \
  -H 'Content-Type: application/json' \
  -d '{
    "kind":"agda-string-atom-generic",
    "specExpression":"editorSpecificationJSON genericRow",
    "valueExpression":"editorValueJSON genericRow ({body})",
    "sourceExpression":"editorSourceFromJSONOr {bodyString} genericRow {json}",
    "maxDepth":8
  }' \
  'http://127.0.0.1:8080/admin-api/v1/databases/demo/tables/Demo.GenericRows.rows/editor'

Open the row in the webapp. The structured editor appears below the record body when native Agda row evaluation is available.

Fetch Records¶

curl -s 'http://127.0.0.1:8080/term-store/v1/databases/demo/records?table=Demo.Basic.someData&language=agda'

Unknown or empty tables return 200 OK with an empty records array when the database exists and the language matches.

Run A Preprocessor¶

Schema mode does not contact the store:

python3 preproc/agda_tdb_preprocess.py \
  --tdb-mode=schema \
  --out artifacts/generated/demo-schema.agda \
  examples/agda/DemoStep1Numbers.agda

Data mode fetches records and writes ordinary Agda:

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

Lean and Rocq use --input and --output instead of Agda's positional input and --out; see Preprocessors.

Run Tests¶

python3 tools/mlttdb_test.py

The root runner writes an HTML test summary under artifacts/test-runs/ and updates artifacts/test-runs/index.html.