Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
b3e6896
wasm: capture IO.println via Module.print, route into cell output
junjihashimoto Jun 10, 2026
86bcb40
feat(wasm): generic EXTRA_WASM_DIRS for third-party Lean libraries
junjihashimoto Jun 10, 2026
86048c2
ci: switch wasm build to EXTRA_WASM_DIRS (drops Hesper-as-submodule)
junjihashimoto Jun 10, 2026
3fbc52e
Dockerfile.docs-builder: drop hesper/, hesper-wasm/ COPY + build
junjihashimoto Jun 10, 2026
0e5afc9
docs(README): explain xeus-lean's vendor-agnostic extension contract
junjihashimoto Jun 10, 2026
442fe1d
Remove Sparkle-specific build wiring + drop examples/sparkle, noteboo…
junjihashimoto Jun 10, 2026
2deb4c8
ci + docker: remove Sparkle/Hesper build steps; wire in mock-extra pl…
junjihashimoto Jun 10, 2026
4c73161
REPL + Display + notebooks: drop hard-coded Sparkle/Hesper imports
junjihashimoto Jun 10, 2026
340068a
Add tests/fixtures/mock-extra/ — reference plug-in fixture
junjihashimoto Jun 10, 2026
63bfecf
test_wasm_node: assert mock-extra fixture round-trips end-to-end
junjihashimoto Jun 10, 2026
be9ef49
EXTRA_WASM_DIRS: ship umbrella-only oleans, .xeus-auto-imports + test…
junjihashimoto Jun 11, 2026
43b70c5
test_wasm_node: skip mock-extra assertion when fixture isn't in VFS
junjihashimoto Jun 11, 2026
1ec4977
mock-extra/build-wasm.sh: archive Lean-generated wrappers + export lp…
junjihashimoto Jun 11, 2026
93e7dd7
mock-extra/build-wasm.sh: weak mi_malloc_small shim for archive-order…
junjihashimoto Jun 12, 2026
a1fa139
fix(mock-extra): undef LEAN_MIMALLOC in wrappers to dodge heap mismatch
junjihashimoto Jun 12, 2026
1d7784b
test(e2e): drop sparkle hdl describe; skip CI-flaky #latex MathJax
junjihashimoto Jun 12, 2026
f3fad63
fix(wasm): isolate rich-display output from instrumentation stderr
junjihashimoto Jun 12, 2026
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
129 changes: 20 additions & 109 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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: |
Expand Down Expand Up @@ -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/
Expand Down Expand Up @@ -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.
# ============================================================
Expand Down
3 changes: 0 additions & 3 deletions .github/workflows/docs.yml
Original file line number Diff line number Diff line change
Expand Up @@ -63,9 +63,6 @@ jobs:
- 'lean-toolchain'
- 'pixi.toml'
- 'pixi.lock'
- 'examples/sparkle/**'
- 'hesper/**'
- 'hesper-wasm/**'
- 'scripts/**'
- 'Dockerfile.docs-builder'
- '.github/workflows/docs.yml'
Expand Down
3 changes: 0 additions & 3 deletions .gitmodules

This file was deleted.

Loading
Loading