nx_ingest_pipeline.nx
buildroot/runtime/nx_ingest_pipeline.nx
about
nx_ingest_pipeline.nx -- orchestrate: ingest -> QED-db -> auto-verify.
Wraps the per-source ingesters (MetaMath, Lean, Mizar) with a common
pipeline that:
1. Runs the appropriate ingester on raw corpus bytes
2. Inserts each parsed declaration into nx_qed_db with the right
source_system code and initial verify_status
3. Runs nx_auto_verify over the inserted entries
4. Emits an aggregate JSON-line stats record
Substrate-native, no AI, no external network.
genealogy_id: wiedijk_qed_1994 (unified pipeline vision)
lineage_id: theorem_ingestion + autonomous_proving + qed_database
dependencies 8 imports · 1 importers
imports: syscalls.nxnx_axioms.nxnx_qed_db.nxnx_prover.nxnx_auto_verify.nxnx_theorem_ingest.nxnx_lean_ingest.nxnx_mizar_ingest.nx
imported by: nx_ingest_pipeline_test.nx
structs
| 39 | struct PipelineResult |
consts
| 33 | const NX_PIPE_SRC_METAMATH: i64 = 0 |
| 34 | const NX_PIPE_SRC_LEAN: i64 = 1 |
| 35 | const NX_PIPE_SRC_MIZAR: i64 = 2 |
| 49 | const NX_PIPE_RESULT_BYTES: i64 = 56 |
functions
| 51 | func nx_pipe_result_alloc() -> *PipelineResult called by 1: main |
| 69 | func nx_pipe_run_metamath(buf: *u8, len: i64, qed: *QedDb, |
| 105 | func nx_pipe_run_lean(buf: *u8, len: i64, qed: *QedDb, |
| 136 | func nx_pipe_run_mizar(buf: *u8, len: i64, qed: *QedDb, |
| 169 | func nx_ingest_pipeline_run(src_code: i64, buf: *u8, len: i64, qed: *QedDb, |
| 190 | func pp_putc(fd: i64, c: i64) -> i64 called by 1: pp_i64 |
| 197 | func pp_str(fd: i64, s: *u8, n: i64) -> i64 called by 1: nx_pipe_emit_result |
| 202 | func pp_i64(fd: i64, n: i64) -> i64 |
| 226 | func nx_pipe_emit_result(fd: i64, r: *PipelineResult) -> i64 |