Skip to content

Commit 950c7d6

Browse files
junjihashimotojunjihashimoto
committed
Update README for native + WASM dual build
1 parent c47a32e commit 950c7d6

File tree

1 file changed

+79
-222
lines changed

1 file changed

+79
-222
lines changed

‎README.md‎

Lines changed: 79 additions & 222 deletions
Original file line numberDiff line numberDiff line change
@@ -1,280 +1,137 @@
11
# xeus-lean
22

3-
A Jupyter kernel for Lean 4 based on the [xeus](https://github.com/jupyter-xeus/xeus) framework.
4-
5-
## Overview
6-
7-
`xeus-lean` is a Jupyter kernel for Lean 4 that enables interactive theorem proving and programming in Jupyter notebooks. Unlike traditional kernel designs, **Lean owns the main event loop** and calls the C++ xeus library via FFI (Foreign Function Interface). This architecture provides clean integration with Lean's runtime while leveraging the robust xeus implementation of the Jupyter protocol.
3+
A Jupyter kernel for [Lean 4](https://lean-lang.org/) based on the [xeus](https://github.com/jupyter-xeus/xeus) framework.
4+
Runs both as a **native desktop kernel** and as a **WASM kernel in the browser** via JupyterLite.
85

96
## Features
107

11-
- **Interactive Lean 4**: Execute Lean code in Jupyter notebooks
12-
- **Environment Persistence**: State is maintained across cells with environment tracking
13-
- **Clean Output**: Info messages display as plain text, errors show detailed JSON
14-
- **IO Support**: Full support for `IO` actions including `IO.println`
15-
- **Error Messages**: Formatted error output with position information
16-
- **Debug Mode**: Optional verbose logging via `XLEAN_DEBUG` environment variable
17-
- **Native Performance**: Direct FFI calls with no subprocess overhead
18-
19-
## Architecture
8+
- **Interactive Lean 4** in Jupyter notebooks — `#eval`, `#check`, `def`, `theorem`, etc.
9+
- **Environment persistence** — definitions carry across cells
10+
- **Two build targets**:
11+
- **Native**: Lean-owned main loop, C++ xeus via FFI, runs in Jupyter Lab/Notebook
12+
- **WASM**: Compiled to WebAssembly via emscripten Memory64, runs in JupyterLite (browser, no server needed)
2013

21-
```
22-
┌─────────────────┐
23-
│ Jupyter Client │
24-
│ (Notebook/Lab) │
25-
└────────┬────────┘
26-
│ Jupyter Protocol (ZMQ)
27-
┌────────▼────────┐
28-
│ Lean Main │ ← Lean owns the event loop
29-
│ (XeusKernel) │
30-
└────────┬────────┘
31-
│ FFI calls
32-
┌────────▼────────┐
33-
│ C++ xeus lib │ ← Static library (libxeus_ffi.a)
34-
│ (xeus_ffi.cpp) │
35-
└────────┬────────┘
36-
│ ZMQ
37-
┌────────▼────────┐
38-
│ xeus framework │
39-
│ (protocol) │
40-
└─────────────────┘
41-
```
14+
## Quick Start
4215

43-
**Key Design**:
44-
- **Lean main loop** (`src/XeusKernel.lean`) polls for messages and executes code
45-
- **C++ FFI layer** (`src/xeus_ffi.cpp`) exposes xeus functionality to Lean
46-
- **REPL integration** (`src/REPL/`) provides command evaluation (from [leanprover-community/repl](https://github.com/leanprover-community/repl))
47-
- **Static linking** bundles everything into single `xlean` executable
16+
### Try in the Browser (WASM)
4817

49-
## Dependencies
18+
Visit the [GitHub Pages deployment](https://verilean.github.io/xeus-lean/) — no installation required.
5019

51-
- **CMake** (>= 3.10)
52-
- **C++17** compiler
53-
- **xeus** (>= 5.0.0)
54-
- **xeus-zmq** (>= 1.0.2)
55-
- **nlohmann_json**
56-
- **Lean 4** toolchain (via elan)
57-
- **Lake** (Lean build tool)
58-
59-
## Building from Source
20+
### Native Build
6021

6122
```bash
62-
# 1. Clone the repository
63-
git clone <repository-url>
64-
cd xeus-lean
65-
66-
# 2. Build C++ dependencies (xeus, xeus-zmq)
67-
./build.sh
23+
# Install Lean 4 via elan
24+
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
6825

69-
# 3. Build xlean kernel
26+
# Build
27+
cmake -S . -B build-cmake
28+
cmake --build build-cmake
7029
lake build xlean
7130

72-
# 4. Install kernel spec (creates Jupyter kernel specification)
73-
# TODO: Add installation script
74-
75-
# 5. Verify installation
76-
jupyter kernelspec list # Should show xlean
31+
# Install kernel spec and launch
32+
lake run installKernel
33+
jupyter lab # Select "Lean 4" kernel
7734
```
7835

79-
## Usage
36+
### WASM Build
8037

81-
### Jupyter Lab
38+
Requires: [nix](https://nixos.org/download/) and [pixi](https://pixi.sh/)
8239

8340
```bash
84-
jupyter lab
85-
# Create a new notebook and select "Lean 4" kernel
41+
# Full pipeline: build + test + JupyterLite site + serve on :8888
42+
make deploy
43+
44+
# Or step-by-step:
45+
make lake # Generate .c files from Lean source
46+
make configure # emcmake cmake
47+
make build # emmake make (xlean + test_wasm_node)
48+
make test # Run WASM tests in Node.js
49+
make deploy # Build JupyterLite site + serve
8650
```
8751

88-
### Jupyter Notebook
89-
90-
```bash
91-
jupyter notebook
92-
# Select "Lean 4" from the kernel menu
93-
```
52+
See [WASM_BUILD.md](WASM_BUILD.md) for architecture details and the 5 key bottlenecks solved.
9453

95-
### Example Session
54+
## Example Session
9655

9756
```lean
98-
# Cell 1: Define a function
57+
-- Cell 1: Define a function
9958
def factorial : Nat → Nat
10059
| 0 => 1
10160
| n + 1 => (n + 1) * factorial n
10261
103-
# Cell 2: Evaluate
104-
#eval factorial 5 -- Output: 120
62+
-- Cell 2: Evaluate
63+
#eval factorial 10 -- 3628800
10564
106-
# Cell 3: IO actions
107-
def main : IO Unit := IO.println "Hello from Lean!"
108-
#eval main -- Output: Hello from Lean!
65+
-- Cell 3: Type check
66+
#check @List.map -- {α β : Type} → (α → β) → List α → List β
10967
110-
# Cell 4: Definitions persist
111-
#eval factorial 10 -- Can use factorial from Cell 1
68+
-- Cell 4: IO actions
69+
#eval IO.println "Hello from Lean!" -- Hello from Lean!
11270
```
11371

114-
## Environment Persistence
115-
116-
The kernel tracks Lean environment IDs across cells:
117-
- Each successful cell execution returns a new environment ID
118-
- Subsequent cells use the previous environment ID
119-
- Definitions, theorems, and imports persist throughout the session
120-
- Errors don't update the environment (retry with same state)
121-
122-
Example:
123-
```lean
124-
# Cell 1
125-
def x := 42 -- env: 0 → 1
126-
127-
# Cell 2
128-
def y := x + 1 -- env: 1 → 2 (x is available)
129-
130-
# Cell 3
131-
#eval y -- env: 2, outputs: 43
132-
```
133-
134-
## Output Formatting
72+
## Architecture
13573

136-
The kernel provides clean output for regular execution:
137-
- **Info messages**: Display as plain text (e.g., `#eval` results)
138-
- **Errors**: Show full JSON with position, severity, and hints
139-
- **Empty results**: No output for pure definitions
74+
### Native
14075

141-
Example:
142-
```lean
143-
#eval IO.println "Hello"
144-
-- Output: Hello
145-
146-
#eval 1 + "string"
147-
-- Output: {
148-
-- "env": 2,
149-
-- "messages": [{
150-
-- "severity": "error",
151-
-- "data": "type mismatch...",
152-
-- ...
153-
-- }]
154-
-- }
15576
```
156-
157-
## Debug Mode
158-
159-
Enable verbose logging with the `XLEAN_DEBUG` environment variable:
160-
161-
```bash
162-
# Normal mode (quiet)
163-
jupyter lab
164-
165-
# Debug mode (verbose logging)
166-
XLEAN_DEBUG=1 jupyter lab
77+
Jupyter Client ──ZMQ──▶ Lean Main (XeusKernel.lean)
78+
│ FFI
79+
C++ xeus (xeus_ffi.cpp)
16780
```
16881

169-
Debug output includes:
170-
- FFI initialization steps
171-
- Message polling and parsing
172-
- Execution flow
173-
- Environment state transitions
174-
- Mutex and memory operations
175-
176-
## Configuration
177-
178-
### Build Configuration
179-
180-
Edit `lakefile.lean` to adjust:
181-
- Link paths for xeus libraries
182-
- Interpreter support flag
183-
- Compiler options
184-
185-
### Runtime Configuration
186-
187-
The kernel uses Jupyter's standard connection file mechanism. Advanced users can:
188-
- Specify custom connection files
189-
- Adjust ZMQ ports
190-
- Configure kernel timeouts
191-
192-
## Known Limitations
193-
194-
1. **REPL Elaborator**: Limited support for infix operators in some contexts
195-
- Use `Nat.add 1 1` instead of `1 + 1` if issues arise
196-
- Import Lean provides more elaborate context
197-
2. **Static Linking Required**: Shared library builds had issues with external class registration
198-
3. **Platform Support**: Currently tested on macOS and Linux
82+
Lean owns the main loop, polls for Jupyter messages, and calls the C++ xeus library via FFI.
19983

200-
## Troubleshooting
84+
### WASM
20185

202-
### Kernel doesn't start
203-
```bash
204-
# Check xlean executable
205-
ls .lake/build/bin/xlean
206-
207-
# Run directly to see errors
208-
./.lake/build/bin/xlean test_connection.json
20986
```
210-
211-
### Static linking errors
212-
```bash
213-
# Rebuild C++ FFI library
214-
cd build-cmake
215-
rm libxeus_ffi.a
216-
cmake --build . --target xeus_ffi
217-
218-
# Rebuild xlean
219-
cd ..
220-
lake clean
221-
lake build xlean
87+
Browser ──Web Worker──▶ xlean.js + xlean.wasm
88+
│
89+
Lean runtime (patched for single-threaded WASM)
90+
+ Init .olean files (embedded in VFS)
22291
```
22392

224-
### Import errors
225-
```bash
226-
# Ensure Lean search path is initialized
227-
# Check lean-toolchain matches your Lean version
228-
cat lean-toolchain
229-
```
93+
The entire Lean 4 runtime and Init module are compiled to WASM with emscripten Memory64
94+
(`-sMEMORY64` for 64-bit pointers matching host `.olean` format).
23095

23196
## Project Structure
23297

23398
```
23499
xeus-lean/
235100
├── src/
236-
│ ├── XeusKernel.lean # Main event loop (Lean owns this)
237-
│ ├── xeus_ffi.cpp # C++ FFI exports to Lean
238-
│ └── REPL/ # Lean REPL implementation
239-
│ # (from github.com/leanprover-community/repl)
240-
├── include/
241-
│ └── xeus_ffi.h # FFI function declarations
242-
├── build-cmake/
243-
│ └── libxeus_ffi.a # Static library (C++ → Lean)
244-
├── lakefile.lean # Lake build configuration
245-
├── CMakeLists.txt # C++ build configuration
246-
└── README.md # This file
101+
│ ├── XeusKernel.lean # Native: Lean main loop
102+
│ ├── xeus_ffi.cpp # Native: C++ FFI layer
103+
│ ├── xinterpreter_wasm.cpp # WASM: xeus-lite interpreter
104+
│ ├── main_emscripten_kernel.cpp # WASM: entry point
105+
│ ├── WasmRepl.lean # WASM: REPL exports (@[export])
106+
│ ├── REPL/ # REPL implementation
107+
│ │ └── Frontend.lean # Message accumulation fix
108+
│ ├── pre.js / post.js # Emscripten JS hooks
109+
├── cmake/
110+
│ ├── LeanRtWasm.cmake # Build lean4 runtime for WASM
111+
│ ├── LeanStage0Wasm.cmake # Build stage0 stdlib for WASM
112+
│ ├── GenerateSymbolTable.cmake # dlsym replacement for WASM
113+
│ ├── fix_extern_signatures.py # Auto-fix ABI mismatches
114+
│ └── stubs/ # Libuv stubs for WASM
115+
├── CMakeLists.txt # Dual native/WASM build
116+
├── Makefile # WASM build automation
117+
├── lakefile.lean # Lake build config
118+
├── pixi.toml # Pixi environments (emscripten, jupyterlite)
119+
├── WASM_BUILD.md # WASM architecture & bottleneck docs
120+
└── test_wasm_node.cpp # WASM integration tests
247121
```
248122

249-
## Comparison with Other Jupyter Kernels
123+
## CI/CD
250124

251-
| Aspect | xeus-python | xeus-lean |
252-
|--------|-------------|-----------|
253-
| Language runtime | Python interpreter | Lean 4 runtime |
254-
| Main loop ownership | C++ xeus | Lean |
255-
| Language integration | Embedded Python | FFI to C++ |
256-
| State management | Python context | Environment IDs |
257-
| Build complexity | Medium | High (FFI + static link) |
125+
GitHub Actions builds both targets on every push:
126+
- **Native build**: Linux x86_64, uploads `xlean` binary
127+
- **WASM build**: emscripten Memory64, runs `test_wasm_node`, deploys JupyterLite to GitHub Pages
258128

259129
## License
260130

261131
Apache License 2.0
262132

263-
## Contributing
264-
265-
Contributions are welcome! Key areas:
266-
- Better error message formatting
267-
- Enhanced completion support
268-
- Rich display for proof goals
269-
- Documentation improvements
270-
271-
See `CONTRIBUTING.md` for development guidelines.
272-
273133
## Acknowledgments
274134

275-
This project builds upon the excellent work of:
276-
277-
- **[xeus](https://github.com/jupyter-xeus/xeus) framework** by QuantStack - provides the robust Jupyter kernel protocol implementation
278-
- **[Lean 4 REPL](https://github.com/leanprover-community/repl)** by the Lean community - the `src/REPL/` directory contains code from this project, which provides the command evaluation and elaboration infrastructure
279-
- **[xeus-zmq](https://github.com/jupyter-xeus/xeus-zmq)** - ZMQ-based messaging implementation for xeus
280-
- Various xeus-based kernel implementations that inspired this architecture
135+
- **[xeus](https://github.com/jupyter-xeus/xeus)** by QuantStack — Jupyter kernel protocol framework
136+
- **[Lean 4 REPL](https://github.com/leanprover-community/repl)** by the Lean community — `src/REPL/` is based on this project
137+
- **[xeus-lite](https://github.com/jupyter-xeus/xeus-lite)** — xeus for JupyterLite/WASM

0 commit comments

Comments
 (0)