Table Discovery¶

Table discovery extracts table definitions from proof-assistant source. It is used to create or update database schemas before records exist.

Discovery JSON¶

All discovery backends produce the same shape:

{
  "language": "agda",
  "tables": [
    {
      "name": "someData",
      "qualifiedName": "Demo.Basic.someData",
      "rowType": "MyRowType",
      "lineNumber": 12,
      "declarationOrder": 0
    }
  ]
}

The store adds sourcePath when it persists definitions for a database.

Preprocessor CLI¶

Agda:

python3 preproc/agda_tdb_preprocess.py \
  --tdb-mode=tables \
  examples/agda/DemoStep1Numbers.agda

Lean:

python3 preproc/lean_tdb_preprocess.py \
  --tdb-mode=tables \
  --input examples/lean/DemoLeanExamples.lean

Rocq:

python3 preproc/rocq_tdb_preprocess.py \
  --tdb-mode=tables \
  --input examples/rocq/DemoRocqExamples.v

Each command writes JSON to stdout. Agda accepts --out; Lean and Rocq accept --output.

Native Agda CLI¶

Native Agda table discovery validates the Agda source schema and emits JSON:

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

When using the repository test helper, the selected Agda executable must be installed from the current proof-assistants/agda build-relevant source.

Store API¶

Discover tables without creating a database:

curl -s \
  -X POST \
  -H 'Content-Type: application/json' \
  -d '{"language":"lean","proofAssistantPath":"examples/lean/DemoLeanExamples.lean"}' \
  'http://127.0.0.1:8080/admin-api/v1/table-definitions/discover'

Create or replace a database schema from source:

curl -s \
  -X POST \
  -H 'Content-Type: application/json' \
  -d '{"language":"lean","proofAssistantPath":"examples/lean/DemoLeanExamples.lean"}' \
  'http://127.0.0.1:8080/admin-api/v1/databases/lean-demo/create-from-source'

List stored table definitions:

curl -s \
  'http://127.0.0.1:8080/admin-api/v1/databases/lean-demo/table-definitions'

Backend Selection¶

The SQLite store accepts:

--table-discovery-backend auto
--table-discovery-backend agda-native
--table-discovery-backend agda-preprocessor
--table-discovery-backend lean-preprocessor
--table-discovery-backend rocq-preprocessor
--table-discovery-backend preprocessor

auto selects native Agda for Agda and preprocessors for Lean and Rocq. preprocessor selects a preprocessor for all supported languages.