code wiki / (root) / nx_lean_ingest.nx

nx_lean_ingest.nx

buildroot/runtime/nx_lean_ingest.nx

11211 B292 linesdepth 5pulls 6 transitivereach 8 importersview sourcekind librarytopic lean

docs dependencies structs consts functions

about

nx_lean_ingest.nx -- ingest Lean 4 theorem STATEMENTS (L0 phase). We do not implement a Lean kernel. Instead we parse the statement-level structure of .lean files (theorem / lemma / def / axiom declarations) and emit them into the QED database with verification_status = TRUSTED_LEAN_KERNEL. L1+ phases add statement-to-card mapping, local-proof cross-check, and reverse export. genealogy_id: de_moura_lean_2013 + lean4_2021 + scholze_liquid_tensor + tao_pfr lineage_id: dependent_type_theory + formal_statement_parsing axioms: NX_AX_ZFC_SEPARATION

dependencies 4 imports · 7 importers

imports: nx_syscalls.nxnx_axioms.nxnx_lex.nxnx_ascii.nx

imported by: nx_corpus_drive.nxnx_five_systems_test.nxnx_ingest_pipeline.nxnx_lean_dir_ingest.nxnx_lean_ingest_test.nxnx_lean_stream_ingest.nxnx_lean_stream_ingest_test.nx

structs

47	struct LeanDecl
56	struct LeanDb

consts

28	const NX_LEAN_TOK_NONE: i64 = 0
29	const NX_LEAN_TOK_THEOREM: i64 = 1
30	const NX_LEAN_TOK_LEMMA: i64 = 2
31	const NX_LEAN_TOK_DEF: i64 = 3
32	const NX_LEAN_TOK_AXIOM: i64 = 4
33	const NX_LEAN_TOK_COLON: i64 = 5
34	const NX_LEAN_TOK_ASSIGN: i64 = 6 // :=
35	const NX_LEAN_TOK_LBRACE: i64 = 7 // { for tactic block
36	const NX_LEAN_TOK_RBRACE: i64 = 8
37	const NX_LEAN_TOK_BY: i64 = 9 // by-block proof
38	const NX_LEAN_TOK_IDENT: i64 = 10
39	const NX_LEAN_TOK_NEWLINE: i64 = 11
40	const NX_LEAN_TOK_COMMENT: i64 = 12
44	const NX_LEAN_MAX_NAME_LEN: i64 = 256
45	const NX_LEAN_MAX_STATEMENT_LEN: i64 = 4096
54	const NX_LEAN_DECL_BYTES: i64 = 32
66	const NX_LEAN_MAX_DECLS: i64 = 262144 // bumped from 65536 to fit full mathlib4 (~194k raw)

functions

68	func nx_lean_db_alloc() -> *LeanDb called by 1: nx_lean_ingest_corpus calls 1: sys_mmap
77	func nx_lean_decl_at(db: LeanDb, i: i64) -> LeanDecl called by 5: drive_lean nx_pipe_run_lean nx_lean_ingest_corpus nx_lean_count_kind nx_lean_stream_offer_all
90	func nx_lean_skip_ws(buf: u8, pos: i64, len: i64) -> i64 called by 1: nx_lean_next_token calls 1: nx_lex_is_ws
127	func nx_lean_next_token(buf: u8, pos: i64, len: i64, out_label: *u8) -> i64 called by 1: nx_lean_ingest_corpus calls 3: nx_lean_skip_ws nx_ascii_is_id_start nx_lex_is_id_cont_qualified
202	func nx_lean_ingest_corpus(buf: u8, len: i64) -> LeanDb called by 6: drive_lean main nx_pipe_run_lean main main main calls 4: nx_lean_db_alloc sys_mmap nx_lean_next_token nx_lean_decl_at
283	func nx_lean_count_kind(db: *LeanDb, kind: i64) -> i64 called by 2: main main calls 1: nx_lean_decl_at