Verify website examples in the browser

.github/workflows/pages.yml

@@ -0,0 +1,65 @@
+name: Build and deploy website
+on:
+  push:
+    branches: [main]
+  pull_request:
+  workflow_dispatch:
+permissions:
+  contents: read
+concurrency:
+  group: pages-${{ github.event.pull_request.number || 'deploy' }}
+  cancel-in-progress: true
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v4
+        with:
+          node-version: "22"
+      - name: Check out shared browser verifier
+        uses: actions/checkout@v4
+        with:
+          repository: liquid-java/liquidjava-docs
+          ref: 7b61cdde7010b06629c4cdaf298e5b54daba4f63
+          path: .browser-source
+
+      - name: Set up Java
+        uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: "17"
+
+      - name: Build shared browser verifier
+        working-directory: .browser-source
+        run: |
+          npm ci --ignore-scripts --no-audit --no-fund
+          npm run build:playground
+          npm run test:playground
+          node scripts/playground/export.mjs ..
+
+      - name: Check gallery script
+        run: node --check assets/js/gallery.js
+      - name: Stage website
+        run: |
+          mkdir _site
+          cp index.html robots.txt sitemap.xml llms.txt _headers .nojekyll isolation.js _site/
+          cp -R assets .well-known verifier _site/
+      - uses: actions/upload-pages-artifact@v3
+        if: github.event_name != 'pull_request'
+        with:
+          path: _site
+  deploy:
+    if: github.event_name != 'pull_request'
+    needs: build
+    runs-on: ubuntu-latest
+    permissions:
+      pages: write
+      id-token: write
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - uses: actions/configure-pages@v5
+      - uses: actions/deploy-pages@v4
+        id: deployment

.gitignore

@@ -18,3 +18,10 @@ scripts/
 
 # Logs
 *.log
+
+# generated browser runtime
+verifier/
+isolation.js
+.browser-source/
+
+_site/

README.md

