[formal-systems]

What

Adds a Run in VS Code button next to Run TLC in every lesson and spec playground. It opens this repository in a GitHub codespace with the full TLA+ tooling and hands over the current spec and config, including the learner's edits.

• .devcontainer/: Ubuntu with Java 21 (for TLC), Node 24, the tlaplus.vscode-ide extension, every lesson exported as .tla/.cfg files under lessons/, and a clone of tlaplus/Examples. A welcome page explains the flow.
• scripts/export-lessons.mjs (npm run export-lessons): writes each lesson's spec and config to lessons/<section>/<lesson>/<Module>.{tla,cfg}, reusing src/lib/parse-lesson.ts.
• Handoff: the site and the codespace can't talk to each other directly, so the button copies a one-line command, echo <base64url payload> | node scripts/run-in-codespace.mjs. Pasted into the codespace terminal, it writes the files to playground/<dir>/, opens them in the editor and runs TLC. Folder and file names from the payload are restricted to plain names, so a payload can't write outside playground/.
• The codespace repo and branch can be set with NEXT_PUBLIC_CODESPACES_REPO / NEXT_PUBLIC_CODESPACES_REF, for testing from a fork. The default is tlaplus/tla-by-example.

Large specs

Linux caps a single program argument at 128 KiB, so the payload is piped in by bash's builtin echo instead of being passed as an argument, and the script reads it from stdin as a stream. Spec pages also send only the modules the spec transitively EXTENDS/INSTANCEs. The largest one, SpecifyingSystems, goes from about 235 KB to about 62 KB.

Testing

• npm test: 54 tests, including new suites for the handoff lib (module naming, sanitising, non-ASCII round-trip, module pruning), the Playground button (copy, open, banner, dismiss) and run-in-codespace.mjs (rejected folder and file names, bad payloads, a 300 KB payload). Run on macOS and in a node:24-bookworm container.
• tsc --noEmit and npm run build pass.
• In a Linux container: a 400 KB pasted command writes its files intact, while the old argument form fails with Argument list too long.
• End to end with the TLA+ extension's tla2tools.jar: a handed-over lesson spec model-checks with "No error has been found".
• Every spec page's spec/config combination parses with SANY after module pruning. 7 combinations fail with and without pruning alike, because they need TLAPS or the community modules, which the standalone jar lacks.
• Not covered automatically: the devcontainer itself, which can only be checked by starting a real codespace.

🤖 Generated with Claude Code

[FedericoPonzi]

I've checked out the branch locally and run it.
Preview:

I'm not fully convinced by "Run in Vs Code" as a label, when i click it I would expect my vscode to open up, but instad gets opened in codespaces. I didn't have a codespace setup, so I was a bit confused on how to move forward. After I created it, the vscode loaded with the repo checked out - the file I was looking at it's not opened. Going back to the page now I see:

After I pasted this to the terminal of my codespace, it fails with an error but I guess it's caused by missing files added by this PR. One UX change I'd ask is that as a user I click on Open in vscode, the bar is shown with echo command,, then I can click on a new button to open in a new tab. We can also explain that it will open codespaces and have a link to the documentation. For now, I think it's worth merging so that it can be better tested. Thank you!