Add a browser-native LiquidJava playground - #3
Merged
Merged
Conversation
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>
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>
Co-authored-by: Codex <codex@openai.com>
CatarinaGamboa
approved these changes
Oct 4, 2026
| ROOT = Path(__file__).resolve().parents[2] | ||
| WORK = ROOT / '.playground-build' | ||
| OUTPUT = ROOT / 'playground/runtime' | ||
| VERIFIER = '0.0.35' |
There was a problem hiding this comment.
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
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.
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.
How it works
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