ci(pages): fix JupyterLite "No Kernel" — absolute argv[0] in xlean kernel.json#87
Merged
Merged
Conversation
…rnel.json (#85) The hosted lab (https://verilean.github.io/sparkle/lab/) showed "No Kernel": the deployed `xeus/kernels.json` was `[]`, so no Lean kernel was offered. Root cause (traced through jupyterlite-xeus add_on.py): The Sparkle WASM kernel rebuild step does `cmake --install /work/.wasm-rebuild` into the staging prefix. That installs xeus-lean's **source** `kernel.json`, whose argv is the bare relative string: "argv": [ "xlean" ] (The image's stock env kernel.json uses an *absolute* `/opt/.../bin/xlean`, but `cmake --install` clobbers it with the relative source template.) `jupyter lite build` → `jupyterlite_xeus.add_on.get_kernel_binaries` reads `argv[0]` and checks `argv[0] + ".js"` / `+ ".wasm"`. With `argv[0] == "xlean"` those resolve relative to the build cwd (`/work`), where `xlean.js` / `xlean.wasm` do NOT exist — the real binaries are at `$CAND/bin/xlean.{js,wasm}`. So it warns "kernel binaries not found for xlean", drops xlean from the manifest, and the deployed `kernels.json` comes out `[]`. Fix: after `cmake --install`, rewrite the installed kernel.json's sole argv line from the relative `"xlean"` to the absolute `$CAND/bin/xlean` (sed on the standalone argv line — the image has no jq, and sed avoids the nested-heredoc quoting hazard inside the docker `bash -c '…'`). Verified inside the docs-builder image that `get_kernel_binaries` then resolves both xlean.js and xlean.wasm (FOUND, vs NOT FOUND before), which is what populates `xeus/kernels.json` and lets the lab offer the Lean 4 kernel.
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
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.
Problem
The hosted lab https://verilean.github.io/sparkle/lab/ shows "No Kernel" — no Lean 4 kernel is offered. The deployed
xeus/kernels.jsonis[].Closes #85.
Root cause
The WASM kernel rebuild step runs
cmake --installinto the staging prefix, which installs xeus-lean's sourcekernel.json. That template's argv is the bare relative string:(The stock env kernel.json uses an absolute
/opt/.../bin/xlean, butcmake --installclobbers it.)jupyter lite build→jupyterlite_xeus.add_on.get_kernel_binariesreadsargv[0]and checksargv[0] + ".js"/+ ".wasm". Withargv[0] == "xlean"those resolve relative to the build cwd (/work), where the binaries do not exist — the real ones are at$CAND/bin/xlean.{js,wasm}. So it warns "kernel binaries not found for xlean", drops the kernel, andkernels.jsoncomes out[].Fix
After
cmake --install, rewrite the installed kernel.json's sole argv line from the relative"xlean"to the absolute$CAND/bin/xlean. Usessedon the standalone argv line — the docs-builder image has nojq, andsedavoids the nested-heredoc quoting hazard inside the dockerbash -c '…'.Verification
Confirmed inside the docs-builder image that after the rewrite
get_kernel_binariesresolves bothxlean.jsandxlean.wasm(FOUND, vs NOT FOUND before) — which is what populatesxeus/kernels.jsonand lets the lab offer the Lean 4 kernel.