notebook_run_cell — read-run-publish in one MCP call#15
Merged
Conversation
Adds a `notebook_run_cell` MCP tool that combines the four-step
recipe an agent needs to make a kernel-side computation visible
in the user's open JupyterLab tab without a reload:
1. Read the cell at (path, index) from the .ipynb.
2. Send its source through `KernelBridge.execute` to the live
xeus-lean kernel.
3. Embed the resulting outputs back into the cell via Jupyter
Server's `PUT /api/contents/<path>` (so
jupyter-collaboration's Y.js doc store hears the update
and pushes the diff to every connected browser live).
4. Shell out to `jupyter trust` so the browser's per-session
trust gate doesn't quarantine `image/svg+xml` / `text/html`
payloads as untrusted.
Multi-key MIME bundles (a single `display_data` carrying both
`text/plain` and `image/svg+xml`, as `Display.waveform` does)
get split into one output per MIME type, because JupyterLab
picks the highest-priority renderer within a bundle and hides
the others. Without the split, an agent that prints a build
log AND draws a waveform only sees the waveform appear; with
the split both render.
Drive-by: `Net/HTTP.lean`'s `Content-Length` was computed from
`body.length` (character count), which under-reports when the
body contains the multi-byte UTF-8 characters Lean writes
(`←`, `→`, `≥`, `λ`, …). Jupyter Server then read a truncated
body and rejected the PUT as invalid JSON. Switch to
`body.toUTF8.size` for byte-correct framing.
Add a `#load_file "/path/to/foo.lean"` command magic that reads a
Lean source file from disk and elaborates its commands into the
running kernel session's current environment. Behaves like
pasting the file's contents into a cell:
- definitions, theorems, instances, `open`s, `namespace`s,
`@[extern]` declarations etc. all land in the current env
- one error in the loaded file no longer aborts the cell — every
`MessageLog` diagnostic is forwarded individually via
`logInfo` / `logWarning` / `logError` so the user sees what
landed and what didn't
- module-header `import`s inside the loaded file are silently
ignored because xeus-lean's REPL locks the import list to
what was loaded at session start; we can't add new modules
on the fly here
Internals: pipes the file content through `Lean.Elab.process`
(which is the same `IO.processCommands` loop the compiler uses
for an offline build), then merges the resulting environment
back via `setEnv`.
Pair with `file_write` (or the MCP `file_write` tool) to get a
"draft a snippet → save it → splice it into the live env" loop
without restarting the session.
junjihashimoto
had a problem deploying
to
github-pages
GitHub Actions
Failure
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.
Summary
Adds
notebook_run_cell(ipynb_path, cell_index)to xlean-mcp. It collapses the four-step recipe an MCP host needs to make a kernel-side computation visible in the user's open JupyterLab tab WITHOUT a page reload, all in one call:(path, index).KernelBridge.PUT /api/contents/<path>so jupyter-collaboration's Y.js doc store hears the update and pushes the diff to every connected browser client live.jupyter trustthe file so the browser's per-session trust gate doesn't quarantineimage/svg+xml/text/htmlpayloads as untrusted (the cause of "the cell ran but my SVG only shows after F5" pain).MIME-bundle splitting
A
display_datawhosedatacarries BOTHtext/plainandimage/svg+xml(the shapeDisplay.waveformemits — log + render in one bundle) gets rendered by JupyterLab as the SVG ONLY: the renderer picks the highest-priority MIME and treats the others as fallbacks. The agent sees the SVG appear but the build log silently disappears.outputToCellssplits multi-key bundles into onedisplay_dataper MIME type, so both render. Enumerated against the MIME types xeus-lean'sDisplay.*actually emits (text/plain, text/html, image/svg+xml, image/png, image/jpeg, text/markdown, text/latex, application/json, jupyter-widget-view) rather than iteratingJson.obj's underlyingTreeMap.Raw(whose API moves between Lean versions).Drive-by fix in
Net/HTTP.leanContent-Lengthwas being computed frombody.length— Lean's character count, which under-reports when the body contains the multi-byte UTF-8 characters Lean writes (←,→,≥,λ, …). Jupyter Server then read a truncated body and rejected the PUT with400: Invalid JSON in body of request. Switching tobody.toUTF8.sizegives byte-correct framing.Test plan
tools/listshowsnotebook_run_celltools/call notebook_run_cellagainst a cell whose source draws a Sparkle JIT waveform:outputs_written≥ 2 (split worked)text/plainAND the SVG, live, no reloadmetadata.signatureset (jupyter trust ran)←inlet count ← Signal.reg 0#4) survives Content-Length framing