Skip to content

Add a browser-native LiquidJava playground - #3

Merged
rcosta358 merged 21 commits into
mainfrom
codex/browser-playground
Oct 4, 2026
Merged

rcosta358 merged 21 commits into
mainfrom
codex/browser-playground

Conversation

@rcosta358

@rcosta358 rcosta358 commented Oct 3, 2026 •

Copy link
Copy Markdown
Collaborator

Description

Add a browser playground with editable Java examples, inline diagnostics, and verification controls. Verification runs locally, without a server or changes to the LiquidJava verifier sources.

image

How it works

  • Java in the browser: recompile the published verifier for Java 17 and run it through CheerpJ in a browser worker.
  • Z3 WebAssembly: replace desktop native-library loading with an adapter connecting the existing Z3 Java API to Z3 WASM.
  • Spoon support: supply its classpath and adapt empty exception stack traces so typestate checks work in CheerpJ.
  • GitHub Pages: use a playground-scoped service worker to add the isolation headers Z3 requires; build the runtime automatically in the Pages workflow.

Currently supports one Java 8 source file with bundled annotations and core Java types; external dependencies are unavailable.

Validation: runtime and Jekyll builds, three adapter tests, and browser checks for valid/invalid refinements, aliases, typestates, syntax errors, cancellation, and the GitHub Pages project path passed.

🤖 Generated with Codex

Run the published verifier locally through CheerpJ with a Z3 WebAssembly
native-method adapter and playground-scoped cross-origin isolation.
Build the runtime in the docs Pages workflow and show source diagnostics.

Co-authored-by: Codex <codex@openai.com>
@rcosta358 rcosta358 added documentation Improvements or additions to documentation enhancement New feature or request labels Oct 3, 2026
rcosta358 and others added 20 commits October 4, 2026 00:50
Underline declared names and reported expression or syntax spans instead
of whole lines, and navigate to the corresponding offset.

Co-authored-by: Codex <codex@openai.com>
Match the VS Code diagnostic range from the declared name through the
initializer, excluding the final delimiter and preceding annotations.

Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>
Co-authored-by: Codex <codex@openai.com>

@CatarinaGamboa CatarinaGamboa left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Amazing! Minor commnet

ROOT = Path(__file__).resolve().parents[2]
WORK = ROOT / '.playground-build'
OUTPUT = ROOT / 'playground/runtime'
VERIFIER = '0.0.35'

@CatarinaGamboa CatarinaGamboa Oct 4, 2026 •

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we might want to make this also updatable like the other repos with a PR when we have a new version available Nvm is in #4

@rcosta358
rcosta358 merged commit 0fe4915 into main Oct 4, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

documentation Improvements or additions to documentation enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants