diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 506e8eb..faf19e8 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -68,17 +68,6 @@ jobs:
         ls -lh .lake/build/bin/xlean
         file .lake/build/bin/xlean
 
-    - name: Build Sparkle example
-      run: |
-        cd examples/sparkle
-        lake update
-        lake build sparkleDemo
-
-    - name: Run Sparkle example
-      run: |
-        cd examples/sparkle
-        .lake/build/bin/sparkleDemo
-
     - name: Install Jupyter client (for kernel smoke test)
       run: pip install --user --break-system-packages jupyter_client
 
@@ -136,37 +125,26 @@ jobs:
       # to be in the link line for WASM xlean too.
       run: lake build REPL CommBus Display WasmRepl
 
-    - name: Build Sparkle example (lake) — produces IR .cpp files for WASM
+    - name: Build mock-extra fixture (exercises EXTRA_WASM_DIRS contract)
       run: |
-        # WASM xlean target links libsparkle_wasm.a built from
-        # examples/sparkle/.lake/.../*.cpp. Without this step, the link
-        # fails with "symbol exported via --export not found:
-        # sparkle_cache_get / sparkle_eval_at".
-        cd examples/sparkle
-        lake update
-        lake build SparkleDemo || echo "WARN: Sparkle build failed; xlean link may fail"
-
-    - name: Build Hesper WGSL (lake, optional)
-      run: |
-        # Hesper is a git submodule. Phase 0/1 only builds the WGSL DSL
-        # subset (no FFI, no WebGPU, no GLFW). The build wrapper applies
-        # patches under hesper-wasm/patches/ and a stripped lakefile.
-        if [ -f hesper/Hesper.lean ]; then
-          mkdir -p hesper-wasm/build
-          bash hesper-wasm/build-wasm.sh hesper hesper-wasm/build \
-            Hesper.WGSL.DSL Hesper.WGSL.Helpers Hesper.WGSL.Templates \
-            Hesper.WGSL.Shader Hesper.WGSL.Kernel \
-            || echo "WARN: hesper-wasm build failed; Hesper module unavailable"
-          ls -la hesper-wasm/build 2>/dev/null | head -5 || true
-        else
-          echo "Hesper submodule not initialized; skipping"
-        fi
+        # tests/fixtures/mock-extra/ is xeus-lean's reference
+        # implementation of the third-party plug-in contract:
+        # a tiny Lean lib + C extern + manifest.  If this step
+        # fails the contract is broken; downstream libs can't
+        # rely on it.
+        MOCK_STAGING="${RUNNER_TEMP}/mock-extra-staging"
+        mkdir -p "$MOCK_STAGING"
+        pixi run -e wasm-build bash tests/fixtures/mock-extra/build-wasm.sh \
+          "$MOCK_STAGING"
+        ls -lh "$MOCK_STAGING/lib/" "$MOCK_STAGING/MockExtra/" || true
+        echo "EXTRA_WASM_DIRS=${MOCK_STAGING}" >> "$GITHUB_ENV"
 
     - name: Configure WASM build (emcmake)
       run: |
         pixi run -e wasm-build emcmake cmake -S . -B wasm-build \
           -DCMAKE_BUILD_TYPE=Release \
-          -DCMAKE_FIND_ROOT_PATH_MODE_PACKAGE=ON
+          -DCMAKE_FIND_ROOT_PATH_MODE_PACKAGE=ON \
+          -DEXTRA_WASM_DIRS="${EXTRA_WASM_DIRS}"
 
     - name: Build WASM kernel (emmake)
       run: |
@@ -226,11 +204,9 @@ jobs:
           echo "WARNING: olean dir not found at $OLEAN_SRC — skipping"
           exit 0
         fi
-        # Drop a symlink into OLEAN_SRC so the pack script picks up the
-        # Hesper submodule's WGSL oleans alongside Std/Lean/Sparkle.
-        if [ -d hesper-wasm/build/Hesper ]; then
-          ln -sf "$(realpath hesper-wasm/build/Hesper)" "$OLEAN_SRC/Hesper"
-        fi
+        # Third-party olean files are staged into $OLEAN_SRC directly
+        # by CMake (see CMakeLists.txt's EXTRA_WASM_DIRS block) — no
+        # symlink needed any more.
         mkdir -p _olean_packed
         bash scripts/pack-olean-modules.sh "$OLEAN_SRC" _olean_packed ""
         ls -lh _olean_packed/
@@ -364,77 +340,12 @@ jobs:
         path: _output/
         retention-days: 7
 
-  # ============================================================
-  # Native Sparkle Docker image — builds Dockerfile.native-sparkle
-  # end-to-end (xeus-lean kernel + Sparkle on the search path) and
-  # runs the in-image smoke tests. The smoke step inside the
-  # Dockerfile fails the build if the kernel can't start or if
-  # `import Sparkle` doesn't resolve — same gate the local script
-  # uses, just on every push.
-  #
-  # We deliberately don't push the image anywhere from CI; that's a
-  # release concern and needs separate credentials. This job is the
-  # "does main still build the demo image?" check.
-  # ============================================================
-  native-sparkle-docker:
-    runs-on: ubuntu-latest
-    timeout-minutes: 60
-
-    steps:
-    - name: Checkout code
-      uses: actions/checkout@v4
-
-    - name: Free disk space
-      # The full build pulls Sparkle + the Lean toolchain + xeus deps;
-      # GitHub-hosted runners have ~14 GB free, which is tight.
-      run: |
-        sudo rm -rf /usr/share/dotnet /usr/local/lib/android \
-          /opt/ghc /opt/hostedtoolcache/CodeQL || true
-        df -h
-
-    - name: Set up Docker Buildx
-      uses: docker/setup-buildx-action@v3
-
-    - name: Build native-sparkle image
-      uses: docker/build-push-action@v6
-      with:
-        context: .
-        file: Dockerfile.native-sparkle
-        tags: xeus-lean-native-sparkle:ci
-        push: false
-        load: true
-        # Keep the image inside the runner's docker storage; we don't
-        # publish from CI. Cache to GHA cache so PRs don't pay the
-        # full build cost on every run.
-        cache-from: type=gha,scope=native-sparkle
-        cache-to: type=gha,mode=max,scope=native-sparkle
-
-    - name: Verify the image runs and serves a kernel
-      # Independent end-to-end check: start the container, hit the
-      # Jupyter REST API, and confirm the xlean kernel comes up. The
-      # in-image smoke test already covers correctness; this one
-      # covers "the published image actually starts as documented".
-      run: |
-        docker run -d --name xeus-spark -p 18888:8888 xeus-lean-native-sparkle:ci
-        # Give JupyterLab time to bind 8888.
-        for i in $(seq 1 30); do
-          if curl -fsS http://127.0.0.1:18888/api/status >/dev/null 2>&1; then
-            echo "JupyterLab is up"
-            break
-          fi
-          sleep 1
-        done
-        curl -fsS http://127.0.0.1:18888/api/kernelspecs | python3 -c \
-          "import sys,json; d=json.load(sys.stdin); assert 'xlean' in d['kernelspecs'], d; print('xlean kernelspec OK')"
-        docker logs xeus-spark | tail -40
-        docker stop xeus-spark
-
   # ============================================================
   # Publish ghcr.io/<owner>/xeus-lean base image (main branch only).
   #
-  # Downstream projects (Sparkle, Hesper, ...) FROM this image and
-  # build their own Dockerfile that lake-builds their lib + relinks
-  # xlean via XEUS_LEAN_EXTRA_LIBS. This keeps xeus-lean free of any
+  # Downstream projects FROM this image and build their own
+  # Dockerfile that lake-builds their lib + relinks xlean via
+  # XEUS_LEAN_EXTRA_LIBS.  This keeps xeus-lean free of any
   # project-specific build dependency while still giving downstream
   # users a one-line `FROM` to consume.
   # ============================================================
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 0ff9880..6daa5ea 100644
--- a/.github/workflows/docs.yml
+++ b/.github/workflows/docs.yml
@@ -63,9 +63,6 @@ jobs:
             - 'lean-toolchain'
             - 'pixi.toml'
             - 'pixi.lock'
-            - 'examples/sparkle/**'
-            - 'hesper/**'
-            - 'hesper-wasm/**'
             - 'scripts/**'
             - 'Dockerfile.docs-builder'
             - '.github/workflows/docs.yml'
diff --git a/.gitmodules b/.gitmodules
deleted file mode 100644
index b156d3d..0000000
--- a/.gitmodules
+++ /dev/null
@@ -1,3 +0,0 @@
-[submodule "hesper"]
-	path = hesper
-	url = https://github.com/Verilean/hesper.git
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5d53f40..0b6bf7d 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -148,170 +148,96 @@ if(EMSCRIPTEN)
 
     # xlean WASM executable
     # ======================
-
-    # Sparkle C FFI implementations + Lean-compiled IR sources.
-    # Needed for Signal.sample / Signal.circuit in the WASM REPL.
-    # The Lean interpreter looks up `@[extern]` decls by their mangled
-    # `lp_sparkle___private_...___boxed` name, which lives in the .c
-    # files Lean generated under .lake/build/ir/. We copy all sources
-    # to the build dir with a .cpp extension so CMake's C++17 flag
-    # doesn't reject a .c file. To prevent wasm-ld DCE from stripping
-    # these symbols (nothing in main references them; the interpreter
-    # resolves them dynamically), we wrap them in a static archive
-    # and link with --whole-archive.
-    set(SPARKLE_ROOT "${CMAKE_SOURCE_DIR}/examples/sparkle/.lake/packages/sparkle")
-    set(SPARKLE_C_BARRIER "${SPARKLE_ROOT}/c_src/sparkle_barrier.c")
-    set(SPARKLE_IR_DIR "${SPARKLE_ROOT}/.lake/build/ir")
-    set(SPARKLE_WASM_SOURCES)
-    if(EXISTS "${SPARKLE_C_BARRIER}")
-        # Wrap in extern "C" so the C++ compiler does not name-mangle
-        # sparkle_cache_get / sparkle_eval_at. The callers (Signal.c)
-        # reference them as plain C symbols.
-        file(READ "${SPARKLE_C_BARRIER}" _barrier_body)
-        # #include must stay outside extern "C" (lean.h pulls in C++
-        # headers that must have C++ linkage). Strip the original
-        # #include lines and emit them before the extern "C" block.
-        string(REGEX MATCHALL "#include[^\n]*\n" _barrier_includes "${_barrier_body}")
-        string(REGEX REPLACE "#include[^\n]*\n" "" _barrier_body_no_inc "${_barrier_body}")
-        string(JOIN "" _barrier_inc_str ${_barrier_includes})
-        # WASM debug: rename the upstream functions to *_impl so we can
-        # wrap them with call-counter logging that prints to stderr.
-        # Useful for diagnosing simulation hangs in the WASM REPL.
-        string(REPLACE "sparkle_cache_get" "sparkle_cache_get_impl" _barrier_body_no_inc "${_barrier_body_no_inc}")
-        string(REPLACE "sparkle_eval_at" "sparkle_eval_at_impl" _barrier_body_no_inc "${_barrier_body_no_inc}")
-        set(SPARKLE_C_CPP "${CMAKE_BINARY_DIR}/sparkle_barrier.cpp")
-        file(WRITE "${SPARKLE_C_CPP}"
-"${_barrier_inc_str}
-#include <cstdio>
-extern \"C\" {
-${_barrier_body_no_inc}
-
-// Wrappers that print every Nth call to stderr — surfaces in the
-// browser console as `[sparkle_eval_at] call #...`.
-LEAN_EXPORT lean_obj_res sparkle_cache_get(b_lean_obj_arg ref, b_lean_obj_arg t_obj, lean_obj_arg fallback) {
-    static unsigned long n = 0;
-    if ((++n & 0xFFF) == 1) std::fprintf(stderr, \"[sparkle_cache_get] call #%lu\\n\", n);
-    return sparkle_cache_get_impl(ref, t_obj, fallback);
-}
-LEAN_EXPORT lean_obj_res sparkle_eval_at(b_lean_obj_arg signal_val, b_lean_obj_arg t, lean_obj_arg world) {
-    static unsigned long n = 0;
-    if ((++n & 0x3F) == 1) std::fprintf(stderr, \"[sparkle_eval_at] call #%lu (t=%lu)\\n\", n, lean_unbox(t));
-    return sparkle_eval_at_impl(signal_val, t, world);
-}
-}
-")
-        list(APPEND SPARKLE_WASM_SOURCES "${SPARKLE_C_CPP}")
-        message(STATUS "Including sparkle_barrier.cpp + diagnostic wrappers in xlean for WASM FFI")
-    endif()
-    set(_excluded_init_syms "")
-    if(EXISTS "${SPARKLE_IR_DIR}")
-        file(GLOB_RECURSE _SPARKLE_IR_C RELATIVE "${SPARKLE_IR_DIR}"
-             "${SPARKLE_IR_DIR}/*.c")
-        # Exclude every IR file that references sparkle_jit_* — those
-        # symbols live in sparkle_jit.c which has mismatched signatures
-        # vs the IR's view. Stubs for their `initialize_sparkle_*`
-        # entry points are provided below.
-        set(_filtered "")
-        foreach(_rel ${_SPARKLE_IR_C})
-            file(STRINGS "${SPARKLE_IR_DIR}/${_rel}" _jit_refs REGEX "sparkle_jit_")
-            if(_jit_refs)
-                # Derive the module name from path so we can stub init.
-                string(REGEX REPLACE "\\.c$" "" _mod "${_rel}")
-                string(REPLACE "/" "_" _mod "${_mod}")
-                list(APPEND _excluded_init_syms "${_mod}")
-            else()
-                list(APPEND _filtered "${_rel}")
-            endif()
-        endforeach()
-        set(_SPARKLE_IR_C ${_filtered})
-        foreach(_rel ${_SPARKLE_IR_C})
-            string(REPLACE "/" "_" _flat "${_rel}")
-            string(REGEX REPLACE "\\.c$" ".cpp" _flat "${_flat}")
-            set(_dst "${CMAKE_BINARY_DIR}/sparkle_ir_${_flat}")
-            configure_file("${SPARKLE_IR_DIR}/${_rel}" "${_dst}" COPYONLY)
-            list(APPEND SPARKLE_WASM_SOURCES "${_dst}")
-        endforeach()
-        list(LENGTH _SPARKLE_IR_C _n_ir)
-        message(STATUS "Including ${_n_ir} Sparkle IR .cpp files in xlean for WASM FFI")
-    endif()
-    # Stub initialize_sparkle_* for every IR file we excluded above,
-    # so Sparkle.cpp's module-init sequence still links.
-    set(SPARKLE_JIT_STUB "${CMAKE_BINARY_DIR}/sparkle_jit_stubs.cpp")
-    set(_init_stub_decls "")
-    foreach(_mod ${_excluded_init_syms})
-        set(_init_stub_decls "${_init_stub_decls}INIT_STUB(${_mod})\n")
-    endforeach()
-    file(WRITE "${SPARKLE_JIT_STUB}"
-"#include <lean/lean.h>
-extern \"C\" {
-// The Lean 4.28 IR calls module init with a single uint8_t (builtin flag).
-// Older Lean/sparkle_jit.c used (uint8_t, lean_object*); match the IR.
-#define INIT_STUB(mod) LEAN_EXPORT lean_object* initialize_sparkle_##mod(uint8_t builtin) { return lean_io_result_mk_ok(lean_box(0)); }
-${_init_stub_decls}}
-")
-    list(APPEND SPARKLE_WASM_SOURCES "${SPARKLE_JIT_STUB}")
-    list(LENGTH _excluded_init_syms _n_stubs)
-    message(STATUS "Including sparkle_jit_stubs.cpp (${_n_stubs} init stubs)")
-    if(SPARKLE_WASM_SOURCES)
-        add_library(sparkle_wasm STATIC ${SPARKLE_WASM_SOURCES})
-        target_compile_options(sparkle_wasm PRIVATE -fPIC -g2)
-        target_compile_features(sparkle_wasm PRIVATE cxx_std_17)
-        target_include_directories(sparkle_wasm PRIVATE ${LEAN4_INCLUDE_DIR})
-        set_property(TARGET sparkle_wasm PROPERTY POSITION_INDEPENDENT_CODE ON)
-    endif()
     add_executable(xlean src/main_emscripten_kernel.cpp)
     target_link_libraries(xlean PRIVATE xeus-lite)
     target_link_libraries(xlean PRIVATE xeus-lean-static)
-    # Force-link the entire Sparkle archive so wasm-ld does not strip
-    # the dynamically-resolved `lp_sparkle_*` symbols.
-    # --whole-archive alone is not enough: wasm-ld still gc-sections
-    # unreferenced symbols. --export-dynamic + --no-gc-sections keeps
-    # them in the final wasm so the Lean interpreter's dlsym() works.
-    if(TARGET sparkle_wasm)
-        # Extract LEAN_EXPORT symbol names from the generated IR .cpp
-        # files at configure time and pass them to emcc as
-        # EXPORTED_FUNCTIONS. wasm-ld LTO drops symbols nothing
-        # references; the only reliable way to keep interpreter-
-        # resolved symbols in the final wasm is to name them.
-        set(_sparkle_syms "")
-        foreach(_src ${SPARKLE_WASM_SOURCES})
-            # Skip the stubs file so we don't pick up the macro
-            # parameter `name` as a symbol.
-            if(_src MATCHES "sparkle_jit_stubs\\.cpp$")
-                continue()
-            endif()
-            file(STRINGS "${_src}" _hits REGEX "LEAN_EXPORT[^(]*[ *]([a-zA-Z_][a-zA-Z_0-9]*)\\(")
-            foreach(_l ${_hits})
-                if(_l MATCHES "LEAN_EXPORT[^(]*[ *]([a-zA-Z_][a-zA-Z_0-9]*)\\(")
-                    list(APPEND _sparkle_syms "_${CMAKE_MATCH_1}")
-                endif()
-            endforeach()
-        endforeach()
-        # Always include the C FFI entry points used by Sparkle IR.
-        list(APPEND _sparkle_syms "_sparkle_cache_get" "_sparkle_eval_at")
-        list(REMOVE_DUPLICATES _sparkle_syms)
-        list(LENGTH _sparkle_syms _n_syms)
-        message(STATUS "Sparkle exports: ${_n_syms} symbols will be kept")
-        list(JOIN _sparkle_syms "," _sparkle_csv)
-        set(_sparkle_exports_file "${CMAKE_BINARY_DIR}/sparkle_exports.txt")
-        # No _main — this executable uses EMSCRIPTEN_BINDINGS and
-        # emscripten provides its own entry stub. Listing _main here
-        # triggers "undefined exported symbol" since the user code
-        # never defines it.
-        # Also export _xlean_poll_load_progress so the JS-side setTimeout
-        # in the %load magic can call it as Module._xlean_poll_load_progress.
-        # We schedule the poll through JS instead of
-        # emscripten_async_call because the latter's `void* arg`
-        # wrapper crashes under -sMEMORY64=1.
-        file(WRITE "${_sparkle_exports_file}"
-             "[${_sparkle_csv},_xlean_poll_load_progress]")
-        # LINK_FLAGS does NOT evaluate generator expressions, so use
-        # the concrete archive path instead of $<TARGET_FILE:...>.
-        set(_sparkle_archive "${CMAKE_BINARY_DIR}/libsparkle_wasm.a")
+
+    # Always-on exports: symbols that the JS side calls back into wasm
+    # for housekeeping (poll the %load progress queue, etc.).  Without
+    # them wasm-ld's LTO would garbage-collect the function because the
+    # C++ side never references it.
+    #
+    # Downstream third-party libs add their own exports through the
+    # EXTRA_WASM_DIRS path below.
+    set(_xlean_core_exports "_xlean_poll_load_progress")
+    set(_xlean_core_exports_file "${CMAKE_BINARY_DIR}/xlean_core_exports.txt")
+    file(WRITE "${_xlean_core_exports_file}" "[${_xlean_core_exports}]")
+    set_property(TARGET xlean APPEND_STRING PROPERTY LINK_FLAGS
+        " -sEXPORTED_FUNCTIONS=@${_xlean_core_exports_file}")
+    # ========================================================================
+    # Third-party static libraries (optional) — wired via -DEXTRA_WASM_DIRS
+    # ========================================================================
+    # Generic plug-in point for downstream Lean libraries to attach
+    # their WASM artefacts (static archive + C extern exports + olean
+    # tree) to the xlean build.  xeus-lean knows none of their names;
+    # everything is data-driven from each staging directory's manifest.
+    #
+    # Manifest schema (`<staging>/xeus-lean-extra.json`):
+    #
+    #   {
+    #     "archive":    "lib/libNAME_wasm.a",   // whole-archived into xlean
+    #     "exports":    "lib/NAME_exports.txt", // splatted into EXPORTED_FUNCTIONS
+    #     "olean_root": "TopLevelModule"        // optional, copied to /lib/lean/
+    #   }
+    #
+    # See README.md (`## Extending the kernel with your own Lean lib`)
+    # and `tests/fixtures/mock-extra/` for a worked example.
+
+    set(_extra_olean_specs "")     # filled in below, consumed by the
+                                   # olean stage near LEAN_OLEAN_SRC.
+    set(_extra_archive_paths "")   # also filled in below; consumed by
+                                   # the symbol-table generator and the
+                                   # test_wasm_node link further down.
+    foreach(_extra_dir IN LISTS EXTRA_WASM_DIRS)
+        set(_manifest "${_extra_dir}/xeus-lean-extra.json")
+        if(NOT EXISTS "${_manifest}")
+            message(FATAL_ERROR
+                "EXTRA_WASM_DIRS entry ${_extra_dir} is missing xeus-lean-extra.json.\n"
+                "Expected schema:\n"
+                "  { \"archive\": \"lib/libNAME_wasm.a\",\n"
+                "    \"exports\": \"lib/NAME_exports.txt\",\n"
+                "    \"olean_root\": \"TopLevelModule\" }")
+        endif()
+        file(READ "${_manifest}" _meta)
+        string(JSON _rel_archive   GET "${_meta}" archive)
+        string(JSON _rel_exports   GET "${_meta}" exports)
+        # `olean_root` is optional — a pure C library (no Lean side) can
+        # omit it.  string(JSON) errors fatally on a missing key, so probe
+        # first via the "MEMBER" query.
+        string(JSON _olean_root ERROR_VARIABLE _err GET "${_meta}" olean_root)
+        if(_err)
+            set(_olean_root "")
+        endif()
+
+        set(_archive "${_extra_dir}/${_rel_archive}")
+        set(_exports "${_extra_dir}/${_rel_exports}")
+        if(NOT EXISTS "${_archive}")
+            message(FATAL_ERROR "EXTRA_WASM_DIRS: ${_archive} is missing — rerun the third-party build script")
+        endif()
+        if(NOT EXISTS "${_exports}")
+            message(FATAL_ERROR "EXTRA_WASM_DIRS: ${_exports} is missing — rerun the third-party build script")
+        endif()
+
+        file(STRINGS "${_exports}" _syms)
+        list(LENGTH _syms _n_syms)
+        list(JOIN _syms "," _csv)
+        get_filename_component(_exports_stem "${_exports}" NAME_WE)
+        set(_exports_emcc "${CMAKE_BINARY_DIR}/${_exports_stem}_emcc.txt")
+        file(WRITE "${_exports_emcc}" "[${_csv}]")
+        message(STATUS "EXTRA_WASM_DIRS: linking ${_archive} (${_n_syms} symbols, "
+                "manifest=${_manifest})")
         set_property(TARGET xlean APPEND_STRING PROPERTY LINK_FLAGS
-            " -Wl,--whole-archive ${_sparkle_archive} -Wl,--no-whole-archive -sEXPORTED_FUNCTIONS=@${_sparkle_exports_file}")
-        add_dependencies(xlean sparkle_wasm)
-    endif()
+            " -Wl,--whole-archive ${_archive} -Wl,--no-whole-archive -sEXPORTED_FUNCTIONS=@${_exports_emcc}")
+        list(APPEND _extra_archive_paths "${_archive}")
+
+        if(_olean_root)
+            # Defer the olean copy until the LEAN_OLEAN_SRC block sets up
+            # OLEAN_ASSETS_DIR.  Encode "<dir>|<root>" so a single foreach
+            # later can dispatch.
+            list(APPEND _extra_olean_specs "${_extra_dir}|${_olean_root}")
+        endif()
+    endforeach()
+
     # Link stage0 libraries (order matters: REPL -> Lean -> Std -> Init -> leanrt)
     target_link_libraries(xlean PRIVATE
         ${STAGE0_REPL_LIB}
@@ -377,8 +303,8 @@ ${_init_stub_decls}}
         # as fire-and-forget JS (the cell's stdout shows progress)
         # and returns immediately.  Users wait, then run the next
         # cell once the log says the bundle is ready.
-        # EXPORT_ALL=1 did not retain Sparkle IR symbols; we use
-        # --whole-archive below on sparkle_wasm instead.
+        # EXPORT_ALL=1 did not retain third-party IR symbols; we use
+        # --whole-archive on EXTRA_WASM_DIRS archives instead.
     )
 
     target_link_options(xlean
@@ -424,7 +350,7 @@ ${_init_stub_decls}}
             # blew the WASM binary up to ~480MB, all of which the
             # browser had to decode and keep in Linear Memory for
             # every notebook.  Now we ship Init as a tarball
-            # alongside Std/Lean/Sparkle (see OLEAN_ASSETS_DIR
+            # alongside Std/Lean + EXTRA_WASM_DIRS (see OLEAN_ASSETS_DIR
             # below); post.js fetches and unpacks it in preRun,
             # which blocks WASM main() until /lib/lean/Init/ is
             # populated, so the runtime sees the same VFS layout
@@ -440,7 +366,7 @@ ${_init_stub_decls}}
 
             # Embed Display + CommBus (small + always-imported) via
             # --embed-file (baked into the WASM binary).  Std / Lean /
-            # Init / Sparkle / Hesper are dynamic-load (tarballs).
+            # Init + EXTRA_WASM_DIRS olean trees are dynamic-load (tarballs).
             set(LEAN_OLEAN_STAGING_ROOT "${CMAKE_BINARY_DIR}/olean_staging")
             target_link_options(xlean
                 PUBLIC "SHELL: --embed-file ${LEAN_OLEAN_STAGING_ROOT}@/")
@@ -531,7 +457,7 @@ ${_init_stub_decls}}
             # CommBus is imported by Display, so its olean must be in the
             # VFS too — otherwise `import Display` fails at the header
             # stage with "unknown module prefix 'CommBus'", which then
-            # cascades into Init/Std/Lean/Sparkle being skipped and the
+            # cascades into Init/Std/Lean being skipped and the
             # cell crashing on basic identifiers like `IO.println`.
             set(DISPLAY_OLEAN_SRC "${CMAKE_SOURCE_DIR}/.lake/build/lib/lean")
             foreach(_mod Display CommBus)
@@ -542,30 +468,76 @@ ${_init_stub_decls}}
                     endif()
                 endforeach()
             endforeach()
-            # Copy Sparkle .olean to assets (dynamic load, not embed)
-            set(SPARKLE_OLEAN_SRC "${CMAKE_SOURCE_DIR}/examples/sparkle/.lake/packages/sparkle/.lake/build/lib/lean")
-            if(IS_DIRECTORY "${SPARKLE_OLEAN_SRC}/Sparkle")
+            # Third-party Lean libraries are pulled
+            # in via EXTRA_WASM_DIRS — see the _extra_olean_specs loop
+            # below.  xeus-lean itself stages only the Lean toolchain
+            # oleans (Init/Std/Lean) and Display.
+
+            # Stage third-party olean trees declared via EXTRA_WASM_DIRS.
+            # Each spec is "<dir>|<olean_root>" — copy
+            # <dir>/<root>{,/**}.{olean,olean.private,olean.server,ir,ilean}
+            # into ${OLEAN_ASSETS_DIR}.  Same shape as the toolchain branch
+            # above; the loop has zero hard-coded module names.
+            foreach(_spec IN LISTS _extra_olean_specs)
+                string(REPLACE "|" ";" _parts "${_spec}")
+                list(GET _parts 0 _src_dir)
+                list(GET _parts 1 _root)
+                # A lib may ship as a single umbrella olean
+                # (`<src_dir>/<root>.olean` only, no sub-tree) or as
+                # an umbrella + tree.  Accept either; only warn if
+                # both the umbrella and the tree are missing.
+                set(_has_umbrella FALSE)
+                if(EXISTS "${_src_dir}/${_root}.olean")
+                    set(_has_umbrella TRUE)
+                endif()
+                set(_has_tree FALSE)
+                if(IS_DIRECTORY "${_src_dir}/${_root}")
+                    set(_has_tree TRUE)
+                endif()
+                if(NOT _has_umbrella AND NOT _has_tree)
+                    message(WARNING
+                        "EXTRA_WASM_DIRS: ${_src_dir} declared olean_root="
+                        "${_root} but neither ${_src_dir}/${_root}.olean "
+                        "nor ${_src_dir}/${_root}/ exists — skipping")
+                    continue()
+                endif()
                 foreach(_ext olean olean.private)
-                    if(EXISTS "${SPARKLE_OLEAN_SRC}/Sparkle.${_ext}")
-                        file(COPY "${SPARKLE_OLEAN_SRC}/Sparkle.${_ext}" DESTINATION "${OLEAN_ASSETS_DIR}/")
+                    if(EXISTS "${_src_dir}/${_root}.${_ext}")
+                        file(COPY "${_src_dir}/${_root}.${_ext}"
+                             DESTINATION "${OLEAN_ASSETS_DIR}/")
                     endif()
                 endforeach()
-                file(GLOB_RECURSE _SPARKLE_FILES RELATIVE "${SPARKLE_OLEAN_SRC}"
-                    "${SPARKLE_OLEAN_SRC}/Sparkle/*.olean"
-                    "${SPARKLE_OLEAN_SRC}/Sparkle/*.olean.server"
-                    "${SPARKLE_OLEAN_SRC}/Sparkle/*.olean.private"
-                    "${SPARKLE_OLEAN_SRC}/Sparkle/*.ir"
-                    "${SPARKLE_OLEAN_SRC}/Sparkle/*.ilean")
-                list(LENGTH _SPARKLE_FILES _sparkle_count)
-                foreach(_f ${_SPARKLE_FILES})
-                    get_filename_component(_dir "${_f}" DIRECTORY)
-                    file(MAKE_DIRECTORY "${OLEAN_ASSETS_DIR}/${_dir}")
-                    file(COPY "${SPARKLE_OLEAN_SRC}/${_f}" DESTINATION "${OLEAN_ASSETS_DIR}/${_dir}/")
-                endforeach()
-                message(STATUS "Sparkle: ${_sparkle_count} files → olean_assets (dynamic load)")
-            else()
-                message(STATUS "Sparkle .olean not found")
-            endif()
+                set(_extra_count 0)
+                if(_has_tree)
+                    file(GLOB_RECURSE _EXTRA_FILES RELATIVE "${_src_dir}"
+                        "${_src_dir}/${_root}/*.olean"
+                        "${_src_dir}/${_root}/*.olean.server"
+                        "${_src_dir}/${_root}/*.olean.private"
+                        "${_src_dir}/${_root}/*.ir"
+                        "${_src_dir}/${_root}/*.ilean")
+                    list(LENGTH _EXTRA_FILES _extra_count)
+                    foreach(_f ${_EXTRA_FILES})
+                        get_filename_component(_dir "${_f}" DIRECTORY)
+                        file(MAKE_DIRECTORY "${OLEAN_ASSETS_DIR}/${_dir}")
+                        file(COPY "${_src_dir}/${_f}" DESTINATION "${OLEAN_ASSETS_DIR}/${_dir}/")
+                    endforeach()
+                endif()
+                # Stage the .xeus-auto-imports registry if the
+                # third-party staging dir shipped one.  Lives at the
+                # OLEAN_ASSETS_DIR root so xlean's REPL scanner picks
+                # it up alongside the toolchain auto-imports.
+                # Multiple EXTRA_WASM_DIRS entries can each ship one;
+                # we append each to a single file rather than
+                # overwriting.
+                if(EXISTS "${_src_dir}/.xeus-auto-imports")
+                    file(READ "${_src_dir}/.xeus-auto-imports" _ai_body)
+                    file(APPEND "${OLEAN_ASSETS_DIR}/.xeus-auto-imports"
+                                "# from EXTRA_WASM_DIRS=${_src_dir}\n${_ai_body}\n")
+                    message(STATUS "EXTRA_WASM_DIRS: ${_root}: merged .xeus-auto-imports")
+                endif()
+                message(STATUS "EXTRA_WASM_DIRS: ${_root}: ${_extra_count} files → olean_assets"
+                              " (umbrella=${_has_umbrella} tree=${_has_tree})")
+            endforeach()
 
             # Generate manifest.json listing all .olean asset files
             file(GLOB_RECURSE _ALL_ASSET_FILES
@@ -615,9 +587,11 @@ ${_init_stub_decls}}
         ${STAGE0_LEAN_LIB}
         ${STAGE0_REPL_LIB}
     )
-    if(TARGET sparkle_wasm)
-        list(APPEND _symtab_libs sparkle_wasm)
-    endif()
+    # Add every archive contributed via EXTRA_WASM_DIRS so its Lean
+    # externs end up in the dlsym lookup table too.
+    foreach(_extra_archive_path IN LISTS _extra_archive_paths)
+        list(APPEND _symtab_libs "${_extra_archive_path}")
+    endforeach()
     generate_wasm_symbol_table(${WASM_SYMTAB_FILE} ${_symtab_libs})
 
     # Add symbol table to xlean (generated above)
@@ -635,14 +609,14 @@ ${_init_stub_decls}}
         ${STAGE0_INIT_LIB}
         ${LEANRT_LIB}
     )
-    if(TARGET sparkle_wasm)
-        # wasm_symbol_table.cpp references initialize_sparkle_* — needs
-        # the Sparkle archive to resolve those symbols.
+    # wasm_symbol_table.cpp references symbols from each
+    # EXTRA_WASM_DIRS archive — pull them in via whole-archive so
+    # the references resolve at link time.
+    foreach(_extra_archive_path IN LISTS _extra_archive_paths)
         target_link_options(test_wasm_node PRIVATE
-            "SHELL: -Wl,--whole-archive ${CMAKE_BINARY_DIR}/libsparkle_wasm.a -Wl,--no-whole-archive"
+            "SHELL: -Wl,--whole-archive ${_extra_archive_path} -Wl,--no-whole-archive"
         )
-        add_dependencies(test_wasm_node sparkle_wasm)
-    endif()
+    endforeach()
     target_compile_options(test_wasm_node PRIVATE -fPIC -g2)
     target_link_options(test_wasm_node PRIVATE
         "SHELL: -fwasm-exceptions"
@@ -661,8 +635,10 @@ ${_init_stub_decls}}
         "SHELL: -sEXPORT_ALL=1"
         "SHELL: --profiling-funcs"
     )
-    # test_wasm_node only needs Init .olean files (not Std/Lean/Sparkle).
-    # Create a minimal staging with Init only to keep the binary small.
+    # test_wasm_node only needs Init .olean files (not Std/Lean) plus
+    # whatever EXTRA_WASM_DIRS contributed so the mock-extra fixture
+    # (and any future plug-in test) can resolve `import MockExtra`
+    # against its embedded VFS.
     if(LEAN_TOOLCHAIN_DIR AND EXISTS "${LEAN_OLEAN_SRC}/Init.olean")
         set(TEST_OLEAN_STAGING "${CMAKE_BINARY_DIR}/test_olean_staging/lib/lean")
         file(MAKE_DIRECTORY "${TEST_OLEAN_STAGING}")
@@ -676,6 +652,30 @@ ${_init_stub_decls}}
         if(_cp_rc)
             message(WARNING "Init staging copy failed: rc=${_cp_rc}")
         endif()
+        # Stage every EXTRA_WASM_DIRS olean root + its
+        # .xeus-auto-imports into the same test VFS, mirroring what
+        # xlean does for the deploy target.
+        foreach(_spec IN LISTS _extra_olean_specs)
+            string(REPLACE "|" ";" _parts "${_spec}")
+            list(GET _parts 0 _src_dir)
+            list(GET _parts 1 _root)
+            foreach(_ext olean olean.server olean.private ir ilean)
+                if(EXISTS "${_src_dir}/${_root}.${_ext}")
+                    file(COPY "${_src_dir}/${_root}.${_ext}"
+                         DESTINATION "${TEST_OLEAN_STAGING}/")
+                endif()
+            endforeach()
+            if(IS_DIRECTORY "${_src_dir}/${_root}")
+                file(COPY "${_src_dir}/${_root}"
+                     DESTINATION "${TEST_OLEAN_STAGING}/")
+            endif()
+            if(EXISTS "${_src_dir}/.xeus-auto-imports")
+                file(READ "${_src_dir}/.xeus-auto-imports" _ai_body)
+                file(APPEND "${TEST_OLEAN_STAGING}/.xeus-auto-imports"
+                            "# from EXTRA_WASM_DIRS=${_src_dir}\n${_ai_body}\n")
+            endif()
+            message(STATUS "test_wasm_node: staged ${_root} from ${_src_dir}")
+        endforeach()
         target_link_options(test_wasm_node
             PUBLIC "SHELL: --embed-file ${CMAKE_BINARY_DIR}/test_olean_staging@/")
     endif()
diff --git a/Dockerfile.docs-builder b/Dockerfile.docs-builder
index 43ef20e..5feeec0 100644
--- a/Dockerfile.docs-builder
+++ b/Dockerfile.docs-builder
@@ -27,8 +27,7 @@ COPY scripts/empty-marker.txt /opt/lean-path/.empty
 #
 # Refresh when any of these change:
 #   src/, include/, cmake/, CMakeLists.txt, lakefile.lean,
-#   lean-toolchain, pixi.toml, pixi.lock, examples/sparkle/,
-#   hesper/, hesper-wasm/, scripts/, this Dockerfile.
+#   lean-toolchain, pixi.toml, pixi.lock, scripts/, this Dockerfile.
 
 FROM ghcr.io/prefix-dev/pixi:latest AS builder
 
@@ -60,9 +59,6 @@ COPY include/      ./include/
 COPY share/        ./share/
 COPY scripts/      ./scripts/
 COPY src/          ./src/
-COPY examples/     ./examples/
-COPY hesper/       ./hesper/
-COPY hesper-wasm/  ./hesper-wasm/
 COPY test_wasm_node.cpp ./
 
 # Bring up enough Lean targets that WasmRepl links and that
@@ -70,18 +66,11 @@ COPY test_wasm_node.cpp ./
 # WASM-side targets; xlean-convert is host.
 RUN lake build REPL Display WasmRepl xlean-convert
 
-# Sparkle .olean → embedded into WASM VFS.
-RUN cd examples/sparkle && lake update && lake build SparkleDemo || \
-    echo "WARN: Sparkle build failed; continuing without Sparkle"
-
-# Hesper WGSL DSL (Phase 1).
-RUN if [ -f hesper/Hesper.lean ]; then \
-      mkdir -p hesper-wasm/build && \
-      bash hesper-wasm/build-wasm.sh hesper hesper-wasm/build \
-        Hesper.WGSL.DSL Hesper.WGSL.Helpers Hesper.WGSL.Templates \
-        Hesper.WGSL.Shader Hesper.WGSL.Kernel \
-        || echo "WARN: hesper-wasm build failed"; \
-    else echo "Hesper submodule absent"; fi
+# Third-party Lean libraries are not built here.  The docs-deploy
+# path only ships math-visual + Lean tutorials, and any downstream
+# image that needs an extra library does its own build and passes
+# -DEXTRA_WASM_DIRS=<staging> to emcmake below.  See README.md
+# "Extending the kernel with your own Lean lib".
 
 # Emscripten + cmake + emmake.
 RUN pixi run -e wasm-build fix-emscripten-links || true
