xlean-mcp + JIT-in-kernel + Real-Time Collaboration#53
Merged
Conversation
Add `xlean-mcp` to the `lake build` line and install it onto
`/usr/local/bin` alongside `xlean` / `xlean-convert`. The source
already ships in xeus-lean (`src/MCPMain.lean` +
`src/XLean/MCP/*.lean`), but the binary wasn't being built, so MCP
hosts (Claude Code, Cursor, the MCP inspector) had no way to drive
the kernel without `lake build`ing inside the running container.
With this in the image, the canonical hookup is
"command": "docker",
"args": ["exec", "-i", "<container>", "xlean-mcp"]
— the stdio JSON-RPC server speaks directly to the host.
Install `jupyter-collaboration` (Y.js / CRDT backend, the official Jupyter RTC extension) and pass `--collaborative` on the `jupyter lab` CMD. Without this, external edits to a `.ipynb` — e.g. the `markdown_to_notebook` MCP tool regenerating a chapter from its `.md` source — only land in the browser after a manual "File changed on disk" reload dialog. With it, Jupyter Server watches the file, computes a CRDT update, and pushes the diff to every connected client, so the cells refresh in place.
Make `Sparkle.Core.JIT.JIT.{load,eval,tick,…}` callable from a
notebook `#eval` cell. Until now any cell that touched the JIT
threw
lean::exception: Could not find native implementation of
external declaration 'Sparkle.Core.JIT.JIT.load' (symbols
'lp_sparkle_..._load___boxed' or 'lp_sparkle_..._load')
inside the kernel. Four interlocking pieces are now in place:
1. Pre-build `c_src/sparkle_jit.c` and `c_src/sparkle_barrier.c`
as static archives via `leanc -c -O2 -fvisibility=default`.
`leanc` defaults to `-fvisibility=hidden`, which would mark
every symbol local; overriding to `default` is what lets
`dlsym(RTLD_DEFAULT, ...)` find them later.
2. Force the `lake build xlean` line to rebuild by `rm -f`'ing
the binary first. Lake's build cache doesn't hash
`moreLinkArgs` or env vars, so without this the prior xlean
from cmake's `buildXlean` script is treated as up-to-date and
the extra archives never reach the link.
3. Pass the archives through `XEUS_LEAN_EXTRA_LIBS` wrapped in
`-Wl,--whole-archive ... -Wl,--no-whole-archive`. Without
whole-archive the linker drops every TU because xlean itself
references nothing in them at static-link time.
4. Pin each FFI entry point with `-Wl,--undefined=<sym>`. Even
with whole-archive the Lean linker tail appends
`-Wl,--gc-sections`, which would otherwise strip the symbols
at output time as unreachable; `--undefined=` marks them as
roots so gc-sections keeps the containing sections.
The end state: `nm --dynamic /usr/local/bin/xlean | grep sparkle_jit_load`
shows `T sparkle_jit_load` (uppercase, in `.dynsym`), and the
interpreter's `dlsym(RTLD_DEFAULT, ...)` lookup at `#eval` time
resolves cleanly.
(There's a companion sparkle `lakefile.lean` change setting
`precompileModules := true` on the Sparkle lib so the Lean-side
`lp_*` wrapper symbols land in a per-module `.so`; the kernel
loads those at boot via `LEAN_DYNLIB_PATH`.)
Make `@[extern]` Sparkle declarations callable from the xeus-lean kernel's `#eval` path. The previous commit (`a15560e`) made the C-level FFI symbols (`sparkle_jit_load`, `sparkle_jit_eval`, …) resolvable via `dlsym` against xlean's own dynsym. That gets us half of the way: at `#eval` time the Lean interpreter actually wants to call the *Lean-side* boxing wrapper `lp_sparkle_Sparkle_Core_JIT_JIT_load___boxed`, not the raw C function, and that wrapper only exists when the surrounding Lean module is compiled to native code (it lives in the `.c.o` Lake emits per module, not in the `.olean`). Two changes pin the wrappers down: - `lakefile.lean`: `precompileModules := true` on the `Sparkle` lean_lib. Lake now produces a per-module shared library (e.g. `sparkle_Sparkle_Core_JIT.so`) alongside each `.olean`, with all the `lp_*` symbols exported. - `docker/tutorial/Dockerfile`: extend the Stage-5 kernelspec patch to set `LEAN_DYNLIB_PATH=<sparkle_Sparkle_Core_JIT.so>`. `XeusKernel.lean` already has a loop that reads this env var and calls `Lean.loadDynlib` on each entry at boot, so the precompiled module's symbols become part of `RTLD_DEFAULT`'s search space. We list only `JIT.so` because the other Sparkle modules cross-reference each other and would need a topo-sorted load order; `JIT.so` is self-contained except for the C-level `sparkle_jit_*` symbols already in xlean's dynsym. After this, `#eval JIT.compileAndLoad "..."` returns a valid handle instead of crashing the kernel with "Could not find native implementation".
Three new tutorial cells that exercise paths the harness now
supports end-to-end inside JupyterLab:
- **Ch03 §3.0 Variant — 4-bit Gray-code counter + JIT sim.**
Introduces the `bin XOR (bin >> 1)` trick as a stepping stone
to the rest of the chapter, then shows the same design driven
through `Sparkle.Core.JIT.JIT.{compileAndLoad,eval,tick,
getOutput,destroy}` so the cell renders the expected Gray
sequence inline. Hits the new `LEAN_DYNLIB_PATH`-driven
`lp_*` resolution path.
- **Ch05 §5.5e Worked example — read Verilog, then prove it.**
Inline `verilog!` macro materialises `nextState` for a one-
register synchronous XOR, then proves three theorems about
it via `simp [nextState] ; bv_decide`. Demonstrates that the
Verilog frontend isn't just for type-checking imported code —
the resulting `State`/`Input`/`nextState` shape is reasonable
to prove against directly.
- **Ch08 §8.2/§8.3 in-notebook Yosys run.** Replaces the
illustrative `lake exe sparkle-emit > /tmp/counter8.sv` line
with a runnable `#writeVerilogDesign` cell, then converts the
`yosys -p '...'` block from a `bash` text block to xeus-lean's
`#bash` magic so the synthesis stat output appears below the
cell with no host-side step.
3 tasks
mark-christiaens
pushed a commit
to mark-christiaens/sparkle
that referenced
this pull request
Jun 24, 2026
PR Verilean#53's `precompileModules := true` on `lean_lib Sparkle` made Lake build `libsparkle_Sparkle.so` alongside the oleans. That .so was linked against the C extern_lib archives (`libsparkle_barrier.a`, `libsparkle_jit.a`) but the linker's default `--as-needed` pass discarded every symbol no Lean wrapper currently *calls* directly — including `sparkle_jit_load`, which the dlsym-loaded `JIT.load` boxing wrapper looks up at run time. Tutorial-notebooks CI consequently broke with: symbol lookup error: .lake/build/lib/libsparkle_Sparkle.so: undefined symbol: sparkle_jit_load while building `Notebooks.Gen.Ch03_Sequential` (the new chapter that exercises JIT.load). Fix: pass `-Wl,--whole-archive` around the two extern archives in `moreLinkArgs`, so the linker retains every symbol from them. The `-L ./.lake/build/c_src` path points at the directory the `extern_lib` blocks emit those archives into. `lake build Sparkle`, `lake build TutorialNotebooks`, and `lake exe svparser-test` (42/0) all succeed locally with this change.
junjihashimoto
added a commit
that referenced
this pull request
Jul 1, 2026
xlean-mcp + JIT-in-kernel + Real-Time Collaboration
junjihashimoto
added a commit
that referenced
this pull request
Jul 1, 2026
PR #53's `precompileModules := true` on `lean_lib Sparkle` made Lake build `libsparkle_Sparkle.so` alongside the oleans. That .so was linked against the C extern_lib archives (`libsparkle_barrier.a`, `libsparkle_jit.a`) but the linker's default `--as-needed` pass discarded every symbol no Lean wrapper currently *calls* directly — including `sparkle_jit_load`, which the dlsym-loaded `JIT.load` boxing wrapper looks up at run time. Tutorial-notebooks CI consequently broke with: symbol lookup error: .lake/build/lib/libsparkle_Sparkle.so: undefined symbol: sparkle_jit_load while building `Notebooks.Gen.Ch03_Sequential` (the new chapter that exercises JIT.load). Fix: pass `-Wl,--whole-archive` around the two extern archives in `moreLinkArgs`, so the linker retains every symbol from them. The `-L ./.lake/build/c_src` path points at the directory the `extern_lib` blocks emit those archives into. `lake build Sparkle`, `lake build TutorialNotebooks`, and `lake exe svparser-test` (42/0) all succeed locally with this change.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
End-to-end enablement of the tutorial Docker image as an MCP-driven Sparkle workspace:
xlean-mcpin the image (11bab79). The stdio MCP binary now ships preinstalled so MCP hosts (Claude Code, Cursor, …) can spawn it viadocker exec -i sparkle xlean-mcpinstead of building inside the container. Depends on MCP server improvements: NDJSON transport + kernel_execute + md⇄ipynb sync xeus-lean#14.51a793e). Installjupyter-collaborationand add--collaborativeto thejupyter labCMD. With this, an external edit to a.ipynb(e.g. the MCP server'smarkdown_to_notebookregenerating Ch03 from its.md) propagates to every open JupyterLab tab via Y.js / CRDT without a manual reload dialog.a15560e). Pre-buildc_src/sparkle_jit.candc_src/sparkle_barrier.cwith-fvisibility=default, force the xlean relink to actually consume them viaXEUS_LEAN_EXTRA_LIBSwrapped in--whole-archive+--undefined=<sym>to defeat the Lean linker tail's-Wl,--gc-sections.nm --dynamic xlean | grep sparkle_jit_loadnow showsT sparkle_jit_loadinstead of empty.b8a6bc7).precompileModules := trueon the Sparkle lean_lib so Lake emits asparkle_Sparkle_Core_JIT.sonext to the olean with alllp_*boxing wrappers; the kernelspec patch setsLEAN_DYNLIB_PATH=to that .so so xlean's existingLean.loadDynlibboot loop picks it up.#eval Sparkle.Core.JIT.JIT.compileAndLoad ...now succeeds in a notebook cell instead of throwing "Could not find native implementation".d069c61) that demonstrate the workflows above are working end-to-end inside JupyterLab:verilog!, prove three theorems aboutnextState#bashTest plan
docker build -t sparkle-tutorial:latest -f docker/tutorial/Dockerfile .succeeds end-to-enddocker run --rm -d --name sparkle -p 8888:8888 sparkle-tutorial:latestand Ch03/Ch05/Ch08 cells execute greennm --dynamic /usr/local/bin/xlean | grep sparkle_jit_loadshowsT sparkle_jit_load#eval Sparkle.Core.JIT.JIT.compileAndLoad "/tmp/foo_jit.cpp"returns a handle (does not throw)markdown_to_notebookfrom xlean-mcp regenerates the Ch03.ipynband the open tab updates without a reload prompt (RTC working)docker exec -i sparkle xlean-mcpspeaks NDJSON andtools/listreturns 9 tools includingkernel_execute/markdown_to_notebookDepends on
XEUS_LEAN_REV=mainclone in the Dockerfile picks up the new MCP surface.Known follow-ups
Sparkle.Backend.CppSimemits a_tmp_loop_body_*variable usage before its assignment for thecircuit do { reg + …; return reg }register pattern, so the JIT sim ofgrayCtr/counter8returns wrong runtime values (the JIT mechanism itself works, the synth output is buggy). Not addressed here — separate PR.