nx_coq_dir_ingest.nx source
↩ module page · 74 lines · 2727 B
1// nx_coq_dir_ingest.nx -- ingest every Coq decl in the corpus at
2// nxc2/_offc/coq_corpus.txt (assembled by nx_ingest_dir.sh).
3//
4// Same shape as nx_lean_dir_ingest; only the parser, bridge, output
5// prefix, and corpus path differ -- the rest is identical (which is
6// the "point at X" promise: per-source code is minimal).
7//
8// genealogy_id: substrate_self_hosting_synth_2026_05_14 + point_at_x_ingester
9// lineage_id: per_source_dir_driver
10
11// nx_safety_envelope:
12// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
13// sil_target: SIL1
14// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
15// verdict: NOT_YET_EVALUATED
16
17import "nx_syscalls.nx"
18import "nx_runtime.nx"
19import "nx_tier.nx"
20import "nx_coq_ingest.nx"
21import "nx_ingest_runner.nx"
22import "nx_coq_stream_ingest.nx"
23import "nx_bloom_capacity.nx"
24
25const NX_COQ_DIR_DISK_BUDGET: nx_size = 1073741824
26const NX_COQ_DIR_SHARD_BYTES: nx_size = 104857600
27const NX_COQ_DIR_BLOOM_CAPACITY: nx_int = 1000000
28const NX_COQ_DIR_WATCHDOG_MS: nx_int = 60000
29
30func main() -> nx_exit {
31 let corpus_path: *u8 = "nxc2/_offc/coq_corpus.txt" as *u8
32 let out_prefix: *u8 = "/tmp/nx_ingest_coq" as *u8
33 let ckpt_path: *u8 = "/tmp/nx_ingest_coq.checkpoint" as *u8
34
35 let corpus_len_p: *nx_size = (sys_mmap(NX_SIZEOF_NX_SIZE)) as *nx_size
36 corpus_len_p[0] = 0
37 let corpus: *u8 = sys_read_file(corpus_path, corpus_len_p)
38 if (corpus as nx_size) == 0 {
39 sys_write(NX_FD_STDOUT, "nx_coq_dir_ingest: cannot read corpus\n" as *u8, 38)
40 return 1
41 }
42 let corpus_n: nx_size = corpus_len_p[0]
43
44 sys_write(NX_FD_STDOUT, "nx_coq_dir_ingest: corpus bytes=" as *u8, 32)
45 print_i64(corpus_n as i64)
46 sys_write(NX_FD_STDOUT, "\n" as *u8, 1)
47
48 let db: *CoqDb = nx_coq_ingest_corpus(corpus, corpus_n as i64)
49 sys_write(NX_FD_STDOUT, "nx_coq_dir_ingest: decls parsed=" as *u8, 32)
50 print_i64(db.n_decls as i64)
51 sys_write(NX_FD_STDOUT, "\n" as *u8, 1)
52
53 let run: *NxIngestRun = nx_ingest_run_new(
54 out_prefix,
55 NX_COQ_DIR_DISK_BUDGET,
56 NX_COQ_DIR_SHARD_BYTES,
57 NX_COQ_DIR_BLOOM_CAPACITY,
58 NX_BLOOM_PROFILE_1PCT,
59 ckpt_path,
60 NX_COQ_DIR_WATCHDOG_MS)
61 if run == (0 as *NxIngestRun) { return 2 }
62
63 let row_buf: *u8 = sys_mmap(NX_BUF_HUGE)
64 let n_emitted: nx_int = nx_coq_stream_offer_all(db, run, row_buf)
65
66 sys_write(NX_FD_STDOUT, "nx_coq_dir_ingest: emitted=" as *u8, 27)
67 print_i64(n_emitted as i64)
68 sys_write(NX_FD_STDOUT, " shards=" as *u8, 8)
69 print_i64(nx_ingest_run_n_shards(run) as i64)
70 sys_write(NX_FD_STDOUT, "\n" as *u8, 1)
71
72 nx_ingest_run_close(run)
73 return 0
74}