@@ -115,9 +104,6 @@ RUN PREFIX=$(pixi info -e wasm-host --json 2>/dev/null \
       | python3 -c "import sys,json; print(json.load(sys.stdin)['environments_info'][0]['prefix'])" \
       2>/dev/null || echo ".pixi/envs/wasm-host") && \
     if [ -d "$PREFIX/share/jupyter/olean" ]; then \
-      if [ -d hesper-wasm/build/Hesper ]; then \
-        ln -sf "$(realpath hesper-wasm/build/Hesper)" "$PREFIX/share/jupyter/olean/Hesper"; \
-      fi && \
       mkdir -p /opt/xeus-lean/_olean && \
       bash scripts/pack-olean-modules.sh "$PREFIX/share/jupyter/olean" /opt/xeus-lean/_olean "" && \
       ls -lh /opt/xeus-lean/_olean; \
diff --git a/Dockerfile.native b/Dockerfile.native
index e612456..bc94d6b 100644
--- a/Dockerfile.native
+++ b/Dockerfile.native
@@ -1,14 +1,16 @@
 # Dockerfile.native — xeus-lean base image (kernel + Display lib).
 #
-# Published as `ghcr.io/verilean/xeus-lean:latest`. Project-specific
-# downstream images (Sparkle, Hesper, ...) FROM this and use the
-# generic `XEUS_LEAN_EXTRA_LIBS` extension point declared in
-# `lakefile.lean` to thread their own static libraries into xlean.
+# Published as `ghcr.io/verilean/xeus-lean:latest`. Downstream
+# projects FROM this and use the generic `XEUS_LEAN_EXTRA_LIBS`
+# extension point declared in `lakefile.lean` to thread their own
+# static libraries into xlean.  See README.md ("Extending the
+# kernel with your own Lean lib") and `tests/fixtures/mock-extra/`
+# for the worked example.
 #
 # Run as a JupyterLab server:
 #   docker run --rm -it -p 8888:8888 ghcr.io/verilean/xeus-lean:latest
 #
-# Or as a Sparkle/Hesper base:
+# Or as the base for a downstream image:
 #   FROM ghcr.io/verilean/xeus-lean:latest
 #   COPY my-lib/ /app/my-lib/
 #   RUN cd /app/my-lib && lake build mylib
