nx_coq_stream_ingest_test.nx source
↩ module page · 51 lines · 1750 B
1// nx_coq_stream_ingest_test.nx -- Coq parser -> defense stack.
2
3import "nx_syscalls.nx"
4import "nx_tier.nx"
5import "nx_coq_ingest.nx"
6import "nx_ingest_runner.nx"
7import "nx_coq_stream_ingest.nx"
8import "nx_bloom_capacity.nx"
9
10func main() -> nx_exit {
11 let prefix: *u8 = "/tmp/nx_coq_si_t1" as *u8
12 let ckpt: *u8 = "/tmp/nx_coq_si_t1.checkpoint" as *u8
13
14 let corpus: *u8 = sys_mmap(512)
15 var i: nx_int = 0
16 while i < 512 { corpus[i] = 0; i = i + 1 }
17 let src: *u8 = "Theorem add_comm. Lemma helper_lem. Definition foo := 1. Axiom em." as *u8
18 var k: nx_int = 0
19 while src[k] != 0 { corpus[k] = src[k]; k = k + 1 }
20 let corpus_len: nx_int = k
21
22 let db: *CoqDb = nx_coq_ingest_corpus(corpus, corpus_len)
23 if db.n_decls < 1 { return 11 }
24
25 let run: *NxIngestRun = nx_ingest_run_new(
26 prefix,
27 100000 as nx_size, 4096 as nx_size,
28 100, NX_BLOOM_PROFILE_1PCT,
29 ckpt, 60000)
30 if run == (0 as *NxIngestRun) { return 21 }
31
32 let row_buf: *u8 = sys_mmap(512)
33 let n1: nx_int = nx_coq_stream_offer_all(db, run, row_buf)
34 if (n1 as nx_int) != db.n_decls { return 22 }
35 if nx_ingest_run_n_emitted(run) != db.n_decls { return 23 }
36 if nx_ingest_run_n_duplicate(run) != 0 { return 24 }
37
38 let n2: nx_int = nx_coq_stream_offer_all(db, run, row_buf)
39 if n2 != 0 { return 31 }
40 if nx_ingest_run_n_duplicate(run) != db.n_decls { return 32 }
41 if nx_ingest_run_n_emitted(run) != db.n_decls { return 33 }
42
43 if nx_ingest_run_n_shards(run) < 1 { return 41 }
44 if nx_ingest_run_disk_used_bytes(run) < 30 { return 42 }
45
46 nx_ingest_run_close(run)
47 let cp: *NxCheckpoint = nx_checkpoint_open(ckpt)
48 if nx_checkpoint_get(cp) != db.n_decls { return 51 }
49
50 return 0
51}