@@ -4,18 +4,24 @@ Source for the [LiquidJava](https://github.com/liquid-java) project website, ser
 
 ## Local preview
 
-No build step, no package manager. Open `index.html` directly, or serve the directory:
+Build the shared verifier in the adjacent docs checkout with JDK 17, then export it here:
 
 ```sh
-python3 -m http.server 8000
-# then visit http://localhost:8000
+cd ../liquidjava-docs
+npm ci
+npm run build:playground
+node scripts/playground/export.mjs ../liquid-java.github.io
+node node_modules/http-server/bin/http-server ../liquid-java.github.io -p 8001 -c-1
 ```
 
+Open `http://localhost:8001`. Use HTTPS or localhost and a server with HTTP range support for the JARs. The isolation service worker reloads once; the verifier itself loads on the first Run. Each usage is checked together with its displayed specification, locally in a worker. Results contain only diagnostic titles and messages. Stop, changing examples, and changing tabs cancel pending verification.
+
 ## Structure
 
 - `index.html` — single-page site (markup, content, and inline JS for navbar + theme toggle).
 - `assets/css/style-starter.css` — vendored W3layouts template stylesheet plus LiquidJava overrides. Theme rules layered via `.light-theme` / `.dark-theme` on `<body>`.
-- `assets/js/jquery-3.3.1.min.js` — only JS dependency.
+- `assets/js/gallery.js` — gallery selection and browser verification.
+- `assets/js/jquery-3.3.1.min.js` — vendored jQuery.
 - `assets/images/`, `assets/docs/`, `assets/extension/` — static assets (images, poster PDF, VSCode `.vsix`).
 
 ## Theme toggle
@@ -24,11 +30,13 @@ Dark/light mode is toggled by inline JS at the bottom of `index.html`. The selec
 
 ## Deploying
 
-Push to `main`. GitHub Pages publishes the site automatically.
+Select **GitHub Actions** as the Pages build source. The Pages workflow builds the runtime from a pinned commit of `liquid-java/liquidjava-docs`, validates it, and publishes the static site on pushes to `main`. Update the checkout `ref` after testing a shared-runtime upgrade. Generated `verifier/` and `isolation.js` files are ignored by Git.
 
 ## Related repositories
 
 - [`liquidjava`](https://github.com/liquid-java/liquidjava) — verifier, API, examples
 - [`liquidjava-docs`](https://github.com/liquid-java/liquidjava-docs) — documentation
 - [`liquidjava-tutorial`](https://github.com/liquid-java/liquidjava-tutorial) — tutorial
 - [`vscode-liquidjava`](https://github.com/liquid-java/vscode-liquidjava) — VSCode extension
+
+The introduction video opens on YouTube because the cross-origin isolation required by the verifier prevents embedding its player. Neighboring GitHub Pages projects are excluded from the root isolation worker’s navigation responses.

assets/css/style-starter.css

@@ -12416,24 +12416,6 @@ body:after {
   margin-left: -12%;
 }
 
-.iframe_container{
-  position: relative;
-  overflow: hidden;
-  width: 100%;
-  padding-top: 56.25%; /* 16:9 Aspect Ratio (divide 9 by 16 = 0.5625) */
-}
-
-/* Then style the iframe to fit in the container div with full height and width */
-.responsive-iframe {
-  position: absolute;
-  top: 0;
-  left: 0;
-  bottom: 0;
-  right: 0;
-  width: 100%;
-  height: 100%;
-}
-
 .small_p {
   margin: 1%!important;
 }
@@ -13903,3 +13885,7 @@ body.dark-theme .lj-resource-card--muted .lj-resource-icon { background: transpa
   .lj-steps { grid-template-columns: 1fr; gap: 1.6rem; }
   .lj-install-title { font-size: 1.55rem; }
 }
+
+.lj-verifier-body p { margin: 0 0 0.75rem; }
+.lj-verifier-body p:last-child { margin-bottom: 0; }
+.lj-run:disabled { opacity: 0.6; cursor: wait; }

assets/examples/data/abstract-undoable-edit/correct.java

@@ -1,6 +1,12 @@
-// Path: aliveDone -> aliveNotDone -> aliveDone -> aliveNotDone -> aliveDone
-AbstractUndoableEdit edit = new AbstractUndoableEdit();
-edit.undo();
-edit.redo();
-edit.undo();
-edit.redo();
+import javax.swing.undo.AbstractUndoableEdit;
+
+class Example {
+    static void example() throws Exception {
+        // Path: aliveDone -> aliveNotDone -> aliveDone -> aliveNotDone -> aliveDone
+        AbstractUndoableEdit edit = new AbstractUndoableEdit();
+        edit.undo();
+        edit.redo();
+        edit.undo();
+        edit.redo();
+    }
+}

assets/examples/data/abstract-undoable-edit/incorrect.java

@@ -1,6 +1,12 @@
-// Violation: redo() called twice in a row — second call is in state aliveDone.
-AbstractUndoableEdit edit = new AbstractUndoableEdit();
-edit.undo();
-edit.redo();
-edit.redo();   // INVALID: redo() requires aliveNotDone(edit),
-               //          but edit is in state aliveDone
+import javax.swing.undo.AbstractUndoableEdit;
+
+class Example {
+    static void example() throws Exception {
+        // Violation: redo() called twice in a row — second call is in state aliveDone.
+        AbstractUndoableEdit edit = new AbstractUndoableEdit();
+        edit.undo();
+        edit.redo();
+        edit.redo();   // INVALID: redo() requires aliveNotDone(edit),
+                       //          but edit is in state aliveDone
+    }
+}

assets/examples/data/abstract-undoable-edit/spec.java

@@ -1,3 +1,6 @@
+import liquidjava.specification.*;
+import javax.swing.undo.AbstractUndoableEdit;
+
 @StateSet({"aliveDone", "aliveNotDone", "notAlive"})
 @ExternalRefinementsFor("javax.swing.undo.AbstractUndoableEdit")
 public interface AbstractUndoableEditRefinementsExpert {

assets/examples/data/buffered-reader/correct.java

@@ -1,7 +1,14 @@
-// Path: open -> open -> marked -> marked -> open -> open
-BufferedReader br = new BufferedReader(in);
-br.read();
-br.mark(42);
-br.read();
-br.reset();
-br.read();
+import java.io.BufferedReader;
+import java.io.Reader;
+
+class Example {
+    static void example(Reader in) throws Exception {
+        // Path: open -> open -> marked -> marked -> open -> open
+        BufferedReader br = new BufferedReader(in);
+        br.read();
+        br.mark(42);
+        br.read();
+        br.reset();
+        br.read();
+    }
+}

assets/examples/data/buffered-reader/incorrect.java

@@ -1,7 +1,14 @@
-// Violation: reset() called twice — second call is in state `open`.
-BufferedReader br = new BufferedReader(in);
-br.mark(42);
-br.read();
-br.reset();
-br.reset();   // INVALID: reset() requires marked(br),
-              //          but br is in state open
+import java.io.BufferedReader;
+import java.io.Reader;
+
+class Example {
+    static void example(Reader in) throws Exception {
+        // Violation: reset() called twice — second call is in state `open`.
+        BufferedReader br = new BufferedReader(in);
+        br.mark(42);
+        br.read();
+        br.reset();
+        br.reset();   // INVALID: reset() requires marked(br),
+                      //          but br is in state open
+    }
+}

assets/examples/data/buffered-reader/spec.java

@@ -1,3 +1,7 @@
+import liquidjava.specification.*;
+import java.io.BufferedReader;
+import java.io.Reader;
+
 @RefinementAlias("NonNegative(int v) { v >= 0 }")
 @RefinementAlias("Positive(int v) { v > 0 }")
 @StateSet({"open", "marked", "closed"})

assets/examples/data/choice-callback/correct.java

@@ -1,7 +1,13 @@
-// Path: multiple -> multiple -> multiple
-// Constructor's last argument is `true`, so the SMT solver
-// concludes the result is in state `multiple`.
-ChoiceCallback cb = new ChoiceCallback(
-    "Pick options", new String[]{"a", "b"}, 0, true);
-cb.setSelectedIndexes(new int[]{0});
-cb.setSelectedIndexes(new int[]{0, 1});
+import javax.security.auth.callback.ChoiceCallback;
+
+class Example {
+    static void example() throws Exception {
+        // Path: multiple -> multiple -> multiple
+        // Constructor's last argument is `true`, so the SMT solver
+        // concludes the result is in state `multiple`.
+        ChoiceCallback cb = new ChoiceCallback(
+            "Pick options", new String[]{"a", "b"}, 0, true);
+        cb.setSelectedIndexes(new int[]{0});
+        cb.setSelectedIndexes(new int[]{0, 1});
+    }
+}

assets/examples/data/choice-callback/incorrect.java

@@ -1,6 +1,12 @@
-// Violation: last constructor argument is `false` -> state `single`,
-// where setSelectedIndexes() is forbidden.
-ChoiceCallback cb = new ChoiceCallback(
-    "Pick one", new String[]{"a", "b"}, 0, false);
-cb.setSelectedIndexes(new int[]{0});   // INVALID: requires multiple(cb),
-                                       //          but cb is in state single
+import javax.security.auth.callback.ChoiceCallback;
+
+class Example {
+    static void example() throws Exception {
+        // Violation: last constructor argument is `false` -> state `single`,
+        // where setSelectedIndexes() is forbidden.
+        ChoiceCallback cb = new ChoiceCallback(
+            "Pick one", new String[]{"a", "b"}, 0, false);
+        cb.setSelectedIndexes(new int[]{0});   // INVALID: requires multiple(cb),
+                                               //          but cb is in state single
+    }
+}

assets/examples/data/choice-callback/spec.java

@@ -1,3 +1,6 @@
+import liquidjava.specification.*;
+import javax.security.auth.callback.ChoiceCallback;
+
 @StateSet({"single", "multiple"})
 @ExternalRefinementsFor("javax.security.auth.callback.ChoiceCallback")
 public interface ChoiceCallbackRefinementsExpert {

assets/examples/data/email/correct.java

@@ -1,6 +1,11 @@
-// Path: emptyEmail -> senderSet -> receiverSet -> receiverSet -> bodySet
-Email e = new Email();
-e.from("Alice");
-e.to("Bob");
-e.to("Carol");
-e.body("Hello!");
+
+class Example {
+    static void example() throws Exception {
+        // Path: emptyEmail -> senderSet -> receiverSet -> receiverSet -> bodySet
+        Email e = new Email();
+        e.from("Alice");
+        e.to("Bob");
+        e.to("Carol");
+        e.body("Hello!");
+    }
+}

assets/examples/data/email/incorrect.java

@@ -1,6 +1,11 @@
-// Violation: to() called before from() — sender was never set.
-Email e = new Email();
-e.to("Bob");          // INVALID: requires senderSet or receiverSet,
-                      //          but e is still in emptyEmail
-e.from("Alice");
-e.body("Hello!");
+
+class Example {
+    static void example() throws Exception {
+        // Violation: to() called before from() — sender was never set.
+        Email e = new Email();
+        e.to("Bob");          // INVALID: requires senderSet or receiverSet,
+                              //          but e is still in emptyEmail
+        e.from("Alice");
+        e.body("Hello!");
+    }
+}

assets/examples/data/email/spec.java

@@ -1,20 +1,22 @@
+import liquidjava.specification.*;
+
 @StateSet({"emptyEmail", "receiverSet", "senderSet", "bodySet"})
 public class Email {
 
   @StateRefinement(to = "emptyEmail(this)")
-  public Email() {...}
+  public Email() {}
 
   @StateRefinement(from = "emptyEmail(this)", to = "senderSet(this)")
-  public void from(String s) {...}
+  public void from(String s) {}
 
   @StateRefinement(from = "(senderSet(this)) || (receiverSet(this))",
                    to   = "receiverSet(this)")
-  public void to(String s) {...}
+  public void to(String s) {}
 
   @StateRefinement(from = "receiverSet(this)", to = "receiverSet(this)")
-  public void subject(String s) {...}
+  public void subject(String s) {}
 
   @StateRefinement(from = "receiverSet(this)", to = "bodySet(this)")
-  public void body(String s) {...}
+  public void body(String s) {}
 
 }

assets/examples/data/image-write-param/correct.java

@@ -1,15 +1,22 @@
-ImageWriteParam p = new ImageWriteParam(Locale.US);
-// state: startTiling && startCompression
+import javax.imageio.ImageWriteParam;
+import java.util.Locale;
 
-// --- Tiling axis: drive it independently ---
-p.setTilingMode(2);            // -> tilingExplicit
-p.setTiling(64, 64, 0, 0);     // -> tilingSet
-int w = p.getTileWidth();      // ok in tilingSet
+class Example {
+    static void example() throws Exception {
+        ImageWriteParam p = new ImageWriteParam(Locale.US);
+        // state: startTiling && startCompression
 
-// --- Compression axis: still in startCompression, advance now ---
-p.setCompressionMode(2);       // -> compressionExplicit
-p.setCompressionType("JPEG");  // -> compressionSet
-String t = p.getCompressionType();
+        // --- Tiling axis: drive it independently ---
+        p.setTilingMode(2);            // -> tilingExplicit
+        p.setTiling(64, 64, 0, 0);     // -> tilingSet
+        int w = p.getTileWidth();      // ok in tilingSet
 
-// Order between axes doesn't matter — the two state machines
-// are orthogonal. Each method only constrains its own axis.
+        // --- Compression axis: still in startCompression, advance now ---
+        p.setCompressionMode(2);       // -> compressionExplicit
+        p.setCompressionType("JPEG");  // -> compressionSet
+        String t = p.getCompressionType();
+
+        // Order between axes doesn't matter — the two state machines
+        // are orthogonal. Each method only constrains its own axis.
+    }
+}