diff --git a/Dockerfile.native-sparkle b/Dockerfile.native-sparkle
deleted file mode 100644
index c762079..0000000
--- a/Dockerfile.native-sparkle
+++ /dev/null
@@ -1,172 +0,0 @@
-# Dockerfile.native-sparkle — xeus-lean Jupyter kernel + Sparkle HDL,
-# native build (no WASM). Use this image when you want to run Sparkle
-# simulations in a notebook; the WASM kernel cannot execute the
-# `Signal.loop` interpreter path today.
-#
-# Build:
-#   docker build -f Dockerfile.native-sparkle -t xeus-lean-native-sparkle .
-#
-# Run with JupyterLab on http://localhost:8888 :
-#   docker run --rm -it -p 8888:8888 -v "$PWD/notebooks:/notebooks" \
-#     xeus-lean-native-sparkle
-#
-# In a notebook:
-#   import Sparkle
-#   open Sparkle.Core.Domain Sparkle.Core.Signal
-#
-#   def counter4 : Signal defaultDomain (BitVec 4) :=
-#     Signal.circuit do
-#       let count ← Signal.reg 0#4
-#       count <~ count + 1#4
-#       return count
-#
-#   #eval IO.println s!"counter: {counter4.val 0}"
-
-FROM ubuntu:24.04
-
-# tzdata + dpkg occasionally drop into an interactive prompt during
-# install. Set both vars and a TZ so the build never hangs.
-ENV DEBIAN_FRONTEND=noninteractive
-ENV TZ=Etc/UTC
-
-RUN apt-get update && apt-get install -y --no-install-recommends \
-        cmake build-essential nlohmann-json3-dev \
-        uuid-dev libssl-dev python3 python3-pip \
-        clang libc++-dev libc++abi-dev \
-        curl git ca-certificates \
-        zstd \
- && rm -rf /var/lib/apt/lists/*
-
-# jupyter_client drives smoke-test-native.py; jupyterlab is what the
-# end user opens in their browser.
-RUN pip install --break-system-packages --no-cache-dir jupyter_client jupyterlab
-
-# Install Lean. Toolchain pinned to match xeus-lean.
-RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \
-      | sh -s -- -y --default-toolchain leanprover/lean4:v4.28.0
-ENV PATH="/root/.elan/bin:${PATH}"
-
-WORKDIR /app
-
-# Copy only what each build phase needs — never `COPY . /app`. The
-# repo holds caches, logs, scratch notebooks and other artefacts that
-# could include local secrets; whitelisting the input keeps those out
-# of the image and out of the build cache. Update this list when a
-# new top-level directory becomes load-bearing for the build.
-COPY CMakeLists.txt lakefile.lean lake-manifest.json lean-toolchain /app/
-COPY cmake/    /app/cmake/
-COPY include/  /app/include/
-COPY src/      /app/src/
-
-# Build the C++ FFI library (xeus, xeus-zmq, libzmq fetched via cmake).
-RUN cmake -S . -B build-cmake \
-      -DCMAKE_C_COMPILER=clang \
-      -DCMAKE_CXX_COMPILER=clang++ \
-      -DCMAKE_CXX_FLAGS="-stdlib=libc++" && \
-    cmake --build build-cmake -j
-
-# Linux glibc C23 shim (clang -> __isoc23_strtoull -> Lean's older glibc).
-RUN leanc -c src/glibc_isoc23_compat.c -o build-cmake/glibc_isoc23_compat.o
-
-# Build the kernel binary + the Display lib (so notebook cells can
-# `import Display` for inline SVG/HTML/Markdown rich output).
-RUN lake build xlean Display
-
-# Build Sparkle. `lake update` lazily fetches the upstream sparkle
-# package and its transitive deps; `lake build sparkle` produces the
-# .olean files **and** the per-module compiled `.c.o.export` objects
-# we will link into xlean below (so notebook cells can `#eval`
-# expressions that go through Sparkle's C FFI symbols like
-# `sparkle_eval_at`).
-#
-# xeus-lean and upstream Sparkle now pin the same Lean toolchain
-# (4.28.0 final), so olean headers match — no toolchain override
-# needed.
-COPY examples/sparkle/ /app/examples/sparkle/
-RUN cd examples/sparkle && lake update && lake build SparkleDemo sparkle
-
-# Bundle the per-module Sparkle compiled objects into a single static
-# archive that xlean can link with `--whole-archive`. We exclude
-# `Main.c.o.export` because it carries a `lean_main` symbol that
-# clashes with xlean's own `lean_main`. The archive lives in
-# /app/build-cmake/ so the next step finds it at a stable path.
-RUN cd examples/sparkle/.lake/packages/sparkle/.lake/build/ir && \
-    find . -name "*.c.o.export" ! -name "Main.c.o.export" -print0 \
-      | xargs -0 ar rcs /app/build-cmake/libsparkle_olean.a
-
-# Relink xlean against Sparkle. `XEUS_LEAN_EXTRA_LIBS` is the generic
-# extension point in xeus-lean's lakefile — anything in this whitespace-
-# separated list is appended verbatim to xlean's link line. We wrap the
-# Sparkle libs in `--whole-archive` because no symbol in xlean directly
-# references them (only the Lean interpreter does, at runtime), so a
-# normal link would drop them as dead code.
-RUN rm -f /app/.lake/build/bin/xlean && \
-    XEUS_LEAN_EXTRA_LIBS="-Wl,--whole-archive \
-      /app/build-cmake/libsparkle_olean.a \
-      /app/examples/sparkle/.lake/packages/sparkle/.lake/build/c_src/libsparkle_barrier.a \
-      /app/examples/sparkle/.lake/packages/sparkle/.lake/build/c_src/libsparkle_jit.a \
-      -Wl,--no-whole-archive" \
-      lake build xlean
-
-# Register the kernelspec under /root/.local/share/jupyter so that
-# `jupyter lab` finds it. install-kernelspec.sh also writes
-# LD_LIBRARY_PATH into kernel.json so xlean's runtime libs (libxeus,
-# libxeus-zmq, libzmq) resolve.
-COPY scripts/ /app/scripts/
-RUN bash scripts/install-kernelspec.sh --user
-
-# Make Sparkle + Display importable from notebook cells, and add the
-# Lean toolchain bin dir to PATH so `bv_decide` can spawn `cadical`
-# (the SAT solver ships with elan but isn't on the kernel's default
-# PATH). The kernelspec installer writes LD_LIBRARY_PATH but not LEAN_PATH
-# / PATH, so rather than touch the cross-platform installer we append
-# them here.
-RUN python3 -c "import json,pathlib; \
-p=pathlib.Path('/root/.local/share/jupyter/kernels/xlean/kernel.json'); \
-spec=json.loads(p.read_text()); \
-env=spec.get('env',{}); \
-env['LEAN_PATH']='/app/examples/sparkle/.lake/packages/sparkle/.lake/build/lib/lean:/app/.lake/build/lib/lean'; \
-env['PATH']='/root/.elan/toolchains/leanprover--lean4---v4.28.0/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin'; \
-spec['env']=env; \
-p.write_text(json.dumps(spec,indent=2))"
-
-# Smoke-test the kernel inside the image so a broken build fails the
-# `docker build` rather than silently shipping. Three eval cells take
-# ~5 s; if the kernel can't start at all this fails fast.
-RUN python3 scripts/smoke-test-native.py
-
-# Exercise `import Sparkle` + that the core types kind-check. With the
-# toolchain pins aligned (both 4.28.0 final), `Signal.circuit` macro
-# expansion is now sorry-free and a real simulation cell could run too;
-# the smoke test here is the minimum kernel-loads-Sparkle check.
-RUN python3 scripts/smoke-test-sparkle.py
-
-# Strip build-time crud that doesn't need to ship: each fetched
-# dependency carries a full `.git/` (xeus, xeus-zmq, xtl, cppzmq,
-# libzmq under build-cmake/_deps; sparkle + transitive Lake deps
-# under examples/sparkle/.lake), plus dotfiles like `.clang-format`
-# / `.travis.yml` that are only meaningful in their upstream repo.
-# Removing them shaves several hundred MB and makes the image easier
-# to reason about for security review.
-RUN find /app/build-cmake/_deps -type d -name ".git" -prune -exec rm -rf {} + 2>/dev/null; \
-    find /app/examples/sparkle/.lake -type d -name ".git" -prune -exec rm -rf {} + 2>/dev/null; \
-    find /app \
-      \( -name ".clang-format" -o -name ".clang-tidy" \
-         -o -name ".travis.yml" -o -name ".hgeol" \
-         -o -name ".mailmap" -o -name ".git-blame-ignore-revs" \
-         -o -name ".releash.py" -o -name ".gitignore" \
-         -o -name ".dockerignore" -o -name ".envrc" \) \
-      -delete 2>/dev/null; \
-    true
-
-# Pre-populate /notebooks so users see something on first launch even
-# without a -v mount. Mounting -v $PWD/notebooks:/notebooks at run
-# time will of course override this.
-COPY notebooks/sparkle-native-demo.ipynb /notebooks/sparkle-native-demo.ipynb
-
-# Default command: launch JupyterLab serving /notebooks on :8888.
-WORKDIR /notebooks
-EXPOSE 8888
-CMD ["jupyter", "lab", \
-     "--ip=0.0.0.0", "--allow-root", "--no-browser", \
-     "--ServerApp.token=", "--ServerApp.password="]
diff --git a/Dockerfile.wasm b/Dockerfile.wasm
index e2a7656..449a4c9 100644
--- a/Dockerfile.wasm
+++ b/Dockerfile.wasm
@@ -47,9 +47,6 @@ COPY include/      ./include/
 COPY share/        ./share/
 COPY scripts/      ./scripts/
 COPY src/          ./src/
-COPY examples/     ./examples/
-COPY hesper/       ./hesper/
-COPY hesper-wasm/  ./hesper-wasm/
 COPY notebooks/    ./notebooks/
 COPY test_wasm_node.cpp ./
 
@@ -58,22 +55,11 @@ COPY test_wasm_node.cpp ./
 # it must be built before WasmRepl because WasmRepl.lean imports it.
 RUN lake build REPL Display WasmRepl
 
-# Build Sparkle example to generate .olean files that will be
-# embedded in the WASM VFS (CMakeLists.txt looks for them at
-# examples/sparkle/.lake/packages/sparkle/.lake/build/lib/lean/).
-RUN cd examples/sparkle && lake update && lake build SparkleDemo || \
-    echo "WARNING: Sparkle build failed, continuing without Sparkle support"
-
-# Build Hesper WGSL DSL (Phase 1 — pure Lean, no FFI). The build wrapper
-# under hesper-wasm/ applies WASM-specific patches and a stripped lakefile
-# so the upstream submodule stays unmodified.
-RUN if [ -f hesper/Hesper.lean ]; then \
-      mkdir -p hesper-wasm/build && \
-      bash hesper-wasm/build-wasm.sh hesper hesper-wasm/build \
-        Hesper.WGSL.DSL Hesper.WGSL.Helpers Hesper.WGSL.Templates \
-        Hesper.WGSL.Shader Hesper.WGSL.Kernel \
-        || echo "WARNING: hesper-wasm build failed, continuing without Hesper"; \
-    else echo "Hesper submodule absent, skipping"; fi
+# Third-party Lean libraries (Sparkle, Hesper, …) are not built here.
+# Downstream consumers either run their own build script then pass
+# -DEXTRA_WASM_DIRS=<staging> to emcmake, or they `docker build`
+# from a different Dockerfile FROM this image.  See README.md
+# "Extending the kernel with your own Lean lib" for the contract.
 
 # Build WASM kernel
 # 1. Fix emscripten symlinks
@@ -125,7 +111,8 @@ RUN mkdir -p notebooks && \
     find _output -name "xlean*" -ls && \
     cat _output/xeus/kernels.json
 
-# 7. Pack olean assets (Std/Lean/Sparkle) into per-module zstd tarballs.
+# 7. Pack default olean assets (Std/Lean and any EXTRA_WASM_DIRS
+# olean roots that CMake already staged) into per-module zstd tarballs.
 # Phase 2: replaces ~1.5GB of raw .olean files with ~275MB of compressed
 # tarballs. The runtime (src/post.js) fetches and extracts them.
 RUN apt-get update && apt-get install -y zstd && rm -rf /var/lib/apt/lists/*
@@ -133,9 +120,6 @@ RUN PREFIX=$(pixi info -e wasm-host --json 2>/dev/null \
       | python3 -c "import sys,json; print(json.load(sys.stdin)['environments_info'][0]['prefix'])" \
       2>/dev/null || echo ".pixi/envs/wasm-host") && \
     if [ -d "$PREFIX/share/jupyter/olean" ]; then \
-      if [ -d hesper-wasm/build/Hesper ]; then \
-        ln -sf "$(realpath hesper-wasm/build/Hesper)" "$PREFIX/share/jupyter/olean/Hesper"; \
-      fi && \
       mkdir -p _output/xeus/wasm-host/olean && \
       bash scripts/pack-olean-modules.sh "$PREFIX/share/jupyter/olean" _output/xeus/wasm-host/olean "" && \
       echo "Packed default olean tarballs:" && \
diff --git a/README.md b/README.md
index 42deb7d..66fcd8a 100644
--- a/README.md
+++ b/README.md
@@ -259,35 +259,94 @@ comments inside `src/post.js`.
 
 ## Extending the kernel with your own Lean lib
 
-Downstream projects (Sparkle, Hesper, …) extend
-`ghcr.io/verilean/xeus-lean` by lake-building their own Lean lib and
-re-linking xlean against it. The mechanism is `XEUS_LEAN_EXTRA_LIBS`,
-a generic env-var-driven extension point in `lakefile.lean`. Sketch
-Dockerfile:
-
-```dockerfile
-FROM ghcr.io/verilean/xeus-lean:latest
-
-COPY my-lib/ /app/my-lib/
-RUN cd /app/my-lib && lake update && lake build mylib
-
-# Bundle compiled olean objects into a static archive.
-RUN cd /app/my-lib/.lake/packages/mylib/.lake/build/ir && \
-    find . -name '*.c.o.export' ! -name 'Main.c.o.export' -print0 \
-      | xargs -0 ar rcs /app/build-cmake/libmy_olean.a
-
-# Relink xlean. --whole-archive is required because no symbol in xlean
-# directly references project libs (the Lean interpreter looks them up
-# at runtime), so a normal link would drop them as dead code.
-RUN rm -f /app/.lake/build/bin/xlean && \
-    XEUS_LEAN_EXTRA_LIBS="-Wl,--whole-archive \
-      /app/build-cmake/libmy_olean.a \
-      /app/my-lib/.lake/.../libmy_ffi.a \
-      -Wl,--no-whole-archive" \
-    lake build xlean
+> **What goes in this repo, and what doesn't.**
+>
+> The xeus-lean repository owns three things:
+> 1. The Lean WASM/native kernel (`xlean`, `xlean.wasm/js`) and its
+>    REPL frontend.
+> 2. The JupyterLite hosting glue (`pre.js`, `post.js`, manifest
+>    loader, `%load`, `%memory`).
+> 3. A **vendor-agnostic mechanism** for downstream Lean libraries
+>    to plug their own static archives, Lean externs, and oleans
+>    into both build targets (WASM and native).
+>
+> What it does **not** own: any particular third-party library.
+> Sparkle, Hesper, Mathlib bundle assemblers, future Lean libraries —
+> all of those live in their own repos and use the extension point
+> below.  No third-party project name should appear in xeus-lean's
+> build files (CMake / Dockerfiles / CI workflows / Lean REPL boot).
+>
+> If you find such a name in this repo, file an issue — it's a bug,
+> not a feature.
+
+### Extension point: `EXTRA_WASM_DIRS` (WASM target)
+
+The WASM build accepts a CMake variable `EXTRA_WASM_DIRS` — a
+`;`-separated list of staging directories produced by third-party
+projects.  Each staging directory must contain a manifest:
+
+```json
+// <staging>/xeus-lean-extra.json
+{
+  "archive":    "lib/libmylib_wasm.a",      // whole-archive into xlean
+  "exports":    "lib/mylib_exports.txt",    // one C symbol per line
+  "olean_root": "MyLib"                     // optional; copied to /lib/lean/
+}
+```
+
+The third-party project's build script writes those three artefacts
+into `<staging>/lib/` + `<staging>/MyLib/**` and emits the manifest.
+xeus-lean's CMake then:
+
+1. Whole-archives `libmylib_wasm.a` into `xlean.wasm` (Lean externs
+   would otherwise be DCE'd).
+2. Splats `mylib_exports.txt` into emcc's `-sEXPORTED_FUNCTIONS` so
+   the symbols survive LTO.
+3. Copies `MyLib/**/*.olean` into the JupyterLite olean asset tree
+   alongside `Init/Std/Lean/Mathlib`.
+
+Pass it to the WASM build like so:
+
+```bash
+emcmake cmake -S . -B wasm-build \
+  -DEXTRA_WASM_DIRS="/path/to/mylib-staging;/path/to/otherlib-staging"
 ```
 
-`Dockerfile.native-sparkle` is the worked example.
+### Worked example: `tests/fixtures/mock-extra/`
+
+The repo ships a minimal third-party-style fixture under
+`tests/fixtures/mock-extra/` that exercises the **whole** extension
+path: a `MockExtra` Lean lib with `@[extern "mock_hello"] opaque
+mockHello`, a C file implementing it, a `build-wasm.sh` that emits
+the manifest, and a CI step that links it via `EXTRA_WASM_DIRS` and
+asserts `#eval mockHello ()` returns the expected string.
+
+That fixture is the contract.  If you can write a downstream lib that
+plugs in the same way, you're done.  If `EXTRA_WASM_DIRS` ever
+breaks, the fixture's CI step turns red.
+
+### Build-time caching for downstream consumers
+
+The Lean WASM build itself takes ~30 minutes from cold (Lean
+runtime, REPL, xeus glue, emcc link).  We do **not** want every
+downstream consumer to pay that cost just because they're adding a
+1-MB extra library.  The plan to avoid it:
+
+| Stage | Image / Mechanism | Owner |
+|---|---|---|
+| 1 | Sparkle/Hesper removal + mock-extra fixture exercises the generic path end-to-end via a full WASM rebuild on every CI run. | This PR (#13). |
+| 2 | Publish `ghcr.io/verilean/xeus-lean-wasm-prebuild:<sha>` containing the intermediate `xlean.dir/*.o` + Lean runtime archives + emcc.  CI's WASM job pulls it, builds the third-party staging dir, then **relinks** `xlean.wasm` with `EXTRA_WASM_DIRS` instead of compiling from scratch — should reduce wall time from ~30 min to ~5-10 min. | Follow-up PR. |
+
+So stage 1 proves correctness (the third-party path works); stage 2
+proves it's also fast enough for downstream consumers to use without
+their own CI grinding.  Both stages preserve the rule that xeus-lean
+itself never knows a third-party name.
+
+### Native target
+
+Same story is in progress for the native `xlean` binary (dlopen of
+shared libraries declared via a sibling manifest).  Not yet wired —
+tracked separately so the WASM contract lands first.
 
 ## CI / CD
 
diff --git a/examples/sparkle/.gitignore b/examples/sparkle/.gitignore
deleted file mode 100644
index bacbb2b..0000000
--- a/examples/sparkle/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-.lake/
-build/
diff --git a/examples/sparkle/SparkleDemo.lean b/examples/sparkle/SparkleDemo.lean
deleted file mode 100644
index fc0b1cd..0000000
--- a/examples/sparkle/SparkleDemo.lean
+++ /dev/null
@@ -1,28 +0,0 @@
-/-
-Sparkle HDL demo for xeus-lean Jupyter kernel.
-
-This file verifies that Sparkle can be imported and basic circuit
-definition + simulation works. It serves as both a build-test and
-a reference for notebook cells.
--/
-import Sparkle
-
-open Sparkle.Core.Domain
-open Sparkle.Core.Signal
-
--- A simple 4-bit counter that increments every clock cycle.
--- Uses Sparkle's `circuit do` DSL (Sparkle.Core.CircuitDo): the
--- `let _ ← Signal.reg _` and `_ <~ _` constructs are macros that
--- elaborate to a Signal expression.
-def counter4 : Signal defaultDomain (BitVec 4) :=
-  circuit do
-    let count ← Signal.reg 0#4
-    count <~ count + 1#4
-    return count
-
--- Simulation runs at runtime (not #eval at build time) because
--- Sparkle's Signal.evalSignalAt uses C FFI that requires the
--- native shared library to be loaded.
-def main : IO Unit := do
-  let results := counter4.sample 20
-  IO.println s!"4-bit counter (20 cycles): {results}"
diff --git a/examples/sparkle/lake-manifest.json b/examples/sparkle/lake-manifest.json
deleted file mode 100644
index 7767ee7..0000000
--- a/examples/sparkle/lake-manifest.json
+++ /dev/null
@@ -1,75 +0,0 @@
-{"version": "1.1.0",
- "packagesDir": ".lake/packages",
- "packages":
- [{"url": "https://github.com/Verilean/sparkle",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "c485c0ae2f100d6289c54d18c0dc6c817194875b",
-   "name": "sparkle",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/argumentcomputer/LSpec",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "dc0904293d309af1ba4fcaae581cc8dd7b27f08e",
-   "name": "LSpec",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "437bd7d8c71e5cc00132d66eaf96f2acc0382c1c",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "8668e1ab7c987fb8ed1349f14c3b7b60bd5f27b6",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/dupuisf/BibtexQuery",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "1c5c543d2637aebf90c80aead2d401ae88db13cc",
-   "name": "BibtexQuery",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "38ac5945d744903ffcc473ce1030223991b11cf6",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"}],
- "name": "«sparkle-demo»",
- "lakeDir": ".lake"}
diff --git a/examples/sparkle/lakefile.lean b/examples/sparkle/lakefile.lean
deleted file mode 100644
index eff2892..0000000
--- a/examples/sparkle/lakefile.lean
+++ /dev/null
@@ -1,13 +0,0 @@
-import Lake
-open Lake DSL
-
-package «sparkle-demo» where
-  leanOptions := #[⟨`autoImplicit, false⟩]
-
-require sparkle from git
-  "https://github.com/Verilean/sparkle" @ "main"
-
-@[default_target]
-lean_exe sparkleDemo where
-  root := `SparkleDemo
-  supportInterpreter := true
diff --git a/hesper b/hesper
deleted file mode 160000
index 98210a6..0000000
--- a/hesper
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 98210a6ff20861b1a18e9321720d5296760b37a4
diff --git a/hesper-wasm/build-wasm.sh b/hesper-wasm/build-wasm.sh
deleted file mode 100755
index 707f3f9..0000000
--- a/hesper-wasm/build-wasm.sh
+++ /dev/null
@@ -1,119 +0,0 @@
-#!/usr/bin/env bash
-# build-wasm.sh - Build the Hesper Lean library for the WASM REPL.
-#
-# Steps:
-#  1. Apply patches/*.patch onto the hesper submodule (toolchain-only fixes).
-#  2. Swap in lakefile-wasm.lean (drops LSpec, native-deps, Tests, Examples).
-#  3. Pin the toolchain to xeus-lean's (4.28-rc1).
-#  4. Build the requested target(s) via `lake build`.
-#  5. Copy the produced .olean / .ir / .ilean files into the staging dir.
-#  6. Restore the submodule to a clean state.
-#
-# Usage:
-#   build-wasm.sh <hesper-submodule-dir> <out-staging-dir> [target ...]
-#
-# `target` defaults to `Hesper.WGSL.DSL` (Phase 1 minimum).
-set -euo pipefail
-
-HESPER_DIR="${1:?usage: $0 <hesper-dir> <out-dir> [target ...]}"
-OUT_DIR="${2:?usage: $0 <hesper-dir> <out-dir> [target ...]}"
-shift 2
-TARGETS=("${@:-Hesper.WGSL.DSL}")
-
-if [ ! -f "$HESPER_DIR/Hesper.lean" ]; then
-    echo "ERROR: $HESPER_DIR does not look like a Hesper checkout" >&2
-    exit 1
-fi
-
-# Resolve to absolute paths because the script `cd "$HESPER_DIR"` later
-# and per-file references would break with relative paths after that.
-HESPER_DIR="$(cd "$HESPER_DIR" && pwd)"
-mkdir -p "$OUT_DIR"
-OUT_DIR="$(cd "$OUT_DIR" && pwd)"
-
-WRAP_DIR="$(cd "$(dirname "$0")" && pwd)"
-PATCH_DIR="$WRAP_DIR/patches"
-LAKEFILE_OVERRIDE="$WRAP_DIR/lakefile-wasm.lean"
-TOOLCHAIN_FILE="$(cd "$WRAP_DIR/.." && pwd)/lean-toolchain"
-
-# ------------------------------------------------------------------
-# 1. Save originals so we can restore even if `lake build` fails.
-# ------------------------------------------------------------------
-cd "$HESPER_DIR"
-cp -f lakefile.lean lakefile.lean.xeus-bak 2>/dev/null || true
-cp -f lakefile.toml lakefile.toml.xeus-bak 2>/dev/null || true
-cp -f lean-toolchain lean-toolchain.xeus-bak 2>/dev/null || true
-
-restore() {
-    cd "$HESPER_DIR"
-    [ -f lakefile.lean.xeus-bak ] && mv -f lakefile.lean.xeus-bak lakefile.lean || rm -f lakefile.lean
-    [ -f lakefile.toml.xeus-bak ] && mv -f lakefile.toml.xeus-bak lakefile.toml || rm -f lakefile.toml
-    [ -f lean-toolchain.xeus-bak ] && mv -f lean-toolchain.xeus-bak lean-toolchain || true
-    # Roll patched files back via `git checkout` (submodule has its own .git/).
-    git -C "$HESPER_DIR" checkout -- . 2>/dev/null || true
-}
-trap restore EXIT
-
-# ------------------------------------------------------------------
-# 2. Apply patches.
-# ------------------------------------------------------------------
-if [ -d "$PATCH_DIR" ]; then
-    for p in "$PATCH_DIR"/*.patch; do
-        [ -e "$p" ] || continue
-        echo "[hesper-wasm] applying patch $(basename "$p")"
-        git apply --whitespace=nowarn "$p"
-    done
-fi
-
-# ------------------------------------------------------------------
-# 3. Override lakefile + toolchain.
-# ------------------------------------------------------------------
-cp -f "$LAKEFILE_OVERRIDE" "$HESPER_DIR/lakefile.lean"
-rm -f "$HESPER_DIR/lakefile.toml"           # lake prefers .toml when both exist
-rm -f "$HESPER_DIR/lake-manifest.json"      # force fresh deps resolution
-rm -rf "$HESPER_DIR/.lake/packages"         # forget LSpec / git deps
-if [ -f "$TOOLCHAIN_FILE" ]; then
-    cp -f "$TOOLCHAIN_FILE" "$HESPER_DIR/lean-toolchain"
-fi
-
-# ------------------------------------------------------------------
-# 4. Build.
-# ------------------------------------------------------------------
-echo "[hesper-wasm] lake build ${TARGETS[*]}"
-lake build "${TARGETS[@]}"
-
-# ------------------------------------------------------------------
-# 5. Stage outputs.
-# ------------------------------------------------------------------
-LIB="$HESPER_DIR/.lake/build/lib/lean"
-IR="$HESPER_DIR/.lake/build/ir"
-if [ ! -d "$LIB" ]; then
-    echo "ERROR: $LIB missing — lake build produced no oleans" >&2
-    exit 2
-fi
-
-mkdir -p "$OUT_DIR/Hesper"
-# Copy only the kinds of files the runtime needs:
-#   .olean         — kernel data
-#   .olean.server  — server / metadata layer (Lean 4.28+)
-#   .olean.private — private declarations
-#   .ir / .ilean   — IR for runtime interpreter
-# Skip .trace and .hash (build-time only).
-copy_match() {
-    local src="$1" rel
-    [ -e "$src" ] || return 0
-    rel="${src#$LIB/}"
-    mkdir -p "$OUT_DIR/$(dirname "$rel")"
-    cp -f "$src" "$OUT_DIR/$rel"
-}
-
-# Top-level umbrella + every Hesper/** entry of allowed extensions.
-for ext in olean olean.server olean.private ir ilean; do
-    [ -e "$LIB/Hesper.$ext" ] && copy_match "$LIB/Hesper.$ext"
-    while IFS= read -r -d '' f; do
-        copy_match "$f"
-    done < <(find "$LIB/Hesper" -type f -name "*.$ext" -print0 2>/dev/null)
-done
-
-NUM=$(find "$OUT_DIR" -type f \( -name '*.olean*' -o -name '*.ir' -o -name '*.ilean' \) | wc -l)
-echo "[hesper-wasm] staged $NUM files into $OUT_DIR"
diff --git a/hesper-wasm/lakefile-wasm.lean b/hesper-wasm/lakefile-wasm.lean
deleted file mode 100644
index 287b81f..0000000
--- a/hesper-wasm/lakefile-wasm.lean
+++ /dev/null
@@ -1,20 +0,0 @@
--- WASM-only Lake build override for the hesper submodule.
---
--- Drops upstream's LSpec dependency, the native-deps trigger, and the
--- Tests / Examples libraries. The WASM REPL only needs the compiled
--- `Hesper` Lean library (and not even all of it — Phase 1 needs just
--- WGSL; later phases will pull in more).
---
--- This file is COPIED into the hesper submodule by build-wasm.sh just
--- before `lake build`. The original lakefile.lean / lakefile.toml are
--- preserved on disk and restored after the build.
-
-import Lake
-open Lake DSL
-
-package «Hesper» where
-
-lean_lib «Hesper» where
-  globs := #[.submodules `Hesper]
-
--- We want to expose the lib only — no executables on WASM.
diff --git a/hesper-wasm/patches/0001-lean-4.28-string-slice.patch b/hesper-wasm/patches/0001-lean-4.28-string-slice.patch
deleted file mode 100644
index 2fa0f70..0000000
--- a/hesper-wasm/patches/0001-lean-4.28-string-slice.patch
+++ /dev/null
@@ -1,29 +0,0 @@
-From 0000000000000000000000000000000000000000 Mon Sep 17 00:00:00 2001
-Subject: [PATCH] Hesper/WGSL/Exp: convert String.Slice -> String
-
-In Lean 4.28, String.dropRightWhile returns a String.Slice rather than
-a String. Hesper's WGSL Exp.lean was written against 4.26 and treats
-the result as String. Adding a .toString conversion keeps the existing
-behavior on the new toolchain. The deprecation warning for
-dropRightWhile -> dropEndWhile is left intact for upstream Hesper to
-address.
-
-Applied by xeus-lean's hesper-wasm build wrapper. Drop this patch when
-upstream Hesper supports Lean 4.28+.
----
- Hesper/WGSL/Exp.lean | 2 +-
- 1 file changed, 1 insertion(+), 1 deletion(-)
-
-diff --git a/Hesper/WGSL/Exp.lean b/Hesper/WGSL/Exp.lean
-index 0000000..0000000 100644
---- a/Hesper/WGSL/Exp.lean
-+++ b/Hesper/WGSL/Exp.lean
-@@ -511,7 +511,7 @@
-     let mIntPart := mStr.take 1
-     let mFracPart := mStr.drop 1
-     -- Trim trailing zeros from fraction for cleaner output
--    let mFracTrimmed := mFracPart.dropRightWhile (· == '0')
-+    let mFracTrimmed := (mFracPart.dropRightWhile (· == '0')).toString
-     let mFracFinal := if mFracTrimmed.isEmpty then "0" else mFracTrimmed
-     s!"{sign}{mIntPart}.{mFracFinal}e{expInt}"
-
diff --git a/notebooks/mathlib-demo.ipynb b/notebooks/mathlib-demo.ipynb
index 61551bb..4a92639 100644
--- a/notebooks/mathlib-demo.ipynb
+++ b/notebooks/mathlib-demo.ipynb
@@ -7,7 +7,7 @@
     "# Mathlib in the browser\n",
     "\n",
     "This notebook loads the on-demand Mathlib bundle.  The default xeus-lean\n",
-    "kernel ships only Init/Std/Lean/Sparkle (~280 MB compressed) so the\n",
+    "kernel ships only Init/Std/Lean (~200 MB compressed) so the\n",
     "first-page boot is small; running the next cell fetches Mathlib + its\n",
     "deps (Aesop, Batteries, ImportGraph, ProofWidgets, Plausible, Qq) on\n",
     "top of that.\n",
diff --git a/notebooks/sparkle-demo.ipynb b/notebooks/sparkle-demo.ipynb
deleted file mode 100644
index 6561dca..0000000
--- a/notebooks/sparkle-demo.ipynb
+++ /dev/null
@@ -1,30 +0,0 @@
-{
- "cells": [
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "import Sparkle\n",
-    "open Sparkle.Core.Domain Sparkle.Core.Signal\n",
-    "\n",
-    "#eval IO.println s!\"counter: hello\"\n"
-   ]
-  }
- ],
- "metadata": {
-  "kernelspec": {
-   "display_name": "Lean 4",
-   "language": "lean4",
-   "name": "xlean"
-  },
-  "language_info": {
-   "file_extension": ".lean",
-   "mimetype": "text/x-lean4",
-   "name": "lean"
-  }
- },
- "nbformat": 4,
- "nbformat_minor": 5
-}
\ No newline at end of file
diff --git a/notebooks/sparkle-native-demo.ipynb b/notebooks/sparkle-native-demo.ipynb
deleted file mode 100644
index 131fd90..0000000
--- a/notebooks/sparkle-native-demo.ipynb
+++ /dev/null
@@ -1,283 +0,0 @@
-{
- "cells": [
-  {
-   "cell_type": "markdown",
-   "id": "intro",
-   "metadata": {},
-   "source": "# xeus-lean + Sparkle HDL \u2014 interactive hardware tutorial\n\nThis is the **native** Lean Jupyter kernel with the [Sparkle HDL](https://github.com/Verilean/sparkle) library on the search path. Eleven short sections cover what xeus-lean + Sparkle can do today:\n\n1. **Simulate** an 8-bit counter directly as a Lean function.\n2. **Render an SVG waveform** inline in the notebook.\n3. **Emit a VCD file** (open it in [GTKWave](http://gtkwave.sourceforge.net/) for a real waveform viewer).\n4. **Synthesize SystemVerilog** from a Sparkle DSL function.\n5. **Prove** a hardware property with `bv_decide` / `native_decide`.\n6. **Visualize a real-ish protocol** \u2014 an I\u00b2C master writing one byte, with SCL and SDA on the same plot.\n7. **Stateful circuit** \u2014 a 4-bit counter built with Sparkle's `circuit do ... let count \u2190 Signal.reg ...` macro, evaluated through the C FFI memoized loop.\n8. **Notebook helpers** \u2014 `#help_x`, `#findDecl`, `#listNs`, `#sig`, `#bash`.\n9. **Mermaid sketches** \u2014 quick block-diagram drafts via `#mermaid`.\n10. **Block-accurate diagrams** via `Display.blockDiagram` (trapezoid MUX, real cloud, AND/OR/NOT gates, \u2295 adder).\n11. **Multi-million-tick traces** via `.wdb` \u2014 zstd-block compressed waveform DB, ~50\u00d7 smaller than gzipped VCD, viewer streams only the visible window.\n\n### Two REPL gotchas\n\nThe xlean kernel treats your whole session as one virtual `.lean` file. That has two consequences worth knowing up front:\n\n1. **`import` only works in the very first cell you run.** Once any non-import command has executed, `import Sparkle` will be rejected with *\"invalid 'import' command, it must be used in the beginning of the file\"*. If you hit that, **Restart Kernel** and run the import cell first.\n2. **`open` does NOT persist across cells.** Each cell is type-checked from a snapshot of the env that excludes prior `open`s. Repeat the `open Sparkle.Core.Domain Sparkle.Core.Signal` line at the top of every cell that uses short names."
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "imports",
-   "metadata": {},
-   "outputs": [],
-   "source": "-- FIRST cell: imports go here, before any other command.\n-- The first run loads Sparkle's full olean tree and takes ~90 s.\nimport Display\nimport Sparkle\nimport Sparkle.Compiler.Elab\nimport Sparkle.Backend.VCD\nimport Sparkle.Backend.Verilog"
-  },
-  {
-   "cell_type": "markdown",
-   "id": "md-sec1",
-   "metadata": {},
-   "source": [
-    "## 1. Simulate an 8-bit counter\n",
-    "\n",
-    "A `Signal d \u03b1` in Sparkle is just a function from a clock tick (`Nat`) to a value (`\u03b1`). We can build one directly with the anonymous-constructor syntax `\u27e8fun t => ...\u27e9` and then evaluate it at any tick."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "code-sec1",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "open Sparkle.Core.Domain Sparkle.Core.Signal\n",
-    "\n",
-    "-- An 8-bit counter: at clock tick t, the value is t mod 256.\n",
-    "def counter : Signal defaultDomain (BitVec 8) := \u27e8fun t => BitVec.ofNat 8 t\u27e9\n",
-    "\n",
-    "#eval (counter.val 0).toNat       -- 0\n",
-    "#eval (counter.val 5).toNat       -- 5\n",
-    "#eval (counter.val 255).toNat     -- 255\n",
-    "#eval (counter.val 256).toNat     -- 0  (BitVec wrap-around)"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "md-sec2",
-   "metadata": {},
-   "source": [
-    "## 2. Render the counter as an SVG waveform\n",
-    "\n",
-    "`Display.waveform` takes a list of `Nat` values and emits an SVG with `image/svg+xml` MIME, which JupyterLab renders inline. We sample the counter for 16 ticks and visualize them."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "code-sec2",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "open Sparkle.Core.Domain Sparkle.Core.Signal\n",
-    "\n",
-    "def counterWave : Signal defaultDomain (BitVec 8) := \u27e8fun t => BitVec.ofNat 8 t\u27e9\n",
-    "def samples : List Nat := (List.range 16).map fun t => (counterWave.val t).toNat\n",
-    "\n",
-    "#eval Display.waveform \"cnt[7:0]\" samples 8 28 80"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "md-sec3",
-   "metadata": {},
-   "source": "## 3. Emit a VCD file (for GTKWave)\n\nThe same trace can be written as a [Value Change Dump](https://en.wikipedia.org/wiki/Value_change_dump) \u2014 the format that GTKWave, Surfer, and most commercial waveform viewers consume. The cell below prints the VCD source; in a real flow you would either\n\n- write the plain text:  `IO.FS.writeFile \"counter.vcd\" vcd`, or\n- write a gzip-compressed `.vcd.gz` (~10\u00d7 smaller, GTKWave reads it natively):  `Display.writeGz \"counter.vcd.gz\" vcd`\n\nthen `gtkwave counter.vcd[.gz]`."
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "code-sec3",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "open Sparkle.Core.Domain Sparkle.Core.Signal Sparkle.Backend.VCD\n",
-    "\n",
-    "def cntSig : Signal defaultDomain (BitVec 8) := \u27e8fun t => BitVec.ofNat 8 t\u27e9\n",
-    "\n",
-    "def writer  := (VCDWriter.new \"counter\").addVar \"cnt\" 8\n",
-    "def trace   := sampleBitVecSignal cntSig \"cnt\" 16\n",
-    "def vcd     := generateVCD writer trace\n",
-    "\n",
-    "#eval IO.println vcd"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "md-sec4",
-   "metadata": {},
-   "source": "## 4. Synthesize SystemVerilog from the Sparkle DSL\n\nWe write hardware as a Lean function over `Signal`s \u2014 a tiny ALU that adds and subtracts based on a select bit. Sparkle's elaborator walks the function and produces an IR `Module`, then `toVerilog` emits synthesizable SystemVerilog.\n\nThe cell below defines a `#showVerilog` macro that runs Sparkle's `synthesizeCombinational` pipeline and pipes the result through `Display.verilog`, which renders it with Highlight.js syntax coloring (loaded lazily from a CDN)."
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "code-sec4-helper",
-   "metadata": {},
-   "outputs": [],
-   "source": "-- One-time helper: a #showVerilog macro that runs Sparkle's\n-- synthesizeCombinational pipeline and renders the resulting\n-- SystemVerilog with syntax highlighting (Display.verilog wraps\n-- Highlight.js with a github theme).\nopen Lean Lean.Elab.Command in\nelab \"#showVerilog \" id:ident : command => do\n  let declName \u2190 liftCoreM <| Lean.resolveGlobalConstNoOverload id\n  -- Synthesise the IR module inside TermElabM, then drop back to\n  -- CoreM to fire Display.verilog (which is plain IO).\n  let v \u2190 liftTermElabM do\n    let (module, _) \u2190 Sparkle.Compiler.Elab.synthesizeCombinational declName\n    pure (Sparkle.Backend.Verilog.toVerilog module)\n  liftCoreM <| (Display.verilog v : IO Unit)"
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "code-sec4-syn",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "open Sparkle.Core.Domain Sparkle.Core.Signal\n",
-    "\n",
-    "-- Sparkle DSL: a tiny ALU. `sel = 0` \u2192 a + b, `sel = 1` \u2192 a - b.\n",
-    "def alu (sel : Signal Domain Bool)\n",
-    "        (a b : Signal Domain (BitVec 8)) : Signal Domain (BitVec 8) :=\n",
-    "  Signal.mux sel (a - b) (a + b)\n",
-    "\n",
-    "#showVerilog alu"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "md-sec5",
-   "metadata": {},
-   "source": [
-    "## 5. Prove a hardware property\n",
-    "\n",
-    "The whole reason Sparkle lives inside Lean is *formal* hardware design \u2014 the same `BitVec` we simulate above also has a full proof theory. Lean's `bv_decide` tactic discharges any quantifier-free `BitVec` proposition by SAT; `native_decide` reduces decidable goals at native speed.\n",
-    "\n",
-    "Below we prove four small properties \u2014 the wrap-around our 4-bit counter showed visually, commutativity of 8-bit addition, an XOR-with-0xFF identity, and a theorem about our `counter` simulation itself."
-   ]
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "code-sec5",
-   "metadata": {},
-   "outputs": [],
-   "source": [
-    "-- Wrap-around: 255 + 1 = 0 in 8-bit arithmetic.\n",
-    "example : (255#8 + 1#8 = 0#8) := by native_decide\n",
-    "\n",
-    "-- Commutativity of 8-bit addition (proved via bit-blasting \u2192 SAT).\n",
-    "example (a b : BitVec 8) : a + b = b + a := by bv_decide\n",
-    "\n",
-    "-- A small ALU-style invariant: XOR with 0xFF flips every bit.\n",
-    "example (a : BitVec 8) : (a ^^^ 0xff#8) = ~~~ a := by bv_decide\n",
-    "\n",
-    "-- And a theorem about the `counter` we simulated above:\n",
-    "-- `counter.val t` always equals `BitVec.ofNat 8 t`, by definition.\n",
-    "example (t : Nat) : counter.val t = BitVec.ofNat 8 t := rfl"
-   ]
-  },
-  {
-   "cell_type": "markdown",
-   "id": "35ea302a",
-   "source": "## 6. A real-ish digital protocol: I\u00b2C master\n\nSo far our \"waveform\" was a monotonically-increasing counter \u2014 pretty, but uninteresting. Let's put both *clock* and *data* on the same plot and watch a small I\u00b2C master write the 7-bit address `0x21` (with R/W = 0, so the byte on the bus is `0x42`). Each bit period is `TPB = 8` simulation ticks, with SCL toggling at the half-period. The transaction is:\n\n| bit period | what's happening |\n|------------|------------------|\n| 0          | START \u2014 SDA falls while SCL is high |\n| 1..8       | data bits, MSB first (`0x42 = 0100_0010`) |\n| 9          | ACK \u2014 slave pulls SDA low |\n| 10         | STOP \u2014 SDA rises while SCL is high |\n\nWe build `scl` and `sda` as ordinary `Signal defaultDomain Bool` values, sample 11 bit periods (88 ticks), and render both lanes on one SVG with `Display.boolWave` \u2014 the two-lane digital-waveform helper that ships with xeus-lean.",
-   "metadata": {}
-  },
-  {
-   "cell_type": "code",
-   "id": "3e0212dc",
-   "source": "open Sparkle.Core.Domain Sparkle.Core.Signal\n\n-- Bit-period geometry: 4 ticks SCL low, 4 ticks SCL high.\ndef TPH : Nat := 4\ndef TPB : Nat := 2 * TPH\n\n-- Byte on the wire (7-bit address 0x21 + write bit). MSB first.\ndef addr : BitVec 8 := 0x42#8\n\n-- Serial clock. High during START/STOP framing, toggles otherwise.\ndef scl : Signal defaultDomain Bool := \u27e8fun t =>\n  let bit := t / TPB\n  let off := t % TPB\n  if bit == 0 then true                          -- START framing\n  else if bit \u2265 1 \u2227 bit \u2264 9 then off \u2265 TPH       -- data + ACK clocking\n  else true                                       -- STOP framing\n\u27e9\n\n-- Serial data. START / data / ACK / STOP per the table above.\ndef sda : Signal defaultDomain Bool := \u27e8fun t =>\n  let bit := t / TPB\n  let off := t % TPB\n  if bit == 0 then off < TPH                     -- START: high then low\n  else if bit \u2265 1 \u2227 bit \u2264 8 then\n    addr.getLsbD (7 - (bit - 1))                 -- MSB first\n  else if bit == 9 then false                    -- slave ACK\n  else if bit == 10 then off < TPH               -- STOP: low then high\n  else false\n\u27e9\n\ndef sclSamples : List Bool := (List.range 88).map (fun t => scl.val t)\ndef sdaSamples : List Bool := (List.range 88).map (fun t => sda.val t)\n\n-- `Display.boolWave` ships with xeus-lean \u2014 render the two lanes on\n-- one shared time axis.\n#eval Display.boolWave [(\"SCL\", sclSamples), (\"SDA\", sdaSamples)] 5 28",
-   "metadata": {},
-   "execution_count": null,
-   "outputs": []
-  },
-  {
-   "cell_type": "markdown",
-   "id": "md-appendix",
-   "metadata": {},
-   "source": "## 7. Bonus: a real stateful counter via `circuit do`\n\nSparkle's `circuit do ... let count \u2190 Signal.reg 0#4 ; count <~ count + 1#4 ; return count` macro builds a stateful circuit through `Signal.loop`. Evaluating it from a notebook cell requires that the C FFI symbol `sparkle_eval_at` be reachable from the kernel; this image's `xlean` is linked against `libsparkle_barrier.a` (and the per-module Sparkle compiled objects) precisely so this works.\n\nThe cell below builds a 4-bit counter and samples it. `counter4.val 15 = 15` and `counter4.val 16 = 0` (BitVec wrap), and `#print axioms` confirms it depends on no axioms."
-  },
-  {
-   "cell_type": "code",
-   "execution_count": null,
-   "id": "code-appendix",
-   "metadata": {},
-   "outputs": [],
-   "source": "open Sparkle.Core.Domain Sparkle.Core.Signal\n\ndef counter4 : Signal defaultDomain (BitVec 4) :=\n  circuit do\n    let count \u2190 Signal.reg 0#4\n    count <~ count + 1#4\n    return count\n\n#print axioms counter4\n#eval (counter4.val 0).toNat        -- 0\n#eval (counter4.val 1).toNat        -- 1\n#eval (counter4.val 5).toNat        -- 5\n#eval (counter4.val 15).toNat       -- 15\n#eval (counter4.val 16).toNat       -- 0  (4-bit wrap)"
-  },
-  {
-   "cell_type": "markdown",
-   "id": "cc4c260d",
-   "source": "## 8. Notebook helpers \u2014 find a function, run a shell command, see the menu\n\nThe kernel ships a few notebook-friendly helpers in `Display`:\n\n* `#help_x` \u2014 list every `#`-command (or one specific command).\n* `#findDecl \"needle\"` \u2014 substring-search the active env. AND-mode + paging.\n* `#listNs SomeNamespace` \u2014 list declarations under a prefix.\n* `#sig name` \u2014 show one declaration's type signature.\n* `#bash \"cmd\"` \u2014 run a shell one-liner and dump output to the cell.\n\nThe cells below run each of these against the env we've already built.",
-   "metadata": {}
-  },
-  {
-   "cell_type": "code",
-   "id": "ffc39f6b",
-   "source": "#help_x",
-   "metadata": {},
-   "execution_count": null,
-   "outputs": []
-  },
-  {
-   "cell_type": "code",
-   "id": "c489b781",
-   "source": "-- Substring search across the active env. Two-keyword AND-mode finds\n-- only declarations whose name contains both \"Signal\" and \"register\".\n#findDecl \"Signal\" \"register\" 0 6",
-   "metadata": {},
-   "execution_count": null,
-   "outputs": []
-  },
-  {
-   "cell_type": "code",
-   "id": "d0a121ad",
-   "source": "-- One declaration's type signature.\n#sig Sparkle.Core.Signal.Signal.register",
-   "metadata": {},
-   "execution_count": null,
-   "outputs": []
-  },
-  {
-   "cell_type": "code",
-   "id": "c170e74f",
-   "source": "-- Shell one-liner. Works through `bash -c` so pipes/redirects are fine.\n#bash \"uname -a; date -u +%FT%TZ; ls /app/.lake/build/bin\"",
-   "metadata": {},
-   "execution_count": null,
-   "outputs": []
-  },
-  {
-   "cell_type": "markdown",
-   "id": "35f2c61b",
-   "source": "## 9. Sketch a datapath with `#mermaid`\n\nFor quick block-diagram sketches `#mermaid` is enough \u2014 it pulls\n`mermaid.js` from a CDN on first use and renders inline. Useful\nshapes for hardware diagrams:\n\n| Mermaid syntax | Meaning |\n| -------------- | ------- |\n| `[(R)]`        | register (cylinder) |\n| `>ALU]`        | combinational logic (flag) |\n| `[/in/]` `[\\out\\]` | I/O ports (parallelograms) |\n| `((1#4))`      | constant (circle) |\n| `-->`          | data wire (solid arrow) |\n| `-.->`         | clock wire (dashed arrow) |\n| `==>\\|n\\|`     | bus, with `n`-bit label |\n\nThe cell below shows the same pipelined datapath we'll build with the\nstructured emitter in section 10.",
-   "metadata": {}
-  },
-  {
-   "cell_type": "code",
-   "id": "421fc6b9",
-   "source": "#mermaid \"\nflowchart LR\n  IN[/in/]\n  R1[(R1)]\n  ALU>ALU]\n  R2[(R2)]\n  OUT[/out/]\n  CLK([CLK])\n  IN  --> R1\n  R1  --> ALU\n  ALU ==>|8| R2\n  R2  --> OUT\n  CLK -.-> R1\n  CLK -.-> R2\n  classDef clk fill:#fce4ec,stroke:#c2185b\n  class CLK clk\n\"",
-   "metadata": {},
-   "execution_count": null,
-   "outputs": []
-  },
-  {
-   "cell_type": "markdown",
-   "id": "7934a6f8",
-   "source": "## 10. Block-accurate hardware diagram with `Display.blockDiagram`\n\nWhen you want shapes Mermaid can't draw \u2014 trapezoid MUX, real cloud,\ncanonical AND/OR/NOT gate symbols, \u2295 adder \u2014 `Display.blockDiagram`\nemits a hand-laid SVG. Nodes carry their kind (`reg`, `mux`, `cloud`,\n`andG`, `orG`, `notG`, `adder`, `port`, `const`, `clk`, \u2026) and an\nexplicit `(col, row)` so layout is predictable.\n\nEdges are typed:\n\n* `.data`     \u2014 solid arrow\n* `.clock`    \u2014 pink dashed arrow (clock distribution)\n* `.bus n`    \u2014 thick arrow, labelled with the `n`-bit width",
-   "metadata": {}
-  },
-  {
-   "cell_type": "code",
-   "id": "964d9b68",
-   "source": "def myDP : Display.Diagram := {\n  nodes := [\n    { id := \"in\",  label := \"in\",  kind := .port,  col := 0, row := 0 },\n    { id := \"imm\", label := \"imm\", kind := .const, col := 0, row := 1 },\n    { id := \"CLK\", label := \"CLK\", kind := .clk,   col := 0, row := 2 },\n    { id := \"R1\",  label := \"R1\",  kind := .reg,   col := 1, row := 0 },\n    -- 2-input MUX: inputs := 2 spreads its left-edge pins, edges below\n    -- target M.0 and M.1 explicitly so the lines don't merge.\n    { id := \"M\",   label := \"MUX\", kind := .mux,   col := 2, row := 0, inputs := 2 },\n    { id := \"ALU\", label := \"ALU\", kind := .cloud, col := 3, row := 0 },\n    { id := \"R2\",  label := \"R2\",  kind := .reg,   col := 4, row := 0 },\n    { id := \"out\", label := \"out\", kind := .port,  col := 5, row := 0 }\n  ],\n  edges := [\n    { src := \"in\",  dst := \"R1\"  },\n    { src := \"R1\",  dst := \"M.0\" },\n    { src := \"imm\", dst := \"M.1\" },\n    { src := \"M\",   dst := \"ALU\" },\n    { src := \"ALU\", dst := \"R2\",  kind := .bus 8 },\n    { src := \"R2\",  dst := \"out\" },\n    -- Clock lines route through the rail at the bottom; they no longer\n    -- cross any data wire.\n    { src := \"CLK\", dst := \"R1\",  kind := .clock },\n    { src := \"CLK\", dst := \"R2\",  kind := .clock }\n  ]\n}\n\n#eval Display.blockDiagram myDP",
-   "metadata": {},
-   "execution_count": null,
-   "outputs": []
-  },
-  {
-   "cell_type": "markdown",
-   "id": "1401ec27",
-   "source": "## 11. Multi-million-tick VGA trace via `.wdb`\n\nFor traces too long to keep in memory (or send across the comm) we\nwrite a `.wdb` \u2014 xeus-lean's own per-block, zstd-compressed waveform\nformat. `Display.writeWdb` walks the lanes once, packs each batch of\n65 536 transitions into a zstd frame, and writes a tiny block index\non top. Reading is symmetric: `Display.waveformFromWdb` opens the\nfile and only decompresses the blocks that intersect the JS viewer's\ncurrent viewport.\n\nBelow we model 3 frames of VGA 640\u00d7480 timing \u2014 H_TOTAL = 800,\nV_TOTAL = 525, so 3 \u00d7 800 \u00d7 525 = 1 260 000 clocks. Three lanes:\nhorizontal sync, vertical sync, and display-enable (`de`). On disk\nthe result is roughly 22 KB (\u2248 50 \u00d7 smaller than the equivalent\ngzipped VCD). The viewer scrolls and zooms over the full 1.26 M\ntick range without ever materialising the whole trace.",
-   "metadata": {}
-  },
-  {
-   "cell_type": "code",
-   "id": "f9a7c965",
-   "source": "-- Build the 3 VGA sync lanes as plain Nat \u2192 Bool functions.\n-- H_TOTAL = 800, H_SYNC pulse = first 96 ticks\n-- V_TOTAL = 525, V_SYNC pulse = first 2 lines\n-- DE = active region 144 \u2264 h < 784, 35 \u2264 v < 515\ndef vgaLanes : List Display.WaveformSession.Lane := [\n  { name := \"hsync\", sample := fun t => (t % 800) \u2265 96 },\n  { name := \"vsync\", sample := fun t => ((t / 800) % 525) \u2265 2 },\n  { name := \"de\",    sample := fun t =>\n      let h := t % 800\n      let v := (t / 800) % 525\n      144 \u2264 h \u2227 h < 784 \u2227 35 \u2264 v \u2227 v < 515 }\n]\n\n-- 3 frames worth of clocks. Writing takes ~5 s (one Nat \u2192 Bool call\n-- per tick per lane); the resulting file is ~22 KB.\n#eval Display.writeWdb \"/tmp/vga.wdb\" vgaLanes 1260000\n\n-- Open it. Same interactive canvas as section 6/7; here it serves a\n-- 1.26 M-tick trace with no memory pressure.\n#eval Display.waveformFromWdb \"vga\" \"/tmp/vga.wdb\"",
-   "metadata": {},
-   "execution_count": null,
-   "outputs": []
-  }
- ],
- "metadata": {
-  "kernelspec": {
-   "display_name": "Lean 4",
-   "language": "lean4",
-   "name": "xlean"
-  },
-  "language_info": {
-   "name": "lean",
-   "file_extension": ".lean",
-   "mimetype": "text/x-haskell",
-   "pygments_lexer": "lean",
-   "codemirror_mode": "haskell"
-  }
- },
- "nbformat": 4,
- "nbformat_minor": 5
-}
\ No newline at end of file
diff --git a/scripts/smoke-test-sparkle.py b/scripts/smoke-test-sparkle.py
deleted file mode 100755
index 84a5e9a..0000000
--- a/scripts/smoke-test-sparkle.py
+++ /dev/null
@@ -1,117 +0,0 @@
-#!/usr/bin/env python3
-"""Sparkle-specific smoke test for the native xlean kernel.
-
-Runs after smoke-test-native.py inside Dockerfile.native-sparkle to
-prove that `import Sparkle` resolves and the core types kind-check.
-xeus-lean and Sparkle now pin the same Lean toolchain (4.28.0 final),
-so olean headers match and `Signal.circuit` macros are sorry-free —
-this test stays narrow on purpose, more elaborate simulation lives in
-the bundled `sparkle-native-demo.ipynb`.
-
-Exit codes:
-    0   import resolved + types kind-checked
-    1   kernel start failed
-    2   execute failed
-    3   output mismatch
-"""
-
-import sys
-import textwrap
-import time
-
-try:
-    from jupyter_client.manager import KernelManager
-except ImportError:
-    sys.stderr.write("ERROR: jupyter_client is not installed\n")
-    sys.exit(1)
-
-
-CELL = textwrap.dedent("""\
-    import Sparkle
-    open Sparkle.Core.Domain Sparkle.Core.Signal
-
-    -- Build a tiny stateful counter via Sparkle's `circuit do` DSL
-    -- and evaluate it. This exercises the full path: import resolves,
-    -- `Signal.reg` macro expands, the circuit goes through
-    -- `Signal.loop`, and the C FFI symbol `sparkle_eval_at` is
-    -- reachable from the interpreter (only true if xlean was relinked
-    -- against libsparkle_*.a). A regression on any of those layers
-    -- fails this single cell.
-    def counter4 : Signal defaultDomain (BitVec 4) :=
-      circuit do
-        let count <- Signal.reg 0#4
-        count <~ count + 1#4
-        return count
-
-    #eval IO.println s!"sparkle native: counter4(15)={(counter4.val 15).toNat}"
-""").replace('<-', '←')
-
-# `Signal.loop` runs through the IR interpreter and is slow — even
-# native takes a few seconds.
-TIMEOUT = 120.0
-
-
-def run(km, code):
-    kc = km.client()
-    kc.start_channels()
-    try:
-        kc.wait_for_ready(timeout=TIMEOUT)
-        msg_id = kc.execute(code)
-        outputs = []
-        deadline = time.monotonic() + TIMEOUT
-        while time.monotonic() < deadline:
-            try:
-                msg = kc.get_iopub_msg(timeout=1.0)
-            except Exception:
-                continue
-            if msg.get("parent_header", {}).get("msg_id") != msg_id:
-                continue
-            mtype = msg["msg_type"]
-            content = msg.get("content", {})
-            if mtype == "stream":
-                outputs.append(content.get("text", ""))
-            elif mtype == "execute_result":
-                outputs.append(str(content.get("data", {}).get("text/plain", "")))
-            elif mtype == "error":
-                outputs.append("\n".join(content.get("traceback", [])))
-            elif mtype == "status" and content.get("execution_state") == "idle":
-                return "".join(outputs)
-        raise TimeoutError("execute timed out")
-    finally:
-        kc.stop_channels()
-
-
-def main():
-    print("[sparkle-smoke] starting kernel: xlean", flush=True)
-    km = KernelManager(kernel_name="xlean")
-    try:
-        km.start_kernel()
-    except Exception as e:
-        sys.stderr.write(f"[sparkle-smoke] kernel start failed: {e}\n")
-        sys.exit(1)
-
-    try:
-        out = run(km, CELL)
-    except Exception as e:
-        sys.stderr.write(f"[sparkle-smoke] execute failed: {e}\n")
-        km.shutdown_kernel(now=True)
-        sys.exit(2)
-    finally:
-        try:
-            km.shutdown_kernel(now=True)
-        except Exception:
-            pass
-
-    needle = "sparkle native: counter4(15)=15"
-    if needle in out:
-        print(f"[sparkle-smoke] OK — output: {out.strip()[:200]}")
-        return
-    sys.stderr.write(
-        f"[sparkle-smoke] MISMATCH: expected substring {needle!r}\n"
-        f"  got: {out!r}\n"
-    )
-    sys.exit(3)
-
-
-if __name__ == "__main__":
-    main()
diff --git a/src/Convert.lean b/src/Convert.lean
index d11cef3..df6cef4 100644
--- a/src/Convert.lean
+++ b/src/Convert.lean
@@ -407,7 +407,7 @@ page wants to include the script; without the script the block is
 still readable, just monochrome).
 
 The Markdown→HTML renderer is intentionally minimal: just enough
-to render the Sparkle tutorial chapters cleanly. It covers:
+to render the tutorial chapters cleanly. It covers:
 
   * ATX headings `#`, `##`, …
   * fenced code blocks (already split out as separate cells, so
@@ -421,7 +421,7 @@ to render the Sparkle tutorial chapters cleanly. It covers:
 
 Anything more exotic (footnotes, definition lists, …) falls
 through as a literal paragraph. The chapters under
-`Verilean/sparkle/docs/tutorial/md/` do not use those features.
+`docs/tutorial/md/` (and downstream tutorial trees) do not use those features.
 -/
 
 /-- HTML-escape a string for embedding in text content. -/
diff --git a/src/Display.lean b/src/Display.lean
index 2fd3371..24df515 100644
--- a/src/Display.lean
+++ b/src/Display.lean
@@ -114,7 +114,7 @@ def svg (content : String) : IO Unit := emit "image/svg+xml" content
 def json (content : String) : IO Unit := emit "application/json" content
 
 /-- Pretty-print a `BitVec n` as a 3-row HTML table with binary, hex
-    and decimal renderings. Useful for sparkle / hardware notebooks
+    and decimal renderings. Useful for hardware-design notebooks
     where you want to eyeball the layout of a register or constant. -/
 def bv {n : Nat} (v : BitVec n) : IO Unit := do
   let dec := toString v.toNat
@@ -640,14 +640,14 @@ def bash (cmd : String) : IO Unit := do
 
 `#help_x` lists every notebook command currently registered with
 `Display.helpRegister`. The list is a global `IO.Ref` so other modules
-(Sparkle helpers, Hesper helpers, user-defined ones) can append their
+(downstream helpers, user-defined ones) can append their
 own entries without touching this file:
 
 ```lean
 import Display
 #eval Display.helpRegister {
   command  := "#bv"
-  category := "sparkle"
+  category := "hardware"
   brief    := "Show a BitVec literal in binary, hex, and decimal."
   example  := "#bv 0x42#8"
 }
@@ -659,7 +659,7 @@ alphabetically within each category.
 
 structure HelpEntry where
   command  : String   -- e.g. "#findDecl"
-  category : String   -- e.g. "search", "display", "waveform", "sparkle"
+  category : String   -- e.g. "search", "display", "waveform", "hardware"
   brief    : String   -- one-line description
   -- `usage` rather than `example` because the latter is a Lean keyword.
   usage    : String   -- one-line usage snippet
@@ -1922,7 +1922,7 @@ def waveformFromVCDFile (sessionId : String) (path : String) : IO Unit := do
 `#findDecl "Signal.reg"`         — first 10 matches, case-insensitive substring
 `#findDecl "Signal" "reg"`       — AND search across multiple keywords
 `#findDecl "Signal.reg" 10 20`   — page: skip 10, take 20
-`#listNs Sparkle.Core.Signal`    — declarations whose name starts with that prefix
+`#listNs Foo.Bar`    — declarations whose name starts with that prefix
 `#sig Signal.register`           — single declaration's type signature
 
 The walks the active `Lean.Environment` and filters in O(env-size); current
@@ -2062,7 +2062,7 @@ elab "#findDecl " kws:(str)+ skipTk:(num)? takeTk:(num)? : command => do
   liftCoreM <| Display.emit "text/html" html
 
 open Lean Lean.Elab Lean.Elab.Command Lean.Meta in
-/-- `#listNs Sparkle.Core.Signal skipN? takeN?` — list declarations whose
+/-- `#listNs Foo.Bar skipN? takeN?` — list declarations whose
     fully-qualified name starts with the given namespace prefix. -/
 elab "#listNs " ns:ident skipTk:(num)? takeTk:(num)? : command => do
   let prefixStr := ns.getId.toString
@@ -2135,7 +2135,7 @@ macro "#mermaid " s:str : command => `(#eval Display.mermaid $s)
 /-! ### Built-in help entries
 
 These register on `import Display`. New entries from other modules
-(`SparkleHelp`, future `HesperHelp`, …) call `Display.helpRegister` at
+(downstream registries — `MyLibHelp`, etc.) call `Display.helpRegister` at
 their own initialise time, so users only need to `import` the helper
 module they care about and `#help_x` will pick up the new commands. -/
 
@@ -2164,7 +2164,7 @@ private def builtinHelp : Array Display.HelpEntry := #[
     usage := "#mermaid \"flowchart LR\\n  IN --> R1[(R1)] --> ALU>ALU] --> R2[(R2)] --> OUT\\n  CLK -.-> R1 & R2\"" },
   { command := "Display.verilog", category := "display",
     brief := "Pretty-print a SystemVerilog source string with Highlight.js syntax coloring (CDN-loaded github theme).",
-    usage := "#eval Display.verilog (Sparkle.Backend.Verilog.toVerilog m)" },
+    usage := "#eval Display.verilog \"module dff (...); ...\"" },
   { command := "#blockDiagram", category := "display",
     brief := "Structured HW block diagram (port/reg/mux/cloud/box/andG/orG/notG/adder/const/clk + data/clock/bus edges). Trapezoid MUX, real cloud, gate symbols — shapes Mermaid can't do. Layout uses col/row fields on each node.",
     usage := "#eval Display.blockDiagram { nodes := [...], edges := [...] }" },
@@ -2182,7 +2182,7 @@ private def builtinHelp : Array Display.HelpEntry := #[
     usage := "#findDecl \"Signal\" \"register\" 0 10" },
   { command := "#listNs",   category := "search",
     brief := "List declarations under a namespace prefix.",
-    usage := "#listNs Sparkle.Core.Signal" },
+    usage := "#listNs Foo.Bar" },
   { command := "#sig",      category := "search",
     brief := "Show one declaration's type signature.",
     usage := "#sig Nat.succ" },
