oxilean

Unified facade crate for OxiLean — a Pure Rust interactive theorem prover implementing the Calculus of Inductive Constructions (CiC), inspired by Lean 4.

This crate re-exports all OxiLean library subcrates under a single API surface with feature-gated imports. Zero C/Fortran dependencies.

Architecture

┌──────────────────────────────────────────────────────────┐
│                     oxilean (facade)                     │
├──────────┬──────────┬──────────┬──────────┬──────────────┤
│  parse   │   elab   │   meta   │  codegen │   build-sys  │
├──────────┴──────────┴──────────┴──────────┴──────────────┤
│                      kernel (TCB)                        │
├──────────┬──────────┬──────────┬──────────┬──────────────┤
│ std-lib  │ runtime  │   lint   │   wasm   │  cli (bin)   │
└──────────┴──────────┴──────────┴──────────┴──────────────┘

Crate	Role
`oxilean-kernel`	Trusted computing base — type checker, expressions, declarations (zero external deps)
`oxilean-parse`	Lexer, parser, surface AST
`oxilean-meta`	Metavar WHNF, unification, tactics, type class synthesis, discrimination trees
`oxilean-elab`	Elaborator — surface syntax to kernel terms
`oxilean-std`	Standard library definitions (Nat, Bool, List, mathematics)
`oxilean-codegen`	LCNF compilation and optimization
`oxilean-runtime`	Memory management, closures, I/O, task scheduling
`oxilean-build`	Project compilation, incremental builds, dependency management
`oxilean-lint`	Static analysis and lint rules
`oxilean-wasm`	WebAssembly bindings
`oxilean-cli`	Command-line binary (not re-exported; use directly)

Installation

Add to your Cargo.toml:

[dependencies]
oxilean = "0.1"

Or with all library components:

[dependencies]
oxilean = { version = "0.1", features = ["full"] }

Feature Flags

Feature	Default	Description
`kernel`	yes	Trusted computing base for type checking
`parse`	yes	Concrete syntax → abstract syntax parser
`elab`	yes	Surface syntax → kernel terms elaborator
`meta`	yes	Metavar-aware WHNF, unification, type class synthesis, tactics
`codegen`	no	LCNF-based compilation and optimization
`runtime`	no	Runtime system with GC, closures, and bytecode interpretation
`std-lib`	no	Standard library (Nat, Bool, List, etc.)
`lint`	no	Static analysis and lint rules
`build-sys`	no	Build system with incremental compilation
`wasm`	no	WebAssembly bindings (excluded from `full`)
`full`	no	All components except `wasm`

Usage

Default features (kernel + parse + elab + meta)

use oxilean::kernel::{Environment, TypeChecker, Expr, Name, Level, Declaration};
use oxilean::parse::{Parser, Lexer, Token};
use oxilean::elab::{ElabContext, elaborate_expr, elaborate_decl, TypeInferencer};
use oxilean::meta::{MetaContext, TacticState, InstanceSynthesizer, DiscrTree};

Full feature set

# Cargo.toml
oxilean = { version = "0.1", features = ["full"] }

use oxilean::kernel;
use oxilean::parse;
use oxilean::elab;
use oxilean::meta;
use oxilean::codegen;
use oxilean::runtime;
use oxilean::std_lib;
use oxilean::lint;
use oxilean::build_sys;

Selecting individual components

Include only what you need to minimize compile times:

# Cargo.toml — kernel + standard library only
oxilean = { version = "0.1", default-features = false, features = ["kernel", "std-lib"] }

use oxilean::kernel::{Environment, Expr, Name};
use oxilean::std_lib;

Working with the type checker

use oxilean::kernel::{Environment, TypeChecker};

fn check_definitions(env: &Environment) {
    let tc = TypeChecker::new(env);
    // Type-check expressions against the kernel's CiC rules
    // ...
}

Parsing and elaboration pipeline

use oxilean::parse::Parser;
use oxilean::elab::ElabContext;

fn process_source(source: &str) {
    let parser = Parser::new(source);
    // Parse surface syntax, then elaborate into kernel terms
    // ...
}

Module Reference

All modules are re-exported at the crate root via pub use:

Module	Source Crate	Access
`oxilean::kernel`	`oxilean-kernel`	`use oxilean::kernel;`
`oxilean::parse`	`oxilean-parse`	`use oxilean::parse;`
`oxilean::elab`	`oxilean-elab`	`use oxilean::elab;`
`oxilean::meta`	`oxilean-meta`	`use oxilean::meta;`
`oxilean::codegen`	`oxilean-codegen`	`use oxilean::codegen;`
`oxilean::runtime`	`oxilean-runtime`	`use oxilean::runtime;`
`oxilean::std_lib`	`oxilean-std`	`use oxilean::std_lib;`
`oxilean::lint`	`oxilean-lint`	`use oxilean::lint;`
`oxilean::build_sys`	`oxilean-build`	`use oxilean::build_sys;`
`oxilean::wasm`	`oxilean-wasm`	`use oxilean::wasm;`

CLI Companion

The oxilean-cli crate provides a command-line binary for interactive use:

cargo install oxilean-cli
oxilean check MyProject.lean

oxilean-cli is a standalone binary and is not re-exported through this facade crate.

Related Projects

OxiLean is part of the COOLJAPAN Pure Rust ecosystem:

OxiZ — SMT solver (SAT/SMT reasoning)
Legalis-RS — Legal technology library
SciRS2 — Scientific computing
OxiBLAS — Pure Rust BLAS
OxiFFT — Pure Rust FFT

oxilean 0.1.1