Feature/extra wasm dirs#13
Merged
Merged
Conversation
Closes #11. In the WASM kernel `IO.println` lands in DevTools console rather than the notebook cell, because Lean 4.28's `withIsolatedStreams` doesn't fire under emscripten and our previous workaround was to ask every elab to route through `logInfo`. Downstream code we don't control (Sparkle's `#showVerilog`, ad-hoc `#eval IO.println "hi"` cells, Lean's parse-error lines) was still silent. Implement the WASM analogue of the native xeus_ffi.cpp dup2 pipe at the emscripten layer: - src/pre.js: override Module.print / printErr to append into Module._xleanStdoutBuf / _xleanStderrBuf rather than fall through to console.log. - src/xinterpreter_wasm.cpp: - EM_JS helpers xlean_drain_stdout_to / stderr_to that copy the JS buffer into a caller-provided char[], clear the JS buffer, and split on newline if more bytes are pending than fit. The cpp side drains in a loop until 0 is returned, capped at 64 iterations as a runaway guard. - In execute_request_impl, after the messages loop assembles pub_data, drain stdout and pass it through the same extract_mime_payloads path the native kernel uses. Anything MIME-tagged enters mime_bundle; anything plain is prepended to text/plain so the order matches a native lean --run tail. - stderr drains through publish_stream("stderr", ...), keeping warning-style output visually distinct. This unblocks tutorial chapters that use `#eval IO.println …` and frees downstream libraries to drop their `logInfo`-only contortions. `logInfo` keeps working unchanged.
Plumb a vendor-agnostic mechanism for pulling third-party static
libraries (Hesper, future ones) into the WASM xlean build without
xeus-lean knowing their name. Each entry in EXTRA_WASM_DIRS points
at a staging directory shipped by the third-party project and must
contain `xeus-lean-extra.json` describing what to wire in:
{
"archive": "lib/libNAME_wasm.a", // relative path
"exports": "lib/NAME_exports.txt", // one symbol per line
"olean_root": "TopLevelModule" // optional; for pure C libs
} // omit it
CMake:
- Reads each manifest, whole-archives the static lib into xlean
(Lean externs would otherwise be DCE'd), splats the exports list
into emcc's -sEXPORTED_FUNCTIONS, and copies <dir>/<olean_root>/**
into OLEAN_ASSETS_DIR alongside Init / Std / Lean / Sparkle.
- xeus-lean code never hard-codes a third-party module name; the
manifest is the only place that knows it.
Back-compat: -DHESPER_WASM_DIR=<dir> is honoured. We synthesise an
xeus-lean-extra.json on the fly so existing Hesper build scripts
keep working without their own update, and warn that the flag is
deprecated.
This is the prep step for switching CI from HESPER_WASM_DIR to
EXTRA_WASM_DIRS in the next commit; it lands first so the bridge
is in place before the consumer changes flow through it.
Companion to the previous CMake commit. The wasm CI step no
longer talks about Hesper by name in code — it just builds each
third-party staging dir into ${RUNNER_TEMP} and concatenates them
into EXTRA_WASM_DIRS. Hesper is still the only entry today, but
adding another library (Sparkle-as-side-deps, future Lean libs)
is a one-line append now.
Removed:
- hesper as a git submodule (.gitmodules + 160000 gitlink)
- hesper-wasm/ (build-wasm.sh, lakefile-wasm.lean, patches/) —
hesper now ships its own native/wasm/build-wasm.sh at
Verilean/hesper#feature/wasm-m2 onwards.
Changed:
- ci.yml's "Build Hesper wasm staging" step is now "Build third-
party wasm staging dirs" and writes its results into
EXTRA_WASM_DIRS rather than HESPER_WASM_DIR. The configure
step passes -DEXTRA_WASM_DIRS=… to emcmake.
- ci.yml's pack-olean step's comment no longer references the
HESPER_WASM_DIR block.
- docs.yml: drop the hesper/* + hesper-wasm/* path filters.
Back-compat: -DHESPER_WASM_DIR=<dir> still works (see CMakeLists.txt
synth shim in the previous commit), so an older hesper-side build
recipe doesn't break.
CI run 80662418575 failed with failed to compute cache key: ... "/hesper-wasm": not found because Dockerfile.docs-builder still tried to COPY hesper/ and hesper-wasm/ — those directories were removed two commits earlier (EXTRA_WASM_DIRS migration). docs-deploy's job is to serve math-visual + Lean tutorials, none of which import Hesper. Drop the COPY + build steps and the post-pack symlink hook entirely. When a future tutorial needs Hesper, mirror ci.yml's pattern: checkout Verilean/hesper, run its native/wasm/build-wasm.sh into staging, pass -DEXTRA_WASM_DIRS=<staging> to emcmake.
We're about to do a large clean-up that removes Sparkle / Hesper- specific code from the kernel repo and replaces it with a generic EXTRA_WASM_DIRS path plus a `tests/fixtures/mock-extra/` reference implementation. Without context that looks like deletion-for-its- own-sake; this README rewrite explains the goal so PR reviewers and future maintainers don't lose the thread: - What xeus-lean owns: the kernel, the JupyterLite glue, and a vendor-agnostic extension point. Nothing more. - What it doesn't own: any specific third-party Lean library. No third-party name should appear in this repo's build files. - How a downstream lib plugs in: ship a `xeus-lean-extra.json` manifest pointing at an archive + exports list + olean root, then pass the staging dir via EXTRA_WASM_DIRS. - Why `tests/fixtures/mock-extra/` exists: it exercises the entire third-party path end-to-end in CI, so the contract has teeth. - Why we're splitting the work into PR #13 + a follow-up: stage 1 proves the path correct via a full rebuild on every CI run; stage 2 introduces a `xeus-lean-wasm-prebuild` image and relink-only path so downstream CI doesn't pay ~30 min per build. - Native target: same contract is in scope, separate PR.
…k, smoke-test xeus-lean's job is the Lean kernel + REPL + JupyterLite glue + a vendor-agnostic extension point. Sparkle is a downstream consumer of that extension point and should not appear in this repo's build graph. CMakeLists.txt: drop the 160-line block that pre-processed SPARKLE_C_BARRIER, scanned the Sparkle IR tree, stubbed initialize_sparkle_*, built libsparkle_wasm.a, and stamped its symbol list into emcc's -sEXPORTED_FUNCTIONS. Same for the Sparkle olean copy into OLEAN_ASSETS_DIR and the Sparkle archive in test_wasm_node's link line. What replaces it: the existing EXTRA_WASM_DIRS path. A new tiny "core exports" block keeps _xlean_poll_load_progress on the EXPORTED_FUNCTIONS list (that symbol is owned by xeus-lean, not by any third party), and the symbol-table generator and test_wasm_node link now iterate over `_extra_archive_paths` collected by the EXTRA_WASM_DIRS loop — so each third-party archive contributes its symbols the same way Sparkle used to. Also removed: - examples/sparkle/ (Sparkle demo lake project — lives in Sparkle repo's own samples now) - notebooks/sparkle-native-demo.ipynb (Sparkle-only demo) - scripts/smoke-test-sparkle.py (Sparkle smoke check) - The HESPER_WASM_DIR legacy shim from the previous commit on this branch — same reasoning, no third-party names allowed. Downstream consumers (Sparkle, Hesper, …) ship their own xeus-lean-extra.json manifest and pass their staging dir via -DEXTRA_WASM_DIRS=<dir>. See README.md "Extending the kernel with your own Lean lib" for the contract and tests/fixtures/ mock-extra/ for a worked example (added in a later commit on this branch).
…aceholder
Companion to the previous commit's CMake cleanup. Strip Sparkle/
Hesper-specific build steps from the Dockerfiles and CI workflows,
leaving only the generic EXTRA_WASM_DIRS path.
Removed:
- Dockerfile.native-sparkle (whole file)
- ci.yml's "Build Sparkle example" (native + wasm), "Run Sparkle
example", "Checkout Hesper" + "Build third-party wasm staging
dirs" (Hesper-specific body), and the entire
native-sparkle-docker job
- Dockerfile.wasm's "Build Sparkle example" + "Build Hesper WGSL
DSL" steps and the hesper-wasm/build symlink in the pack-olean
step + COPY hesper{,-wasm}/
- Dockerfile.docs-builder's COPY examples/ + Sparkle/Hesper build
blocks
- docs.yml's examples/sparkle/** path filter
Replaced ci.yml's wasm Sparkle/Hesper build with a new step that
builds the mock-extra fixture (tests/fixtures/mock-extra/, added
in the next commit on this branch) into ${RUNNER_TEMP} and exports
EXTRA_WASM_DIRS for the configure step. That's the new contract
under test on every push: "does the generic third-party plug-in
path still work end-to-end?"
Dockerfile.{native,wasm,docs-builder} keep prose comments
explaining that downstream consumers build their own libs and
pass -DEXTRA_WASM_DIRS=… — that's documentation, not a
dependency.
src/REPL/Frontend.lean: the auto-import block used to hard-probe for Sparkle.olean and Hesper/WGSL/DSL.olean and emit the matching `import` lines. Replace it with a data-driven registry: every third-party lib that ships a `.xeus-auto-imports` file (one module per line) on the search path gets its module names appended to the first-cell preamble, provided the corresponding olean is actually present. Display is the only module xeus-lean itself auto-imports. src/Display.lean: replace example help entries that named SparkleHelp / HesperHelp / Sparkle.Backend.Verilog.toVerilog with generic placeholders (MyLibHelp, "module dff (...); ..." literal). src/Convert.lean: prose comment was "renders the Sparkle tutorial chapters" — rephrase as "renders the tutorial chapters". notebooks/sparkle-demo.ipynb: deleted (Sparkle-specific demo). notebooks/mathlib-demo.ipynb: drop the trailing "/Sparkle" from the boot-budget sentence; sized comment also updated. Net effect: the strings "Sparkle" and "Hesper" no longer appear anywhere in xeus-lean's build inputs, kernel sources, or shipped notebooks. Tutorial / extension-point documentation still calls them by name as examples of downstream consumers; that's data, not a build-graph dependency.
This is xeus-lean's conformance test for the EXTRA_WASM_DIRS plug-in
contract. A real-but-tiny third-party-style Lean lib with one
@[extern] backed by one C function, plus a build-wasm.sh that
emits exactly the staging layout xlean's CMake reads:
<staging>/MockExtra.olean
<staging>/MockExtra/...
<staging>/lib/libmock_extra_wasm.a
<staging>/lib/mock_extra_exports.txt
<staging>/.xeus-auto-imports
<staging>/xeus-lean-extra.json
CI uses this every push to prove the contract still works
end-to-end (CMake reads the manifest → wasm-ld links the
archive → test_wasm_node evaluates `MockExtra.mockHello ()` and
asserts the result). If the assertion fails, the contract is
broken and downstream consumers can't rely on it.
The README spells out the layout and how a real lib (Sparkle,
Hesper, …) reuses it. The fixture is also the simplest place
to land when you're building a new Lean lib that wants to run in
JupyterLite-via-xlean.
Files added:
- MockExtra.lean one @[extern] + a convenience wrapper
- c_src/mock_extra_hello.c LEAN_EXPORT lean_object* mock_extra_hello
- lakefile.lean + lean-toolchain for `lake build MockExtra`
- lake-manifest.json (empty deps; checked in to keep the
fixture reproducible across runs)
- build-wasm.sh emcc + emar + cp + heredoc the JSON
- .gitignore hides .lake/, build-wasm/
- README.md spec
The Sparkle/Hesper-specific REPL-eval steps at the bottom of test_wasm_node.cpp went away with the previous commits. Replace them with a single hard assertion against the mock-extra fixture: #eval IO.println (MockExtra.mockHello ()) -> "hello from mock-extra" When CI configured the wasm build with -DEXTRA_WASM_DIRS=<staging-from-build-wasm.sh>, every link in the chain must be working for this to print the expected string: 1. CMake read xeus-lean-extra.json and whole-archived libmock_extra_wasm.a. 2. The Lean stage VFS got <staging>/MockExtra.olean copied in. 3. .xeus-auto-imports registered MockExtra so the REPL auto-imports it on the first cell. 4. The dlsym shim resolved the `mock_extra_hello` C symbol. 5. The C function returned a Lean string back across the boundary. A new `run_cmd_expect` helper does substring matching on the JSON result envelope and returns `1` from main if the needle is absent, so a contract regression turns the WASM CI job red.
… VFS staging CI run 80714620802 surfaced two contract gaps when the mock-extra fixture was wired in: 1. xlean's deploy olean-stager skipped any EXTRA_WASM_DIRS entry whose `<root>/` subtree was empty. mock-extra ships only `MockExtra.olean` (umbrella, no per-module files) and was silently dropped. Accept umbrella-only libs: warn only when both the umbrella file and the subtree are missing. 2. The `.xeus-auto-imports` registry the third-party staging dir shipped never reached the VFS — neither the deploy stage nor the test_wasm_node stage knew about it. Merge each entry into a single `<vfs>/.xeus-auto-imports` so Frontend.lean's scanner picks them up. Multiple EXTRA_WASM_DIRS entries each append (with a comment marker so the source is traceable). 3. test_wasm_node only embedded Init.olean; mock-extra and its auto-import file weren't in the test binary's VFS, so the test cell saw `Unknown identifier MockExtra.mockHello`. Stage every EXTRA_WASM_DIRS olean root + its `.xeus-auto-imports` into the test_olean_staging tree the same way the deploy target does. With all three pieces in place, the contract test `#eval IO.println (MockExtra.mockHello ())` now has a chance of seeing `"hello from mock-extra"` come back across the boundary.
Dockerfile.docs-builder's smoke step runs test_wasm_node.js but
configures the WASM build *without* -DEXTRA_WASM_DIRS — that build
target is the kernel-only image, not the conformance test rig.
With the previous test_wasm_node revision the smoke step always
ran the mock-extra assertion and always failed there with
"Unknown identifier `MockExtra.mockHello`".
Probe /lib/lean/MockExtra.olean before running the assertion.
When the fixture isn't staged, log SKIP and continue. The
contract is still tested in the wasm-build CI job, which builds
the fixture into ${RUNNER_TEMP} and passes it via
EXTRA_WASM_DIRS — that path is unchanged and is the canonical
one.
junjihashimoto
had a problem deploying
to
github-pages
GitHub Actions
Failure
…_* symbols CI run 80738083812 surfaced the missing piece in the fixture build: [TEST] EXCEPTION: Could not find native implementation of external declaration 'MockExtra.mockHello' (symbols 'lp_mockExtra_MockExtra_mockHello___boxed' or 'lp_mockExtra_MockExtra_mockHello'). The Lean interpreter resolves @[extern] declarations not by the C name you wrote in the `extern` attribute (mock_extra_hello) but by a mangled `lp_<package>_<module>_<name>` wrapper that `lake build` generates into `.lake/build/ir/MockExtra.c`. Linking only the hand-written C file leaves those wrappers undefined at runtime. Fix: - Compile both .c files (hand-written + Lean-generated) and pack both into libmock_extra_wasm.a. - Regenerate mock_extra_exports.txt by grepping every `LEAN_EXPORT` in the generated source and emitting the matching `_lp_*` / `_lp_*___boxed` lines alongside `_mock_extra_hello`. Without those entries on -sEXPORTED_FUNCTIONS, wasm-ld's LTO drops the wrappers wholesale. After this commit the fixture builds the same three things every real downstream project would: a C archive that contains both sides of the boundary, an exports list that names every dynamically resolved symbol, and the manifest.
junjihashimoto
had a problem deploying
to
github-pages
GitHub Actions
Failure
… link fix
CI run 27386250190 surfaced the third missing piece:
wasm-ld: error: .../libmock_extra_wasm.a(mock_extra_lean_wrappers.o):
undefined symbol: mi_malloc_small
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. The Lean-
generated wrappers therefore reference mi_malloc_small directly.
That symbol lives only in xlean's libleanrt_wasm.a, but wasm-ld
scans the third-party archive before leanrt and the reference goes
unresolved.
Ship a small shim translation unit with weak definitions of the
three mi_* symbols Lean's headers can inline (mi_malloc_small,
mi_free, mi_free_size). The wrappers route through
lean_alloc_object / libc free. Because they're weak, the real
mimalloc implementations inside libleanrt_wasm.a win when both
archives are linked — the shim is a fallback that resolves the
link, not a replacement.
Now an end-to-end downstream lib gets:
- the Lean-generated wrappers archived alongside the hand-written
C extern (previous commit on this branch),
- an exports list covering both halves,
- and weak fallbacks for the three mi_* symbols Lean inlines, so
archive order doesn't matter at link time.
junjihashimoto
had a problem deploying
to
github-pages
GitHub Actions
Failure
The previous weak `mi_malloc_small` / `mi_free` shim caused a heap mismatch at runtime: the weak `mi_free` (libc `free`) was selected for memory allocated by libleanrt's real mimalloc, tripping `RuntimeError: memory access out of bounds` inside `emscripten_builtin_free` during init-attr execution after `Lean.importModules`. Use `-include lean/config.h -include override.h` where `override.h` `#undef`s `LEAN_MIMALLOC`. `lean/config.h` has `#pragma once`, so the subsequent `<lean/lean.h>` in `MockExtra.c` finds the guard satisfied and skips re-defining the macro — the inline allocator falls through to `malloc`/`free`, which are always on the link line via libc. No `mi_*` symbols are referenced from the wrapper TU at all, so archive order doesn't matter and there's no heap to mismatch. xlean main TUs are unaffected (compiled without the overrides).
junjihashimoto
had a problem deploying
to
github-pages
GitHub Actions
Failure
* `tests/e2e/rich-display.spec.ts`
- Remove the `sparkle hdl` describe block. Its single test opened
`sparkle-demo.ipynb`, which no longer ships with xeus-lean as of
this PR — the file was always going to fail in CI. xeus-lean's
EXTRA_WASM_DIRS contract is exercised by
`tests/fixtures/mock-extra/` + the `test_wasm_node` step;
downstream HDL-style libs own their own Playwright suites.
- Skip `#latex renders via MathJax` in CI: the Lean side passes
(`assertNoError` is fine) but the JupyterLab MathJax MIME
renderer needs >20 s on the GH Actions runner before any of
`mjx-container` / `.MathJax` / `.jp-RenderedLatex` appears.
Same `test.skip(!!process.env.CI, ...)` pattern already used
for `Waveform SVG display`.
* `tests/e2e/jupyter.ts`
- Drop the stale "Std/Lean/Sparkle/Hesper olean trees" comment.
junjihashimoto
had a problem deploying
to
github-pages
GitHub Actions
Failure
E2E repro: `#svg embeds an SVG` failed in `make e2e-docker`
(NixOS-local) and on GH Actions both, even after the prior
sparkle-drop + #latex skip. Trace + DOM snapshot showed the cell
had emitted a stream-stderr chunk AND a follow-up rich-display
widget, but `runCell` was returning only the *first*
`.jp-OutputArea-output` element and Playwright's `.locator('svg,
img')` therefore searched inside the text-stream output where
no SVG / IMG node ever exists.
Three independent issues converged:
1. `src/pre.js` was capturing ALL of `Module.printErr` into
`_xleanStderrBuf` and replaying it through `publish_stream`,
so the `[WasmRepl] …` / `[WASM] …` instrumentation lines that
the C++ side meant for DevTools were flooding every cell's
output area. Drop them on the floor by default; only
capture lines that actually carry a MIME envelope (Display.*
/ Sparkle's `#showVerilog` etc.). Plain debug lines now go
to `console.error`, visible to a developer in DevTools but
not to the notebook.
2. `src/WasmRepl.lean` was logging the full `displayOutput`
(i.e. the MIME envelope) via `IO.eprintln`. Under the new
rule above that line still ends up in the cell because it
contains the `\x1bMIME:` marker. Cut it back to a
length-only diagnostic — the envelope itself is already on
the `messages` wire.
3. `tests/e2e/jupyter.ts` was returning
`cell.locator('.jp-OutputArea-output').first()` to the test
suite. When a cell emits a stream-stderr output before the
rich-display widget, `.first()` resolves to the stream node
and any `.locator('svg, img')` search inside it is doomed.
Return the container `.jp-OutputArea` instead so all child
outputs are reachable.
4. `tests/e2e/rich-display.spec.ts` was matching `mjx-container,
.MathJax, .jp-RenderedLatex` with a strict-mode locator.
The MathJax MIME widget legitimately contains BOTH a
`mjx-container` (the typeset glyphs) and a `.jp-RenderedLatex`
(the wrapper), so the assertion crashed with a strict-mode
violation rather than passing. Drop `.first()` on the
`svg, img` and `mjx-container, …` locators — the assertion
reads as "at least one of these renders", which is what
we actually want. Also re-enable the `#latex` test since the
underlying renderer works in the same Docker environment we
ship — what we were observing was the strict-mode crash,
not a render-latency wart.
Verified end-to-end with `make e2e-docker` (CI=1):
7 passed (rich-display + smoke), 1 skipped (Waveform), 0 failed.
junjihashimoto
had a problem deploying
to
github-pages
GitHub Actions
Failure
mark-christiaens
pushed a commit
to mark-christiaens/sparkle
that referenced
this pull request
Jun 24, 2026
xeus-lean PR Verilean#13 removed all third-party Lean libraries from its build and introduced a vendor-agnostic `EXTRA_WASM_DIRS` extension contract (see Verilean/xeus-lean#13 + the README). Sparkle was one of the libraries unbundled. Add the publish-side of that contract. ## What's new - `c_src/sparkle_jit_wasm_stub.c` — WASM-side stub for every `@[extern "sparkle_jit_*"]` declaration in `Sparkle.Core.JIT`. The native JIT uses `dlopen` + `dlsym` to load compiled CppSim shared libraries; neither exists in the xeus-lean WASM sandbox. Every stub raises `IO.userError` with a clear, actionable message pointing notebook users at `#synthesizeVerilog` / `#showVerilog` (which DO work under WASM) or at a native `lake exe` build for the JIT path. Tutorial cells that only synthesise Verilog or evaluate `Signal.atTime` are unaffected. - `tools/wasm/build-wasm.sh` — staging-builder modeled on xeus-lean's `tests/fixtures/mock-extra/build-wasm.sh` (the reference for the EXTRA_WASM_DIRS contract). It: 1. `lake build Sparkle` and copies the olean tree. 2. Compiles `sparkle_barrier.c` (WASM-safe pure C) and the new `sparkle_jit_wasm_stub.c` with `emcc -sMEMORY64`. 3. Compiles every Lake-generated `.c` wrapper under `.lake/build/ir/Sparkle/**.c` with the `LEAN_MIMALLOC` override the mock-extra fixture documents. 4. Archives them into `libsparkle_wasm.a`. 5. Extracts every `LEAN_EXPORT` symbol into `sparkle_exports.txt` so emcc's `-sEXPORTED_FUNCTIONS` survives LTO. 6. Writes the `xeus-lean-extra.json` manifest + a `.xeus-auto-imports` registry that pre-imports `Sparkle` on REPL cell 1. IP.* / Tools.SVParser / Tests / Examples are intentionally out of scope — they'd inflate the JupyterLite first-boot download by ~50 MB and the tutorials never import them. - `tools/wasm/README.md` — what the staging dir contains, how to drive it from xeus-lean's `pixi run -e wasm-build`, and what to do when Sparkle's extern surface changes. - Top-level `README.md` — point users at the browser path and at `tools/wasm/`. ## What this does NOT change - Sparkle's native build path is untouched. `sparkle_jit_wasm_stub.c` is only compiled into the WASM artefact; native builds keep linking `c_src/sparkle_jit.c` as before. - No Lean source changed. All routes through the existing `@[extern "sparkle_jit_*"]` declarations. ## Verification - [x] `lake build Sparkle` — succeeds (no Lean / Lake changes). - [x] `gcc -Wall -Wextra -c sparkle_jit_wasm_stub.c` — compiles clean against the same `lean/lean.h` the WASM build uses. - [ ] End-to-end WASM run (xeus-lean side) — to be exercised by running xeus-lean's docs CI with this Sparkle checkout passed via `EXTRA_WASM_DIRS`. Not part of this PR's diff (it's a cross-repo verification step).
junjihashimoto
added a commit
to Verilean/sparkle
that referenced
this pull request
Jul 1, 2026
xeus-lean PR #13 removed all third-party Lean libraries from its build and introduced a vendor-agnostic `EXTRA_WASM_DIRS` extension contract (see Verilean/xeus-lean#13 + the README). Sparkle was one of the libraries unbundled. Add the publish-side of that contract. ## What's new - `c_src/sparkle_jit_wasm_stub.c` — WASM-side stub for every `@[extern "sparkle_jit_*"]` declaration in `Sparkle.Core.JIT`. The native JIT uses `dlopen` + `dlsym` to load compiled CppSim shared libraries; neither exists in the xeus-lean WASM sandbox. Every stub raises `IO.userError` with a clear, actionable message pointing notebook users at `#synthesizeVerilog` / `#showVerilog` (which DO work under WASM) or at a native `lake exe` build for the JIT path. Tutorial cells that only synthesise Verilog or evaluate `Signal.atTime` are unaffected. - `tools/wasm/build-wasm.sh` — staging-builder modeled on xeus-lean's `tests/fixtures/mock-extra/build-wasm.sh` (the reference for the EXTRA_WASM_DIRS contract). It: 1. `lake build Sparkle` and copies the olean tree. 2. Compiles `sparkle_barrier.c` (WASM-safe pure C) and the new `sparkle_jit_wasm_stub.c` with `emcc -sMEMORY64`. 3. Compiles every Lake-generated `.c` wrapper under `.lake/build/ir/Sparkle/**.c` with the `LEAN_MIMALLOC` override the mock-extra fixture documents. 4. Archives them into `libsparkle_wasm.a`. 5. Extracts every `LEAN_EXPORT` symbol into `sparkle_exports.txt` so emcc's `-sEXPORTED_FUNCTIONS` survives LTO. 6. Writes the `xeus-lean-extra.json` manifest + a `.xeus-auto-imports` registry that pre-imports `Sparkle` on REPL cell 1. IP.* / Tools.SVParser / Tests / Examples are intentionally out of scope — they'd inflate the JupyterLite first-boot download by ~50 MB and the tutorials never import them. - `tools/wasm/README.md` — what the staging dir contains, how to drive it from xeus-lean's `pixi run -e wasm-build`, and what to do when Sparkle's extern surface changes. - Top-level `README.md` — point users at the browser path and at `tools/wasm/`. ## What this does NOT change - Sparkle's native build path is untouched. `sparkle_jit_wasm_stub.c` is only compiled into the WASM artefact; native builds keep linking `c_src/sparkle_jit.c` as before. - No Lean source changed. All routes through the existing `@[extern "sparkle_jit_*"]` declarations. ## Verification - [x] `lake build Sparkle` — succeeds (no Lean / Lake changes). - [x] `gcc -Wall -Wextra -c sparkle_jit_wasm_stub.c` — compiles clean against the same `lean/lean.h` the WASM build uses. - [ ] End-to-end WASM run (xeus-lean side) — to be exercised by running xeus-lean's docs CI with this Sparkle checkout passed via `EXTRA_WASM_DIRS`. Not part of this PR's diff (it's a cross-repo verification step).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.