diff --git a/src/REPL/Frontend.lean b/src/REPL/Frontend.lean
index e6aaaef..d05e5fc 100644
--- a/src/REPL/Frontend.lean
+++ b/src/REPL/Frontend.lean
@@ -92,50 +92,72 @@ def processInput (input : String) (cmdState? : Option Command.State)
   IO.eprintln "[processInput] initSearchPath done"
   enableInitializersExecution
   let fileName   := fileName.getD "<input>"
-  -- Auto-import Display (and, when present, Sparkle / Hesper) on the
-  -- first cell. Why: the Lean REPL only allows `import` at the very
+  -- Auto-import Display + any extras the deployment declared on the
+  -- first cell.  Why: the Lean REPL only allows `import` at the very
   -- start of a "file", and each cell after the first reuses the prior
   -- cmdState — so once any cell has run, the user can no longer
-  -- import anything. We pre-inject the imports that ship with the
-  -- kernel so `#help_x`, `Display.html`, etc. work without the user
+  -- import anything.  We pre-inject the imports the kernel ships
+  -- with so `#help_x`, `Display.html`, etc. work without the user
   -- having to remember to put `import Display` in cell 1.
   --
   -- The auto-import only runs when `cmdState?` is `none` (i.e. the
-  -- very first cell). User code in that cell still runs after the
-  -- imports — anything the user typed is concatenated.
+  -- very first cell).  User code in that cell still runs after the
+  -- imports.
   --
