Feature/wasm m2#8
Merged
Merged
Conversation
First step toward browser WebGPU via emdawnwebgpu, following the plan
in docs/research/wasm-webgpu-plan.md.
* native/CMakeLists.txt: Emscripten short-circuit branch that produces
libhesper_wasm.a from bridge_wasm_stub.cpp + cuda_bridge_stub.cpp and
returns before any Dawn / GLFW / CUDA-driver machinery.
* native/bridge.cpp: guard dawn_proc.h / DawnNative.h includes and the
dawnProcSetProcs call behind #ifndef __EMSCRIPTEN__ so the existing
native build is untouched.
* native/bridge_wasm_stub.cpp (new): every lean_hesper_* extern as a
stub returning IO.Error("Wasm bridge not wired yet"). Lets xeus-lean
link Hesper modules now; real wgpu* wiring lands in M2/M3.
* native/wasm/build-libhesper-wasm.sh (new): emcmake + emmake wrapper.
Locally produces an 18 KB libhesper_wasm.a containing all expected
lean_hesper_* symbols.
* native/.gitignore (new): build/, build-cmake/, build-wasm/, archives.
No native code paths change; this only adds a new EMSCRIPTEN branch.
…sm.a
Move the wasm build recipe from xeus-lean's hesper-wasm/ directory into
hesper itself so xeus-lean no longer has to know hesper internals.
xeus-lean follows up by calling this one script and linking the result.
* native/wasm/lakefile-wasm.lean (new): WGSL-only Lake override that
drops LSpec, doc-gen4, nativeDeps, Tests / Examples / lean_exe.
Lifted from xeus-lean/hesper-wasm/lakefile-wasm.lean verbatim, no
upstream-version patch needed now that hesper main is on Lean 4.28.
* native/wasm/build-wasm.sh (new): single script with two phases —
`lake build` against the override + emcc build of libhesper_wasm.a
via the EMSCRIPTEN branch in native/CMakeLists.txt. Stages outputs
to `<out-dir>/Hesper{,/**}.{olean,olean.server,olean.private,ir,ilean}`
and `<out-dir>/lib/libhesper_wasm.a`. Env knobs: LEAN_TOOLCHAIN_OVERRIDE,
SKIP_LIB, SKIP_OLEAN, BUILD_TYPE. Restore-on-trap ensures the repo's
lakefile.lean / lean-toolchain survive a failed `lake build`.
* native/wasm/build-libhesper-wasm.sh (removed): superseded by the
unified script.
* docs/research/wasm-webgpu-plan.md: M2 section rewritten to match
reality — hesper now owns the build recipe; the xeus-lean PR is just
a `-DHESPER_WASM_DIR=...` consumer.
Verified locally with emsdk 4.0.12 + Lean 4.28.0:
$ native/wasm/build-wasm.sh /tmp/out
...
[hesper-wasm] staged 222 olean files
[hesper-wasm] staged 18K libhesper_wasm.a
No native code paths change; this only adds a wasm-side staging recipe.
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.