Skip to content

README.md

Latest commit

 

History

History
114 lines (86 loc) · 4.45 KB

README.md

File metadata and controls

114 lines (86 loc) · 4.45 KB

xeus-lean

A Jupyter kernel for Lean 4 based on the xeus framework. Runs both as a native desktop kernel and as a WASM kernel in the browser via JupyterLite.

Features

  • Interactive Lean 4 in Jupyter notebooks — #eval, #check, def, theorem, etc.
  • Environment persistence — definitions carry across cells
  • Two build targets:
    • Native: Lean-owned main loop, C++ xeus via FFI, runs in Jupyter Lab/Notebook
    • WASM: Compiled to WebAssembly via emscripten Memory64, runs in JupyterLite (browser, no server needed)

Quick Start

Pick whichever path matches your setup. Each tutorial is self-contained and copy-pasteable.

Path Time What you get
Browser 1 min JupyterLite at github.io, no install
Docker — native kernel 10 min Local Jupyter with Sparkle (Signal.loop works here, not in WASM)
Docker — WASM build 30 min Reproduce the JupyterLite static site, customize bundled libs
From source — native 30 min Hack on the kernel itself

Stuck? See the troubleshooting guide.

For internals (the 5 WASM bottlenecks, the env-reuse workaround, the per-module zstd tarball pipeline), see WASM_BUILD.md.

Example Session

-- Cell 1: Define a function
def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

-- Cell 2: Evaluate
#eval factorial 10  -- 3628800

-- Cell 3: Type check
#check @List.map  -- {α β : Type} → (α → β) → List α → List β

-- Cell 4: IO actions
#eval IO.println "Hello from Lean!"  -- Hello from Lean!

Architecture

Native

Jupyter Client ──ZMQ──▶ Lean Main (XeusKernel.lean)
                             │ FFI
                        C++ xeus (xeus_ffi.cpp)

Lean owns the main loop, polls for Jupyter messages, and calls the C++ xeus library via FFI.

WASM

Browser ──Web Worker──▶ xlean.js + xlean.wasm
                             │
                        Lean runtime (patched for single-threaded WASM)
                        + Init .olean files (embedded in VFS)

The entire Lean 4 runtime and Init module are compiled to WASM with emscripten Memory64 (-sMEMORY64 for 64-bit pointers matching host .olean format).

Project Structure

xeus-lean/
├── src/
│   ├── XeusKernel.lean              # Native: Lean main loop
│   ├── xeus_ffi.cpp                 # Native: C++ FFI layer
│   ├── xinterpreter_wasm.cpp        # WASM: xeus-lite interpreter
│   ├── main_emscripten_kernel.cpp   # WASM: entry point
│   ├── WasmRepl.lean                # WASM: REPL exports (@[export])
│   ├── REPL/                        # REPL implementation
│   │   └── Frontend.lean            # Message accumulation fix
│   ├── pre.js / post.js             # Emscripten JS hooks
├── cmake/
│   ├── LeanRtWasm.cmake             # Build lean4 runtime for WASM
│   ├── LeanStage0Wasm.cmake         # Build stage0 stdlib for WASM
│   ├── GenerateSymbolTable.cmake    # dlsym replacement for WASM
│   ├── fix_extern_signatures.py     # Auto-fix ABI mismatches
│   └── stubs/                       # Libuv stubs for WASM
├── CMakeLists.txt                   # Dual native/WASM build
├── Makefile                         # WASM build automation
├── lakefile.lean                    # Lake build config
├── pixi.toml                        # Pixi environments (emscripten, jupyterlite)
├── WASM_BUILD.md                    # WASM architecture & bottleneck docs
└── test_wasm_node.cpp               # WASM integration tests

CI/CD

GitHub Actions builds both targets on every push:

  • Native build: Linux x86_64, uploads xlean binary
  • WASM build: emscripten Memory64, runs test_wasm_node, deploys JupyterLite to GitHub Pages

License

Apache License 2.0

Acknowledgments

  • xeus by QuantStack — Jupyter kernel protocol framework
  • Lean 4 REPL by the Lean community — src/REPL/ is based on this project
  • xeus-lite — xeus for JupyterLite/WASM