Term Store¶

The term store is the HTTP server that stores databases, table definitions, and ordered records.

SQLite Store¶

The implemented persistent store is:

sqlite-store/term_store_sqlite.js

Run it with:

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

It uses Node's built-in node:sqlite module and requires Node.js 22.5 or newer. It serves:

• validation API under /term-store/v1
• administrative API under /admin-api/v1
• CRUD webapp from /
• ff-generics editor assets from /ff-generics/ when configured

Database Metadata¶

Each database stores:

Field	Meaning
databaseName	Database identity in API paths.
language	One of agda, lean, or rocq.
proofAssistantPath	Source file used for table discovery and verification.

Set metadata:

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

Records¶

Records are stored per database and table. The store generates lowercase UUIDs unless a test or fixture provides one explicitly.

The validation API returns live records in deterministic table order.

Table Definitions¶

Table definitions are stored independently from records. This supports creating a database from proof-assistant source before inserting data.

Stored definitions include:

name
qualifiedName
rowType
sourcePath
lineNumber
declarationOrder

When listing tables through the admin API, table names include both schema definitions and tables that currently have records.

Row Evaluation¶

The administrative API can ask a configured backend to evaluate an expression in the context of a stored row. The database must have a proofAssistantPath, and the selected backend must support the database language.

When initialization checks are enabled, the store first runs a proof-assistant typecheck/table-discovery pass for every configured database. The webapp opens the normal interface only after those checks pass; while they run, it shows the initialization status returned by /admin-api/v1/initialization.

The current implementation supports this for Agda through the modified native compiler:

curl -s \
  -X POST \
  -H 'Content-Type: application/json' \
  -d '{"expression":"editorValueJSON genericRow ({body})"}' \
  'http://127.0.0.1:8080/admin-api/v1/databases/demo/records/{uuid}/eval'

MLTTDB control arguments are passed on the command line. Semantic Agda options must live in the source file or library configuration.

Structured Editors¶

The webapp can display an ff-generics structured editor for a record when its table has an editor configuration. The store does not infer constructors or know type-specific code; it stores proof-assistant expressions supplied by the database author.

Configure a table:

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'

The Agda source file is responsible for importing ff-generics, providing or deriving the Generic StringAtoms value, and exposing helper expressions such as editorSpecificationJSON, editorValueJSON, and editorSourceFromJSONOr.