nx_mizar_dir_ingest.nx source
↩ module page · 68 lines · 2460 B
1// nx_mizar_dir_ingest.nx -- ingest every Mizar decl in the corpus
2// at nxc2/_offc/mizar_corpus.txt.
3
4// nx_safety_envelope:
5// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
6// sil_target: SIL1
7// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
8// verdict: NOT_YET_EVALUATED
9
10import "nx_syscalls.nx"
11import "nx_runtime.nx"
12import "nx_tier.nx"
13import "nx_mizar_ingest.nx"
14import "nx_ingest_runner.nx"
15import "nx_mizar_stream_ingest.nx"
16import "nx_bloom_capacity.nx"
17
18const NX_MIZ_DIR_DISK_BUDGET: nx_size = 1073741824
19const NX_MIZ_DIR_SHARD_BYTES: nx_size = 104857600
20const NX_MIZ_DIR_BLOOM_CAPACITY: nx_int = 1000000
21const NX_MIZ_DIR_WATCHDOG_MS: nx_int = 60000
22
23func main() -> nx_exit {
24 let corpus_path: *u8 = "nxc2/_offc/mizar_corpus.txt" as *u8
25 let out_prefix: *u8 = "/tmp/nx_ingest_mizar" as *u8
26 let ckpt_path: *u8 = "/tmp/nx_ingest_mizar.checkpoint" as *u8
27
28 let corpus_len_p: *nx_size = (sys_mmap(NX_SIZEOF_NX_SIZE)) as *nx_size
29 corpus_len_p[0] = 0
30 let corpus: *u8 = sys_read_file(corpus_path, corpus_len_p)
31 if (corpus as nx_size) == 0 {
32 sys_write(NX_FD_STDOUT, "nx_mizar_dir_ingest: cannot read corpus\n" as *u8, 40)
33 return 1
34 }
35 let corpus_n: nx_size = corpus_len_p[0]
36
37 sys_write(NX_FD_STDOUT, "nx_mizar_dir_ingest: corpus bytes=" as *u8, 34)
38 print_i64(corpus_n as i64)
39 sys_write(NX_FD_STDOUT, "\n" as *u8, 1)
40
41 let db: *MizarDb = nx_mizar_ingest_corpus(corpus, corpus_n as i64)
42 sys_write(NX_FD_STDOUT, "nx_mizar_dir_ingest: decls parsed=" as *u8, 34)
43 print_i64(db.n_decls as i64)
44 sys_write(NX_FD_STDOUT, "\n" as *u8, 1)
45
46 let run: *NxIngestRun = nx_ingest_run_new(
47 out_prefix,
48 NX_MIZ_DIR_DISK_BUDGET,
49 NX_MIZ_DIR_SHARD_BYTES,
50 NX_MIZ_DIR_BLOOM_CAPACITY,
51 NX_BLOOM_PROFILE_1PCT,
52 ckpt_path,
53 NX_MIZ_DIR_WATCHDOG_MS)
54 if run == (0 as *NxIngestRun) { return 2 }
55
56 let row_buf: *u8 = sys_mmap(NX_BUF_HUGE)
57 let key_buf: *u8 = sys_mmap(NX_BUF_SMALL)
58 let n_emitted: nx_int = nx_mizar_stream_offer_all(db, run, row_buf, key_buf)
59
60 sys_write(NX_FD_STDOUT, "nx_mizar_dir_ingest: emitted=" as *u8, 29)
61 print_i64(n_emitted as i64)
62 sys_write(NX_FD_STDOUT, " shards=" as *u8, 8)
63 print_i64(nx_ingest_run_n_shards(run) as i64)
64 sys_write(NX_FD_STDOUT, "\n" as *u8, 1)
65
66 nx_ingest_run_close(run)
67 return 0
68}