nx_hol_dir_ingest.nx source
↩ module page · 67 lines · 2381 B
1// nx_hol_dir_ingest.nx -- ingest every HOL Light decl in the corpus
2// at nxc2/_offc/hol_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_hol_ingest.nx"
14import "nx_ingest_runner.nx"
15import "nx_hol_stream_ingest.nx"
16import "nx_bloom_capacity.nx"
17
18const NX_HOL_DIR_DISK_BUDGET: nx_size = 1073741824
19const NX_HOL_DIR_SHARD_BYTES: nx_size = 104857600
20const NX_HOL_DIR_BLOOM_CAPACITY: nx_int = 1000000
21const NX_HOL_DIR_WATCHDOG_MS: nx_int = 60000
22
23func main() -> nx_exit {
24 let corpus_path: *u8 = "nxc2/_offc/hol_corpus.txt" as *u8
25 let out_prefix: *u8 = "/tmp/nx_ingest_hol" as *u8
26 let ckpt_path: *u8 = "/tmp/nx_ingest_hol.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_hol_dir_ingest: cannot read corpus\n" as *u8, 38)
33 return 1
34 }
35 let corpus_n: nx_size = corpus_len_p[0]
36
37 sys_write(NX_FD_STDOUT, "nx_hol_dir_ingest: corpus bytes=" as *u8, 32)
38 print_i64(corpus_n as i64)
39 sys_write(NX_FD_STDOUT, "\n" as *u8, 1)
40
41 let db: *HolDb = nx_hol_ingest_corpus(corpus, corpus_n as i64)
42 sys_write(NX_FD_STDOUT, "nx_hol_dir_ingest: decls parsed=" as *u8, 32)
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_HOL_DIR_DISK_BUDGET,
49 NX_HOL_DIR_SHARD_BYTES,
50 NX_HOL_DIR_BLOOM_CAPACITY,
51 NX_BLOOM_PROFILE_1PCT,
52 ckpt_path,
53 NX_HOL_DIR_WATCHDOG_MS)
54 if run == (0 as *NxIngestRun) { return 2 }
55
56 let row_buf: *u8 = sys_mmap(NX_BUF_HUGE)
57 let n_emitted: nx_int = nx_hol_stream_offer_all(db, run, row_buf)
58
59 sys_write(NX_FD_STDOUT, "nx_hol_dir_ingest: emitted=" as *u8, 27)
60 print_i64(n_emitted as i64)
61 sys_write(NX_FD_STDOUT, " shards=" as *u8, 8)
62 print_i64(nx_ingest_run_n_shards(run) as i64)
63 sys_write(NX_FD_STDOUT, "\n" as *u8, 1)
64
65 nx_ingest_run_close(run)
66 return 0
67}