Preprocessors¶

Preprocessors let the demonstration profile run on ordinary proof-assistant installations. They consume extended source with table declarations and emit ordinary source for schema or data checking.

Language	Script	Input option	Output option
Agda	preproc/agda_tdb_preprocess.py	positional input	--out
Lean	preproc/lean_tdb_preprocess.py	--input	--output
Rocq	preproc/rocq_tdb_preprocess.py	--input	--output

All preprocessors support:

--tdb-mode=schema
--tdb-mode=data
--tdb-mode=tables

Data mode also requires:

--tdb-host HOST
--tdb-port PORT
--tdb-name DATABASE

Agda¶

Schema mode rewrites:

x :T: A

into:

x : Type _
x = A

Data mode removes table declarations and emits ordinary Agda definitions for fetched records using encoded UUID identifiers.

Lean¶

Schema mode rewrites table declarations into transparent ordinary Lean abbreviations:

abbrev x : Sort _ := A

Data mode emits fetched records inside a generated TermDatabaseValidation namespace.

Rocq¶

Schema mode rewrites:

x :T: A.

into:

Definition x : Type := A.

Data mode emits ordinary Rocq Local Definitions with canonical encoded UUID identifiers.

Limits¶

The preprocessors are demonstration-profile parsers. They are not semantic proof-assistant implementations. The generated ordinary source is the artifact that should be checked by Agda, Lean, or Rocq.