Dockerfile.wasm

FROM ghcr.io/prefix-dev/pixi:latest AS builder

# Install curl, git for elan, xz-utils for node binary, and python3
# for the pixi-prefix discovery and kernel.json rewrite steps.
RUN apt-get update && apt-get install -y curl git xz-utils python3 && rm -rf /var/lib/apt/lists/*

# Install Lean via elan
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
ENV PATH="/root/.elan/bin:${PATH}"

# Install Node.js 23+ (required by emscripten Memory64 WASM output)
# pixi bundles node v16 which is too old for wasm64
RUN curl -fsSL https://nodejs.org/dist/v23.6.0/node-v23.6.0-linux-x64.tar.xz \
    | tar -xJ -C /usr/local --strip-components=1

WORKDIR /opt/xeus-lean

# Copy pixi configuration first for better caching
COPY pixi.toml pixi.lock* ./

# Install wasm-build and wasm-host environments
RUN pixi install -e wasm-build || pixi install -e wasm-build --no-lockfile-update
RUN pixi install -e wasm-host || pixi install -e wasm-host --no-lockfile-update

# Copy source
COPY . .

# Build Lean REPL (generates .c files needed by cmake)
# Display is a separate lib providing #html/#latex/#md/#svg commands;
# 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

# Build WASM kernel
# 1. Fix emscripten symlinks
RUN pixi run -e wasm-build fix-emscripten-links || true

# 2. Configure with emcmake (match CI flags)
RUN pixi run -e wasm-build emcmake cmake -S . -B wasm-build \
      -DCMAKE_BUILD_TYPE=Release \
      -DCMAKE_FIND_ROOT_PATH_MODE_PACKAGE=ON

# 3. Build with emmake
RUN pixi run -e wasm-build emmake make -C wasm-build -j$(nproc) xlean test_wasm_node

# 4. Run WASM tests with system Node.js 23+
RUN node --experimental-wasm-memory64 wasm-build/test_wasm_node.js

# 5. Install to wasm-host prefix and rewrite kernel.json argv to
#    an absolute path (jupyterlite-xeus reads argv[0] verbatim and
#    appends .js/.wasm to locate the kernel binaries).
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") && \
    echo "=== Installing to PREFIX: $PREFIX ===" && \
    pixi run -e wasm-build cmake --install wasm-build --prefix "$PREFIX" && \
    ABS_PREFIX=$(realpath "$PREFIX") && \
    python3 -c "import json,pathlib; \
p=pathlib.Path('$PREFIX/share/jupyter/kernels/xlean/kernel.json'); \
spec=json.loads(p.read_text()); \
spec['argv']=['$ABS_PREFIX/bin/xlean']; \
p.write_text(json.dumps(spec, indent=2))" && \
    echo "=== Verifying installation ===" && \
    ls -lh "$PREFIX/bin/" | grep xlean && \
    ls -lh "$PREFIX/share/jupyter/kernels/xlean/" && \
    cat "$PREFIX/share/jupyter/kernels/xlean/kernel.json"

# 6. Generate JupyterLite static site
RUN mkdir -p notebooks && \
    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") && \
    echo "=== Building JupyterLite with PREFIX: $PREFIX ===" && \
    pixi run -e wasm-build jupyter lite build \
      --XeusAddon.prefix="$PREFIX" \
      "--XeusAddon.default_channels=[https://conda.anaconda.org/conda-forge]" \
      --contents notebooks \
      --output-dir _output \
      --force && \
    echo "=== Verifying JupyterLite output ===" && \
    find _output -name "xlean*" -ls && \
    cat _output/xeus/kernels.json

# 7. Pack olean assets (Std/Lean/Sparkle) 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/*
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 olean tarballs:" && \
      ls -lh _output/xeus/wasm-host/olean/; \
    fi

# --- Serve stage ---
FROM python:3.12-slim

WORKDIR /app
COPY --from=builder /opt/xeus-lean/_output /app/dist

EXPOSE 8888

CMD ["python", "-m", "http.server", "8888", "--directory", "/app/dist"]
# cache-bust 1776418690