-  -- WASM gates each pre-import on the olean being in the embedded
-  -- VFS (because trimmed-down WASM kernels may drop Sparkle/Hesper).
-  -- Native always ships Display via lean-toolchain, but Sparkle and
-  -- Hesper may be absent in the base image; gate those by checking
-  -- their olean path in the build's lean search path.
+  -- Extension: a downstream lib (anything shipped via EXTRA_WASM_DIRS)
+  -- registers its own auto-imports by writing one module name per
+  -- line into a file under one of these names somewhere on the
+  -- search path:
+  --
+  --     /lib/lean/.xeus-auto-imports          (WASM VFS)
+  --     <root>/.xeus-auto-imports             (each native search root)
+  --
+  -- Lines starting with `#` and blank lines are ignored.  Each
+  -- listed module is imported only if its olean is actually
+  -- present (so an outdated registry doesn't fail elaboration).
+  -- xeus-lean itself names no third-party module — they appear
+  -- only inside the .xeus-auto-imports file the third-party build
+  -- script writes.
   let input ←
     if cmdState?.isNone then do
-      let imports ← if isWasm then do
-        let hasSparkle ← (System.FilePath.mk "/lib/lean/Sparkle.olean").pathExists
-        let hasHesper  ← (System.FilePath.mk "/lib/lean/Hesper/WGSL/DSL.olean").pathExists
-        pure <|
-          "import Display\n"
-          ++ (if hasSparkle then "import Sparkle\n" else "")
-          ++ (if hasHesper  then "import Hesper.WGSL.DSL\n" else "")
-      else do
-        -- Probe for each module via LEAN_PATH (set by the kernelspec).
-        -- A module foo.bar.Baz lives at <root>/foo/bar/Baz.olean for
-        -- some root in LEAN_PATH; if none of those roots has the
-        -- file, the module isn't available and we skip its import.
-        let leanPath ← Lean.searchPathRef.get
-        let probe (rel : System.FilePath) : IO Bool := do
-          for root in leanPath do
-            if (← (root / rel).pathExists) then return true
-          return false
-        let hasDisplay ← probe ("Display.olean" : System.FilePath)
-        let hasSparkle ← probe ("Sparkle.olean" : System.FilePath)
-        let hasHesper  ← probe (("Hesper" : System.FilePath) / "WGSL" / "DSL.olean")
-        pure <|
-          (if hasDisplay then "import Display\n" else "")
-          ++ (if hasSparkle then "import Sparkle\n" else "")
-          ++ (if hasHesper  then "import Hesper.WGSL.DSL\n" else "")
-      pure (imports ++ input)
+      -- 1. Compute the list of search roots to probe.  WASM uses the
+      --    fixed /lib/lean prefix because LEAN_PATH isn't populated
+      --    from the kernelspec there; native uses the search path.
+      let roots ← if isWasm then
+        pure [System.FilePath.mk "/lib/lean"]
+      else
+        Lean.searchPathRef.get
+      let oleanExists (mod : String) : IO Bool := do
+        let rel : System.FilePath := System.FilePath.mk (mod.replace "." "/" ++ ".olean")
+        for root in roots do
+          if (← (root / rel).pathExists) then return true
+        return false
+      -- 2. Always-on auto-import is just Display.  Anything else is
+      --    sourced from .xeus-auto-imports registries.
+      let coreImports := if (← oleanExists "Display") then "import Display\n" else ""
+      -- 3. Read each .xeus-auto-imports file under the search roots
+      --    and collect distinct module names.
+      let mut extras : List String := []
+      let mut seen : Std.HashSet String := {}
+      for root in roots do
+        let registry := root / ".xeus-auto-imports"
+        if ← registry.pathExists then
+          let body ← IO.FS.readFile registry
+          for line in body.splitOn "\n" do
+            let line := line.trim
+            if line.isEmpty || line.startsWith "#" then continue
+            if seen.contains line then continue
+            seen := seen.insert line
+            extras := extras ++ [line]
+      -- 4. Drop registry entries whose olean is missing — keeps a
+      --    stale list from breaking the first cell.
+      let mut extraImports := ""
+      for mod in extras do
+        if ← oleanExists mod then
+          extraImports := extraImports ++ s!"import {mod}\n"
+        else
+          IO.eprintln s!"[processInput] .xeus-auto-imports: skipping `{mod}` (olean not found)"
+      pure (coreImports ++ extraImports ++ input)
     else
       pure input
   let inputCtx   := Parser.mkInputContext input fileName
@@ -149,12 +171,13 @@ def processInput (input : String) (cmdState? : Option Command.State)
     let initOlean := System.FilePath.mk "/lib/lean/Init.olean"
     let initDir := System.FilePath.mk "/lib/lean/Init"
     let initOleanExists ← initOlean.pathExists
-    -- Check additional modules
+    -- Check core modules (Std/Lean/Display).  Anything else lives
+    -- under a third-party search root and isn't worth a diagnostic
+    -- here — the auto-import block above already logged misses.
     let stdOlean ← (System.FilePath.mk "/lib/lean/Std.olean").pathExists
     let leanOlean ← (System.FilePath.mk "/lib/lean/Lean.olean").pathExists
-    let sparkleOlean ← (System.FilePath.mk "/lib/lean/Sparkle.olean").pathExists
     let displayOlean ← (System.FilePath.mk "/lib/lean/Display.olean").pathExists
-    IO.eprintln s!"[processInput] Std.olean={stdOlean} Lean.olean={leanOlean} Sparkle.olean={sparkleOlean} Display.olean={displayOlean}"
+    IO.eprintln s!"[processInput] Std.olean={stdOlean} Lean.olean={leanOlean} Display.olean={displayOlean}"
     let initDirExists ← initDir.isDir
     IO.eprintln s!"[processInput] /lib/lean/Init.olean exists={initOleanExists}, /lib/lean/Init isDir={initDirExists}"
     let sp ← Lean.searchPathRef.get
diff --git a/src/WasmRepl.lean b/src/WasmRepl.lean
index eca503d..b5d647b 100644
--- a/src/WasmRepl.lean
+++ b/src/WasmRepl.lean
@@ -76,7 +76,14 @@ def execute (stateRef : IO.Ref REPL.State) (code : String) (envId : UInt32) (has
   -- because Lean 4.28's #eval stdout capture (withIsolatedStreams)
   -- does not work in WASM.
   let displayOutput ← Display.drain
-  IO.eprintln s!"[WasmRepl] displayOutput='{displayOutput.take 200}' len={displayOutput.length}"
+  -- NB: do NOT inline `displayOutput` into the diagnostic — it can
+  -- contain MIME envelopes (raw 0x1B / 0x1E), and the WASM
+  -- `Module.printErr` shim treats any line carrying `\x1bMIME:` as
+  -- user-visible cell output.  Logging the envelope here once made
+  -- the SVG / HTML / LaTeX previews vanish under a duplicate copy
+  -- of the same marker on every cell, which broke the Playwright
+  -- `#svg embeds an SVG` test.  Keep the diagnostic length-only.
+  IO.eprintln s!"[WasmRepl] displayOutput len={displayOutput.length}"
 
   match result with
   | (.inl response, newState) =>
diff --git a/src/pre.js b/src/pre.js
index 28f8a58..b97dc39 100644
--- a/src/pre.js
+++ b/src/pre.js
@@ -5,3 +5,43 @@ Module.preRun.push(() => {
   ENV.LEAN_PATH = "/lib/lean";
   ENV.LEAN_SYSROOT = "/";
 });
+
+// Capture WASM stdout so xinterpreter_wasm.cpp can drain it at the
+// end of each execute_request and route it through the same MIME /
+// publish pipeline the native kernel uses.  Without this hook
+// emscripten's default `Module.print` would route IO.println straight
+// to console.log — invisible to the notebook cell.
+//
+// This is the WASM analogue of `xeus_ffi.cpp`'s dup2-based fd-1 pipe.
+// See https://github.com/Verilean/xeus-lean/issues/11.
+//
+// stderr is treated differently: most of what the runtime writes to
+// it is `[WasmRepl] …` / `[WASM] …` instrumentation that's only
+// useful in the DevTools console.  Capturing it like stdout would
+// flood every cell's output area and drown out the rich-display
+// payload that arrives a frame later — empirically that broke the
+// Playwright `#svg embeds an SVG` test even though the SVG payload
+// itself was emitted correctly.  Tag a line with the MIME envelope
+// (Display.* / `#showVerilog` etc.) if you genuinely need it in the
+// notebook cell; everything else goes to console.error so it stays
+// visible to a developer without leaking into user-visible output.
+Module._xleanStdoutBuf = '';
+Module._xleanStderrBuf = '';
+Module.print = function (text) {
+  if (arguments.length > 1) {
+    text = Array.prototype.slice.call(arguments).join(' ');
+  }
+  Module._xleanStdoutBuf += text + '\n';
+};
+Module.printErr = function (text) {
+  if (arguments.length > 1) {
+    text = Array.prototype.slice.call(arguments).join(' ');
+  }
+  if (text && text.indexOf('\x1bMIME:') !== -1) {
+    Module._xleanStderrBuf += text + '\n';
+  } else {
+    if (typeof console !== 'undefined' && console.error) {
+      console.error(text);
+    }
+  }
+};
diff --git a/src/xinterpreter_wasm.cpp b/src/xinterpreter_wasm.cpp
index 04066ee..73eb58a 100644
--- a/src/xinterpreter_wasm.cpp
+++ b/src/xinterpreter_wasm.cpp
@@ -400,6 +400,70 @@ EM_JS(int, xlean_load_fail_msg_to, (char* buf, int max_bytes), {
     stringToUTF8(s, Number(buf), max_bytes);
     return n;
 });
+
+// Drain Module._xleanStdoutBuf (populated by the Module.print hook
+// in pre.js) into a caller-allocated buffer.  Returns the number of
+// UTF-8 bytes written, or -1 if the JS buffer doesn't fit; caller
+// must drain in a loop until 0 is returned.  Resets the JS buffer
+// in the same step so a partial-drain followed by a fresh write
+// doesn't lose new bytes.
+//
+// See https://github.com/Verilean/xeus-lean/issues/11 for context.
+EM_JS(int, xlean_drain_stdout_to, (char* buf, int max_bytes), {
+    var s = Module._xleanStdoutBuf || '';
+    if (!s) return 0;
+    var n = lengthBytesUTF8(s);
+    if (n + 1 > max_bytes) {
+        // Move just the head into the buffer and stash the rest;
+        // the next drain() call will pick the rest up.  Splitting
+        // bytewise is unsafe — we'd cut a multi-byte UTF-8 sequence
+        // — so split on the last newline that fits.  IO.println
+        // emits one whole line per call, so an internal newline is
+        // always present unless someone wrote raw bytes.
+        var fitChars = max_bytes - 1;
+        var head = s.substring(0, fitChars);
+        var cut = head.lastIndexOf('\n');
+        if (cut < 0) {
+            // Single line bigger than max_bytes; truncate at fitChars
+            // (this may corrupt a UTF-8 codepoint, accept the loss).
+            head = s.substring(0, fitChars);
+            Module._xleanStdoutBuf = s.substring(fitChars);
+        } else {
+            head = s.substring(0, cut + 1);
+            Module._xleanStdoutBuf = s.substring(cut + 1);
+        }
+        var hn = lengthBytesUTF8(head);
+        stringToUTF8(head, Number(buf), max_bytes);
+        return hn;
+    }
+    Module._xleanStdoutBuf = '';
+    stringToUTF8(s, Number(buf), max_bytes);
+    return n;
+});
+
+EM_JS(int, xlean_drain_stderr_to, (char* buf, int max_bytes), {
+    var s = Module._xleanStderrBuf || '';
+    if (!s) return 0;
+    var n = lengthBytesUTF8(s);
+    if (n + 1 > max_bytes) {
+        var fitChars = max_bytes - 1;
+        var head = s.substring(0, fitChars);
+        var cut = head.lastIndexOf('\n');
+        if (cut < 0) {
+            head = s.substring(0, fitChars);
+            Module._xleanStderrBuf = s.substring(fitChars);
+        } else {
+            head = s.substring(0, cut + 1);
+            Module._xleanStderrBuf = s.substring(cut + 1);
+        }
+        var hn = lengthBytesUTF8(head);
+        stringToUTF8(head, Number(buf), max_bytes);
+        return hn;
+    }
+    Module._xleanStderrBuf = '';
+    stringToUTF8(s, Number(buf), max_bytes);
+    return n;
+});
 #endif
 
 #ifdef __EMSCRIPTEN__
@@ -733,6 +797,57 @@ void interpreter::execute_request_impl(send_reply_callback cb,
             }
         }
 
+#ifdef __EMSCRIPTEN__
+        // Drain any IO.println / fprintf(stderr) that ran during elab.
+        // pre.js redirects Module.print(/Err) into JS-side buffers; we
+        // pull them here so the same `extract_mime_payloads` path
+        // handles Sparkle's `#showVerilog → IO.println MIME` etc.
+        // Mirrors xeus_ffi.cpp's dup2 capture on the native kernel.
+        {
+            std::string stdout_captured;
+            static char drain_buf[64 * 1024];
+            for (int safety = 0; safety < 64; ++safety) {
+                int n = xlean_drain_stdout_to(drain_buf, sizeof(drain_buf));
+                if (n <= 0) break;
+                stdout_captured.append(drain_buf, drain_buf + n);
+            }
+            if (!stdout_captured.empty()) {
+                std::string plain;
+                extract_mime_payloads(stdout_captured, mime_bundle, plain);
+                if (!plain.empty()) {
+                    // Prepend stdout's plain text to the rendered
+                    // messages so the order matches what a native
+                    // `lean --run` user would see on a tail of stdout.
+                    std::string prefix = plain;
+                    // IO.println always tacks on a trailing newline,
+                    // but text/plain rendering doesn't need it.
+                    while (!prefix.empty() && prefix.back() == '\n') {
+                        prefix.pop_back();
+                    }
+                    if (!prefix.empty()) {
+                        if (pub_data.contains("text/plain")) {
+                            std::string old = pub_data["text/plain"]
+                                .get<std::string>();
+                            pub_data["text/plain"] = prefix + "\n" + old;
+                        } else {
+                            pub_data["text/plain"] = prefix;
+                        }
+                    }
+                }
+            }
+
+            std::string stderr_captured;
+            for (int safety = 0; safety < 64; ++safety) {
+                int n = xlean_drain_stderr_to(drain_buf, sizeof(drain_buf));
+                if (n <= 0) break;
+                stderr_captured.append(drain_buf, drain_buf + n);
+            }
+            if (!stderr_captured.empty()) {
+                publish_stream("stderr", stderr_captured);
+            }
+        }
+#endif
+
         // Publish rich-display payloads first so they appear above the
         // plain-text result in the notebook (matches IPython ordering).
         if (!mime_bundle.empty()) {
diff --git a/test_wasm_node.cpp b/test_wasm_node.cpp
index 5f41b1f..2edee1d 100644
--- a/test_wasm_node.cpp
+++ b/test_wasm_node.cpp
@@ -8,6 +8,7 @@
 #include <unordered_set>
 #include <unordered_map>
 #include <stdexcept>
+#include <sys/stat.h>
 #include <lean/lean.h>
 
 #ifdef __EMSCRIPTEN__
@@ -348,6 +349,41 @@ int main() {
         }
     };
 
+    // run_cmd_expect — like run_cmd but asserts that `needle` appears
+    // somewhere in the JSON result (which is what
+    // `lean_wasm_repl_execute` returns).  Used for the
+    // mock-extra-fixture check below where we need a hard contract
+    // failure to fail the WASM build, not just a noisy stderr.
+    auto run_cmd_expect = [&](const char* desc, const char* code_str,
+                              const char* needle,
+                              uint32_t env_id = 0, uint8_t has_env = 0) -> bool {
+        std::cerr << "[TEST] Execute (expect '" << needle << "'): '" << desc << "'" << std::endl;
+        try {
+            lean_object* code = lean_mk_string(code_str);
+            lean_inc(state_ref);
+            lean_object* res = lean_wasm_repl_execute(state_ref, code, env_id, has_env);
+            if (lean_io_result_is_error(res)) {
+                std::cerr << "[TEST] FAILED: lean_wasm_repl_execute" << std::endl;
+                lean_io_result_show_error(res);
+                lean_dec(res);
+                return false;
+            }
+            lean_object* result = lean_io_result_get_value(res);
+            const char* result_str = lean_string_cstr(result);
+            std::cerr << "[TEST] Result: " << (result_str ? result_str : "(null)") << std::endl;
+            bool ok = result_str && std::string(result_str).find(needle) != std::string::npos;
+            if (!ok) {
+                std::cerr << "[TEST] FAILED: expected '" << needle
+                          << "' in result" << std::endl;
+            }
+            lean_dec(res);
+            return ok;
+        } catch (const std::exception& e) {
+            std::cerr << "[TEST] EXCEPTION: " << e.what() << std::endl;
+            return false;
+        }
+    };
+
     // Stress test: WasmRepl auto-chains hasEnv=0 calls on the latest env so
     // processHeader runs only once, working around the WASM 5th-fresh-import
     // bug. Run many calls to verify the env-reuse path is stable.
@@ -400,47 +436,44 @@ int main() {
     run_cmd("#eval unsafeIO (do let r ← IO.mkRef (0 : Nat); r.set 42; return (← r.get))",
             "#eval unsafeIO (do let r ← IO.mkRef (0 : Nat); r.set 42; return (← r.get))");
 
-    // Sparkle tests — auto-imported on first call by Frontend.lean.
-    // No `import Sparkle` line here because env-reuse means imports only
-    // fire on the first call.
-    std::cerr << "\n[TEST] === Sparkle Simulation Tests ===" << std::endl;
-
-    std::cerr << "[TEST] Step 11a: simple eval (Sparkle is auto-imported)" << std::endl;
-    run_cmd("Sparkle eval",
-            "#eval IO.println \"sparkle: ok\"");
-
-    std::cerr << "[TEST] Step 11b: Signal.const + sample" << std::endl;
-    run_cmd("Signal.const sample",
-            "open Sparkle.Core.Domain Sparkle.Core.Signal\n"
-            "def s : Signal defaultDomain (BitVec 4) := \xe2\x9f\xa8" "fun _ => 7#4" "\xe2\x9f\xa9\n"
-            "#eval IO.println s!\"sparkle: {s.sample 1}\"");
-
-    std::cerr << "[TEST] Step 11c: Signal.register (no feedback)" << std::endl;
-    run_cmd("Signal.register",
-            "open Sparkle.Core.Domain Sparkle.Core.Signal\n"
-            "def r := Signal.register 5#4 " "\xe2\x9f\xa8" "fun _ => 9#4" "\xe2\x9f\xa9\n"
-            "#eval IO.println s!\"sparkle: {r.sample 2}\"");
-
-    std::cerr << "[TEST] Step 11d: Signal.loop (feedback - THE hang test)" << std::endl;
-    run_cmd("Signal.loop",
-            "open Sparkle.Core.Domain Sparkle.Core.Signal\n"
-            "def counter := Signal.loop (fun s => Signal.register 0#4 (s.map (\xc2\xb7 + 1#4)))\n"
-            "#eval IO.println s!\"sparkle: {counter.val 0}\"");
-
-    // Hesper WGSL DSL tests — Hesper.WGSL.DSL is auto-imported by Frontend
-    // when /lib/lean/Hesper/WGSL/DSL.olean exists in the VFS.
-    // Phase 1 of the Hesper integration: pure-Lean WGSL DSL, no FFI.
-    std::cerr << "\n[TEST] === Hesper WGSL DSL Tests ===" << std::endl;
-
-    std::cerr << "[TEST] Step 12a: Hesper namespace available" << std::endl;
-    run_cmd("Hesper namespace",
-            "#eval IO.println \"hesper: ok\"");
-
-    std::cerr << "[TEST] Step 12b: build a small Exp and toWGSL it" << std::endl;
-    run_cmd("Hesper.WGSL Exp",
-            "open Hesper.WGSL\n"
-            "def e : Exp (.scalar .f32) := Exp.var \"x\"\n"
-            "#eval IO.println s!\"hesper: {e.toWGSL}\"");
+    // === EXTRA_WASM_DIRS contract test: the mock-extra fixture ===
+    //
+    // When the WASM build was configured with
+    //   -DEXTRA_WASM_DIRS=tests/fixtures/mock-extra/staging
+    // (CI's wasm-build job does this), CMake whole-archives
+    // libmock_extra_wasm.a into xlean, stages MockExtra.olean into the
+    // VFS, and registers MockExtra in the kernel's .xeus-auto-imports.
+    // This step exercises the whole chain: import resolution, dlsym
+    // lookup of the C extern, the Lean call into C, and the C->Lean
+    // string return value.
+    //
+    // The Dockerfile.docs-builder smoke-test path does NOT pass
+    // EXTRA_WASM_DIRS, so MockExtra.olean is absent from this binary's
+    // embedded VFS.  Detect that and skip the assertion — the contract
+    // is exercised by the wasm-build CI job, not by smoke-testing the
+    // docs-builder image.
+    std::cerr << "\n[TEST] === EXTRA_WASM_DIRS contract (mock-extra fixture) ===" << std::endl;
+
+    struct stat st;
+    if (stat("/lib/lean/MockExtra.olean", &st) != 0) {
+        std::cerr << "[TEST] SKIP: /lib/lean/MockExtra.olean not in VFS — "
+                     "this binary was built without EXTRA_WASM_DIRS pointing "
+                     "at tests/fixtures/mock-extra.  The contract is covered "
+                     "by the wasm-build CI job instead." << std::endl;
+    } else {
+        bool mock_extra_ok = run_cmd_expect(
+            "MockExtra.mockHello ()",
+            "#eval IO.println (MockExtra.mockHello ())",
+            "hello from mock-extra");
+
+        if (!mock_extra_ok) {
+            std::cerr << "[TEST] FAILED: mock-extra fixture didn't return the "
+                         "expected string.  EXTRA_WASM_DIRS contract is broken; "
+                         "downstream Lean libs cannot rely on it." << std::endl;
+            lean_dec(state_ref);
+            return 1;
+        }
+    }
 
     std::cerr << "[TEST] All steps completed successfully!" << std::endl;
     lean_dec(state_ref);
diff --git a/tests/e2e/jupyter.ts b/tests/e2e/jupyter.ts
index 62607cb..1ba9016 100644
--- a/tests/e2e/jupyter.ts
+++ b/tests/e2e/jupyter.ts
@@ -18,7 +18,7 @@ const KERNEL_BOOT_TIMEOUT = 300_000;
 // Cells that hit `import` paths (and therefore a fresh
 // `processInput` → `processHeader` → `importModulesCore`) can take
 // 30-60 s on the GitHub Actions runner where memory pressure from
-// the loaded Std/Lean/Sparkle/Hesper olean trees hurts kernel
+// the loaded Std/Lean olean trees hurts kernel
 // throughput. Locally the same cells finish in 1-2 s, but in CI we
 // have seen `#latex` exceed 60 s. Three minutes is generous enough
 // to absorb that without masking real hangs.
@@ -126,7 +126,14 @@ export async function runCell(page: Page, source: string): Promise<Locator> {
   await page.keyboard.press('Shift+Enter');
 
   // Wait for the output area under the just-run cell.
-  const output = cell.locator('.jp-OutputArea-output').first();
+  //
+  // Use the *container* (`.jp-OutputArea`) rather than the first
+  // individual `.jp-OutputArea-output` element: a single cell can
+  // emit several outputs in sequence (stderr stream first, rich
+  // display widget second), and tests that look for `svg` / `img`
+  // inside the rich payload would miss it if we narrowed to the
+  // stream output that happens to arrive first.
+  const output = cell.locator('.jp-OutputArea').first();
   await output.waitFor({ state: 'visible', timeout: CELL_EXEC_TIMEOUT });
 
   // Wait for kernel to go idle again before moving on.
diff --git a/tests/e2e/rich-display.spec.ts b/tests/e2e/rich-display.spec.ts
index 2e1d395..17ee09c 100644
--- a/tests/e2e/rich-display.spec.ts
+++ b/tests/e2e/rich-display.spec.ts
@@ -63,8 +63,13 @@ test.describe.serial('rich display', () => {
       String.raw`#latex "\\int_0^1 x^2 \\, dx = \\frac{1}{3}"`
     );
     await assertNoError(output);
+    // Both the outer `.jp-RenderedLatex` widget and the
+    // MathJax-typed `mjx-container` inside it satisfy the
+    // selector, so `.first()` it explicitly — toBeVisible with
+    // a non-strict locator would still pass, but the test reads
+    // more honestly as "at least one of these renders".
     await expect(
-      output.locator('mjx-container, .MathJax, .jp-RenderedLatex')
+      output.locator('mjx-container, .MathJax, .jp-RenderedLatex').first()
     ).toBeVisible();
   });
 
@@ -76,7 +81,7 @@ test.describe.serial('rich display', () => {
     await assertNoError(output);
     // SVG may be rendered inline or wrapped in an <img> tag depending
     // on JupyterLab's MIME renderer. Accept either form.
-    await expect(output.locator('svg, img')).toBeVisible();
+    await expect(output.locator('svg, img').first()).toBeVisible();
   });
 
   test('#eval do loop with Display.latex', async () => {
@@ -125,80 +130,13 @@ test.describe.serial('rich display', () => {
       '#eval Display.waveform "clk" [0,1,0,1,0,1,0,1] (bitWidth := 1) (cellW := 30) (height := 60)'
     );
     // Should produce an SVG with a path element (the waveform line)
-    await expect(output.locator('svg, img')).toBeVisible();
+    await expect(output.locator('svg, img').first()).toBeVisible();
   });
 });
 
-/**
- * Sparkle HDL tests. These run in a separate kernel session because
- * `import Sparkle` must be in the first cell (REPL only processes
- * imports in the initial header). Loading 26 Sparkle modules takes
- * extra time.
- */
-test.describe.serial('sparkle hdl', () => {
-  let sparklePage: Page;
-
-  test.beforeAll(async ({ browser }) => {
-    test.setTimeout(600_000);
-    sparklePage = await browser.newPage();
-    // Open sparkle-demo.ipynb which has `import Sparkle` in the first cell
-    await openLeanNotebook(sparklePage, 'sparkle-demo.ipynb');
-  });
-
-  test.afterAll(async () => {
-    await sparklePage?.close();
-  });
-
-  test('Sparkle counter simulation + waveform', async () => {
-    // Capture WASM stderr logs for debugging
-    const logs: string[] = [];
-    sparklePage.on('console', (msg) => {
-      const text = msg.text();
-      if (text.includes('processInput') || text.includes('headerMsg') ||
-          text.includes('Sparkle') || text.includes('error') ||
-          text.includes('import') || text.includes('WasmRepl') ||
-          text.includes('searchPath') || text.includes('not found')) {
-        logs.push(`[${msg.type()}] ${text}`);
-      }
-    });
-
-    // Also capture ALL console messages to a separate list for post-mortem.
-    const allLogs: string[] = [];
-    sparklePage.on('console', (msg) => {
-      allLogs.push(`[${msg.type()}] ${msg.text()}`);
-    });
-
-    const cells = sparklePage.locator('.jp-Notebook .jp-CodeCell');
-    const cell = cells.first();
-    const editor = cell.locator('.cm-content').first();
-    await editor.click();
-    await sparklePage.keyboard.press('Shift+Enter');
-
-    // Wait for output. Sparkle import takes minutes on first run because
-    // 7000+ .olean files are fetched lazily from the JupyterLite server.
-    test.setTimeout(600_000);
-    const output = cell.locator('.jp-OutputArea-output').first();
-    try {
-      await output.waitFor({ state: 'visible', timeout: 540_000 });
-    } catch (e) {
-      // Dump ALL WASM logs on timeout so we can see where it hung.
-      console.log('=== TIMEOUT — dumping ALL console logs ===');
-      for (const log of allLogs.slice(-200)) {
-        console.log(log);
-      }
-      throw e;
-    }
-
-    // Dump WASM REPL logs
-    console.log('=== WASM REPL debug logs ===');
-    for (const log of logs) {
-      console.log(log);
-    }
-
-    // Dump output text
-    const text = await output.textContent();
-    console.log(`=== Output (first 500 chars) ===\n${text?.substring(0, 500)}`);
-
-    await expect(output).toContainText('counter:');
-  });
-});
+// Third-party-Lean-lib HDL/display tests (formerly `sparkle hdl`)
+// have been removed: xeus-lean no longer bundles a specific HDL
+// library, and the EXTRA_WASM_DIRS contract is exercised by
+// `tests/fixtures/mock-extra/` + the native `test_wasm_node`
+// step, not via Playwright.  Downstream repos that ship their
+// own Lean lib own their own Playwright suites.
diff --git a/tests/fixtures/mock-extra/.gitignore b/tests/fixtures/mock-extra/.gitignore
new file mode 100644
index 0000000..102c00d
--- /dev/null
+++ b/tests/fixtures/mock-extra/.gitignore
@@ -0,0 +1,3 @@
+.lake/
+.cache/
+build-wasm/
diff --git a/tests/fixtures/mock-extra/MockExtra.lean b/tests/fixtures/mock-extra/MockExtra.lean
new file mode 100644
index 0000000..99e2197
--- /dev/null
+++ b/tests/fixtures/mock-extra/MockExtra.lean
@@ -0,0 +1,32 @@
+/-!
+# MockExtra — reference fixture for xeus-lean's EXTRA_WASM_DIRS path
+
+This is intentionally trivial: a single `@[extern]` declaration whose
+implementation lives in `c_src/mock_extra_hello.c`.  It exercises:
+
+- a `lake build` producing the olean tree
+- a C extern that the WASM xlean kernel must resolve at link time
+- the `xeus-lean-extra.json` manifest schema (written by
+  `build-wasm.sh`)
+
+If a downstream Lean library can plug into xlean the same way this
+fixture does, the contract is satisfied.
+
+The CI step `Build mock-extra fixture` builds this into a staging
+directory and passes it via `-DEXTRA_WASM_DIRS=…`; `test_wasm_node`
+then asserts that a Lean cell evaluating `MockExtra.mockHello ()`
+returns the expected string.
+-/
+
+namespace MockExtra
+
+/-- The greeting string the WASM test rig expects to see. -/
+@[extern "mock_extra_hello"]
+opaque mockHello : Unit → String
+
+/-- Convenience wrapper so `IO.println (← MockExtra.greeting)` reads
+    naturally inside a notebook cell. -/
+def greeting : IO String :=
+  pure (mockHello ())
+
+end MockExtra
diff --git a/tests/fixtures/mock-extra/README.md b/tests/fixtures/mock-extra/README.md
new file mode 100644
index 0000000..dd3bd00
--- /dev/null
+++ b/tests/fixtures/mock-extra/README.md
@@ -0,0 +1,94 @@
+# `tests/fixtures/mock-extra/` — reference plug-in fixture
+
+This directory is xeus-lean's **conformance test** for the
+`EXTRA_WASM_DIRS` plug-in contract.  It contains the smallest
+imaginable third-party Lean lib (one `@[extern]` declaration backed
+by one C function) plus a build script that produces exactly the
+layout xlean's CMake expects.
+
+It is not shipped with the kernel.  It exists so that:
+
+1. CI can prove on every push that the contract still works end-to-end.
+2. Downstream library authors (Sparkle, Hesper, the next idea) have
+   a copy-pasteable starting point.
+
+If you are adding a Lean library to xeus-lean's WASM build, mirror
+the four files here and adjust the names.
+
+## Layout
+
+```
+tests/fixtures/mock-extra/
+├── MockExtra.lean            -- @[extern "mock_extra_hello"] opaque mockHello
+├── c_src/
+│   └── mock_extra_hello.c    -- LEAN_EXPORT lean_object* mock_extra_hello(...)
+├── lakefile.lean             -- one-line `lean_lib MockExtra`
+├── lean-toolchain            -- pinned to match xeus-lean's
+├── build-wasm.sh             -- → <staging>/{MockExtra/,lib/,xeus-lean-extra.json}
+└── README.md                 -- you're here
+```
+
+## What `build-wasm.sh` produces
+
+Pass any empty (or pre-existing) directory; the script populates it
+with the staging layout xlean's CMake reads:
+
+```
+<staging>/
+├── MockExtra.olean
+├── MockExtra/                ← per-module olean subtree
+├── lib/
+│   ├── libmock_extra_wasm.a
+│   └── mock_extra_exports.txt
+├── .xeus-auto-imports        ← optional, registers MockExtra in cell 1
+└── xeus-lean-extra.json      ← manifest the CMake EXTRA_WASM_DIRS loop reads
+```
+
+## How CI uses it
+
+`.github/workflows/ci.yml` runs:
+
+```yaml
+- name: Build mock-extra fixture
+  run: |
+    pixi run -e wasm-build bash tests/fixtures/mock-extra/build-wasm.sh \
+      "${RUNNER_TEMP}/mock-extra-staging"
+    echo "EXTRA_WASM_DIRS=${RUNNER_TEMP}/mock-extra-staging" >> "$GITHUB_ENV"
+```
+
+then the configure step picks `EXTRA_WASM_DIRS` up:
+
+```yaml
+- name: Configure WASM build (emcmake)
+  run: |
+    pixi run -e wasm-build emcmake cmake -S . -B wasm-build \
+      ... -DEXTRA_WASM_DIRS="${EXTRA_WASM_DIRS}"
+```
+
+and `test_wasm_node` evaluates a Lean cell that calls
+`MockExtra.mockHello ()` and asserts the result is
+`"hello from mock-extra"`.  If that assertion fails, the
+EXTRA_WASM_DIRS contract is broken.
+
+## What the contract guarantees
+
+A downstream lib that follows the same layout gets:
+
+| Thing                                | Guaranteed at link time | Guaranteed at runtime |
+| ---                                  | ---                     | ---                   |
+| Lean externs are reachable           | ✓ (whole-archive)       | ✓ (dlsym shim)        |
+| `import MyLib` finds the olean       | ✓ (olean staged)        | ✓ (VFS / search root) |
+| Module auto-imports on first cell    | ✓ (`.xeus-auto-imports`) | ✓                    |
+
+Anything beyond that — Mathlib-bundle-style on-demand loading, JS-side
+display widgets, additional `%load` namespaces — is the consumer's
+responsibility.
+
+## See also
+
+* `README.md` of this repo, section *"Extending the kernel with your
+  own Lean lib"* — the contract written out as prose.
+* `CMakeLists.txt` block titled `EXTRA_WASM_DIRS` — the reader of
+  `xeus-lean-extra.json`.
+* `src/REPL/Frontend.lean`'s auto-import scan — the reader of
+  `.xeus-auto-imports`.
diff --git a/tests/fixtures/mock-extra/build-wasm.sh b/tests/fixtures/mock-extra/build-wasm.sh
new file mode 100755
index 0000000..7c05811
--- /dev/null
+++ b/tests/fixtures/mock-extra/build-wasm.sh
@@ -0,0 +1,186 @@
+#!/usr/bin/env bash
+#
+# build-wasm.sh — reference build script for a third-party Lean
+# library plugging into xlean via -DEXTRA_WASM_DIRS=<staging>.
+#
+# This is intentionally tiny: it does exactly what the contract says
+# it must do and nothing more.  Downstream builds (Sparkle, Hesper,
+# future libs) can copy this layout and substitute their own
+# sources.
+#
+# Usage:
+#   build-wasm.sh <staging-dir>
+#
+# Produces inside <staging-dir>:
+#   <staging>/MockExtra/...            ← olean tree from `lake build`
+#   <staging>/MockExtra.olean          ← top-level umbrella olean
+#   <staging>/lib/libmock_extra_wasm.a ← C extern compiled by emcc
+#   <staging>/lib/mock_extra_exports.txt
+#   <staging>/xeus-lean-extra.json     ← manifest xlean's CMake reads
+#
+# Run from inside an emscripten-enabled shell (`pixi run -e wasm-build …`
+# in this repo) so `emcc`, `emar`, and `lake` are on PATH.
+
+set -euo pipefail
+
+if [ $# -ne 1 ]; then
+    echo "usage: $0 <staging-dir>" >&2
+    exit 2
+fi
+
+STAGING="$(realpath "$1")"
+SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
+
+mkdir -p "$STAGING/lib"
+
+echo "[mock-extra] staging dir : $STAGING"
+echo "[mock-extra] source dir  : $SCRIPT_DIR"
+
+# ---------------------------------------------------------------------
+# 1. Build the olean tree (host Lean — same .olean works in WASM and
+#    native because olean is architecture-independent for libs without
+#    precompileModules).
+# ---------------------------------------------------------------------
+pushd "$SCRIPT_DIR" >/dev/null
+lake build MockExtra
+OLEAN_SRC="$SCRIPT_DIR/.lake/build/lib/lean"
+if [ ! -f "$OLEAN_SRC/MockExtra.olean" ]; then
+    echo "[mock-extra] ERROR: lake didn't produce $OLEAN_SRC/MockExtra.olean" >&2
+    exit 1
+fi
+popd >/dev/null
+
+# Copy olean(s) into the staging dir.  The umbrella file
+# (<root>.olean) lives at <staging>/<root>.olean and the per-module
+# tree lives at <staging>/<root>/...  This is the layout xlean's
+# CMake expects when `olean_root` in the manifest is "MockExtra".
+cp "$OLEAN_SRC/MockExtra.olean" "$STAGING/MockExtra.olean"
+if [ -d "$OLEAN_SRC/MockExtra" ]; then
+    cp -r "$OLEAN_SRC/MockExtra" "$STAGING/MockExtra"
+else
+    mkdir -p "$STAGING/MockExtra"
+fi
+# olean.private / olean.server / ir / ilean siblings, if any.
+for ext in olean.private olean.server ir ilean; do
+    if [ -f "$OLEAN_SRC/MockExtra.$ext" ]; then
+        cp "$OLEAN_SRC/MockExtra.$ext" "$STAGING/"
+    fi
+done
+
+# ---------------------------------------------------------------------
+# 2. Build the C extern + the Lean-generated wrappers as a WASM
+#    static library.
+#
+# Lake generates a `.c` file under `.lake/build/ir/MockExtra.c` that
+# wraps every `@[extern]` declaration in a boxed entry point
+# (`lp_<package>_<module>_<name>` / `___boxed`).  The Lean interpreter
+# calls those wrappers via dlsym, so they MUST be in the archive
+# alongside our hand-written C implementation.  Skipping them is the
+# silent failure that shows up at runtime as
+#   "Could not find native implementation of external declaration
+#    'MockExtra.mockHello' (symbols 'lp_mockExtra_MockExtra_mockHello___boxed'
+#    or 'lp_mockExtra_MockExtra_mockHello')"
+# ---------------------------------------------------------------------
+LEAN_PREFIX="$(lean --print-prefix)"
+LEAN_INCLUDE="$LEAN_PREFIX/include"
+if [ ! -d "$LEAN_INCLUDE" ]; then
+    echo "[mock-extra] ERROR: lean toolchain include dir not found: $LEAN_INCLUDE" >&2
+    exit 1
+fi
+
+GENERATED_C="$SCRIPT_DIR/.lake/build/ir/MockExtra.c"
+if [ ! -f "$GENERATED_C" ]; then
+    echo "[mock-extra] ERROR: lake didn't produce $GENERATED_C" >&2
+    exit 1
+fi
+
+OBJ_HAND="$STAGING/lib/mock_extra_hello.o"
+emcc -O2 -sMEMORY64 -fPIC \
+     -I"$LEAN_INCLUDE" \
+     -c "$SCRIPT_DIR/c_src/mock_extra_hello.c" \
+     -o "$OBJ_HAND"
+
+# Lean's `lean.h` inlines `mi_malloc_small` into the allocator
+# hot path whenever `LEAN_MIMALLOC` is defined, and
+# `lean/config.h` unconditionally defines it for the v4.x
+# toolchain.  When the Lean-generated wrappers inherit that inline
+# expansion, they end up calling `mi_*` from one heap (libc-backed
+# fallback) while libleanrt allocates from a different heap
+# (real mimalloc) — every `lean_dec_ref` on a wrapper-allocated
+# object then trips `RuntimeError: memory access out of bounds`
+# inside `emscripten_builtin_free`.
+#
+# Cleanest fix: compile the wrappers as if `LEAN_MIMALLOC` were
+# never set.  `lean/config.h` is `#pragma once` so it's only
+# evaluated the first time; `-include` of config.h forces that
+# first evaluation now, and the override header `#undef`s the
+# macro before `<lean/lean.h>` is read.  All subsequent
+# `#include <lean/lean.h>` calls in the TU find the guard already
+# satisfied and skip re-defining the macro, so the file falls
+# through to the plain `malloc`/`free` code paths consistently.
+# Those depend only on libc, which is on every emcc link line.
+#
+# xlean's main TUs are unaffected because they're compiled
+# without these overrides.
+OVERRIDE_H="$STAGING/lib/mock_extra_no_mimalloc.h"
+cat > "$OVERRIDE_H" <<'EOF'
+#undef LEAN_MIMALLOC
+EOF
+OBJ_LEAN="$STAGING/lib/mock_extra_lean_wrappers.o"
+emcc -O2 -sMEMORY64 -fPIC -w \
+     -I"$LEAN_INCLUDE" \
+     -include lean/config.h \
+     -include "$OVERRIDE_H" \
+     -c "$GENERATED_C" \
+     -o "$OBJ_LEAN"
+rm -f "$OVERRIDE_H"
+
+emar rcs "$STAGING/lib/libmock_extra_wasm.a" "$OBJ_HAND" "$OBJ_LEAN"
+rm -f "$OBJ_HAND" "$OBJ_LEAN"
+
+# ---------------------------------------------------------------------
+# 3. Exports file — one symbol per line, with the leading underscore
+#    emscripten expects on `-sEXPORTED_FUNCTIONS`.
+#
+# Includes:
+#   - mock_extra_hello: the hand-written C extern.
+#   - every LEAN_EXPORT in the generated .c: the boxed wrappers the
+#     Lean interpreter resolves via dlsym at runtime.
+# ---------------------------------------------------------------------
+EXPORTS="$STAGING/lib/mock_extra_exports.txt"
+{
+    echo "_mock_extra_hello"
+    # Pick up `LEAN_EXPORT <type> <name>(` lines from the generated C.
+    # Match both bare names and the `___boxed` form Lean uses.
+    grep -oE 'LEAN_EXPORT[[:space:]]+[a-zA-Z_][a-zA-Z_0-9*]*[[:space:]]+[a-zA-Z_][a-zA-Z_0-9]*[[:space:]]*\(' \
+         "$GENERATED_C" \
+      | sed -E 's/^LEAN_EXPORT[[:space:]]+[a-zA-Z_][a-zA-Z_0-9*]*[[:space:]]+([a-zA-Z_][a-zA-Z_0-9]*).*/_\1/'
+} | sort -u > "$EXPORTS"
+
+EXPORT_COUNT=$(wc -l < "$EXPORTS")
+echo "[mock-extra] $EXPORT_COUNT symbol(s) → $EXPORTS"
+
+# ---------------------------------------------------------------------
+# 4. xeus-lean-extra.json — the contract xlean's CMake reads.
+# ---------------------------------------------------------------------
+cat > "$STAGING/xeus-lean-extra.json" <<'EOF'
+{
+  "archive":    "lib/libmock_extra_wasm.a",
+  "exports":    "lib/mock_extra_exports.txt",
+  "olean_root": "MockExtra"
+}
+EOF
+
+# ---------------------------------------------------------------------
+# 5. Optional: drop a .xeus-auto-imports registry so xlean's REPL
+#    pre-imports MockExtra on the first cell.  Lives at the olean
+#    root because xlean's auto-import scan walks each search root.
+# ---------------------------------------------------------------------
+cat > "$STAGING/.xeus-auto-imports" <<'EOF'
+# Modules to inject into cell 1 of the xlean REPL.
+# One module name per line; lines starting with # are ignored.
+MockExtra
+EOF
+
+echo "[mock-extra] DONE.  Pass this to xlean's WASM build with:"
+echo "             -DEXTRA_WASM_DIRS=\"$STAGING\""
diff --git a/tests/fixtures/mock-extra/c_src/mock_extra_hello.c b/tests/fixtures/mock-extra/c_src/mock_extra_hello.c
new file mode 100644
index 0000000..9eb275f
--- /dev/null
+++ b/tests/fixtures/mock-extra/c_src/mock_extra_hello.c
@@ -0,0 +1,24 @@
+/*
+ * mock_extra_hello.c — implementation of MockExtra.mockHello.
+ *
+ * Returns a fresh `lean_string_object` whose payload is the literal
+ * "hello from mock-extra".  The Lean call convention for an
+ * `@[extern "mock_extra_hello"] opaque mockHello : Unit -> String`
+ * declaration is:
+ *
+ *   lean_object* mock_extra_hello(lean_object* unit);
+ *
+ * The argument is owned by the caller and must be `lean_dec`'d once
+ * we're done with it.  The return value is owned by the caller.
+ */
+#include <lean/lean.h>
+
+static const char kGreeting[] = "hello from mock-extra";
+
+LEAN_EXPORT lean_object* mock_extra_hello(lean_object* unit_obj) {
+    /* Release the unit argument: the Lean -> C extern ABI hands us
+       ownership of every argument even when the value is uninteresting.
+       Forgetting this leaks one reference per call. */
+    lean_dec(unit_obj);
+    return lean_mk_string(kGreeting);
+}
diff --git a/tests/fixtures/mock-extra/lake-manifest.json b/tests/fixtures/mock-extra/lake-manifest.json
new file mode 100644
index 0000000..38edf68
--- /dev/null
+++ b/tests/fixtures/mock-extra/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "mockExtra",
+ "lakeDir": ".lake"}
diff --git a/tests/fixtures/mock-extra/lakefile.lean b/tests/fixtures/mock-extra/lakefile.lean
new file mode 100644
index 0000000..05d1654
--- /dev/null
+++ b/tests/fixtures/mock-extra/lakefile.lean
@@ -0,0 +1,18 @@
+import Lake
+open Lake DSL
+
+-- Minimal lake project that produces a single `MockExtra.olean`.
+-- The matching native library (libmock_extra_wasm.a or the .so on
+-- native) is built outside lake by `build-wasm.sh` / `build-native.sh`
+-- using emcc / clang directly.  Lake's own native-library support
+-- is fine but pulls in more infrastructure than this fixture needs.
+
+package mockExtra where
+  -- We don't ship `precompileModules` because there are no Lean-side
+  -- C bindings to compile; the lone extern is implemented in C.
+
+lean_lib MockExtra where
+  -- The single-file lib whose top-level module name is "MockExtra".
+  -- Whatever name appears here must match `olean_root` in the
+  -- xeus-lean-extra.json the build script writes.
+  roots := #[`MockExtra]
diff --git a/examples/sparkle/lean-toolchain b/tests/fixtures/mock-extra/lean-toolchain
similarity index 100%
rename from examples/sparkle/lean-toolchain
rename to tests/fixtures/mock-extra/lean-toolchain