Verify tutorial exercises in the browser

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

Author: rcosta358

.github/workflows/pages.yml

@@ -4,15 +4,14 @@ on:
   push:
     branches:
       - main
+  pull_request:
   workflow_dispatch:
 
 permissions:
   contents: read
-  pages: write
-  id-token: write
 
 concurrency:
-  group: pages
+  group: pages-${{ github.event.pull_request.number || 'deploy' }}
   cancel-in-progress: true
 
 jobs:
@@ -29,6 +28,27 @@ jobs:
           cache: npm
           cache-dependency-path: package-lock.json
 
+      - 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: Install dependencies
         run: npm ci
 
@@ -37,21 +57,26 @@ jobs:
           npm run check
           npm run build
 
-      - name: Configure GitHub Pages
-        uses: actions/configure-pages@v5
-
       - name: Upload GitHub Pages artifact
+        if: github.event_name != 'pull_request'
         uses: actions/upload-pages-artifact@v4
         with:
           path: dist/client
 
   deploy:
+    if: github.event_name != 'pull_request'
+    permissions:
+      pages: write
+      id-token: write
     needs: build
     runs-on: ubuntu-latest
     environment:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}
     steps:
+      - name: Configure GitHub Pages
+        uses: actions/configure-pages@v5
+
       - name: Deploy to GitHub Pages
         id: deployment
         uses: actions/deploy-pages@v4

.gitignore

@@ -141,3 +141,8 @@ dist
 vite.config.js.timestamp-*
 vite.config.ts.timestamp-*
 .vite/
+
+# generated shared browser verifier
+verifier/
+isolation.js
+.browser-source/

README.md

@@ -7,11 +7,11 @@ This repository contains a web-based, interactive introduction to LiquidJava. Th
 3. External socket state refinements;
 4. Stack ghost variables.
 
-Learners can edit Java snippets, run lightweight in-browser checks, answer quick knowledge questions, and move freely between sections. The tutorial does not collect, persist, or export user data.
+Learners can edit Java snippets, run LiquidJava verification in the browser, answer quick knowledge questions, and move freely between sections. The tutorial does not collect, persist, or export user data.
 
 ## Preview Locally
 
-Run the local development server:
+Build and export the shared runtime as described below, then run the local development server:
 
 ```sh
 npm run dev
@@ -27,11 +27,24 @@ Each lesson contains:
 
 - Explanatory copy and a read-only example;
 - Starter and solution code;
-- Regular-expression checks for the coding task;
+- A Java filename and exercise-pattern hints for the coding task;
 - Automatically checked multiple-choice and short-answer questions.
 
 Add, remove, or reorder lesson objects to change the tutorial without editing `app.js` or `index.html`.
 
 ## Checker Scope
 
-The browser checker is intentionally lightweight: it recognizes the requested annotations and values but does not run the LiquidJava compiler. Use the LiquidJava VS Code extension for real verification tasks.
+Checks run the real LiquidJava verifier locally in a browser worker. Results show diagnostic titles and messages. Exercise-pattern hints are separate from verification: valid Java with a missing requested contract is reported as “Exercise incomplete”. Editing, resetting, or leaving a lesson cancels pending verification.
+
+Before development or building, build the shared runtime in the adjacent `liquidjava-docs` checkout with JDK 17, then export it here:
+
+```sh
+cd ../liquidjava-docs
+npm ci
+npm run build:playground
+node scripts/playground/export.mjs ../liquidjava-interactive-tutorial
+cd ../liquidjava-interactive-tutorial
+npm run dev
+```
+
+The workflow builds and exports the runtime from a pinned docs commit, validates pull requests, and deploys only from `main`. Update the checkout `ref` after testing a shared-runtime upgrade. Serve over HTTPS (or localhost) with HTTP range support; `npm run dev` supports JAR range requests. The isolation service worker reloads once before mounting the tutorial. The verifier downloads only when you first check an exercise; Stop terminates it. No source code is sent to a verification server.

app.js

@@ -1,4 +1,8 @@
 import { tutorial } from "./tutorial-data.js";
+import { BrowserVerifier, prepareVerifier } from "./verifier/client.mjs";
+
+let preparationError;
+try { await prepareVerifier(); } catch (error) { preparationError = error.message; }
 
 (function () {
   "use strict";
@@ -20,6 +24,8 @@ import { tutorial } from "./tutorial-data.js";
   });
 
   let state = blankState();
+  const verifier = new BrowserVerifier();
+  let checkToken = 0;
 
   const screen = document.querySelector("#screen");
   const navigation = document.querySelector("#step-navigation");
@@ -57,6 +63,8 @@ import { tutorial } from "./tutorial-data.js";
   }
 
   function render() {
+    checkToken++;
+    if (verifier.pending) verifier.cancel();
     renderNavigation();
     const step = steps[state.currentStep];
     document.title = step.id === "welcome" ? content.meta.title : `${step.shortTitle} · ${content.meta.title}`;
@@ -162,7 +170,7 @@ import { tutorial } from "./tutorial-data.js";
               <h2 id="exercise-title-${lesson.id}">${escapeHtml(lesson.exercise.title)}</h2>
               <p>${escapeHtml(lesson.exercise.prompt)}</p>
             </div>
-            <span class="editor-badge">Java</span>
+            <span class="editor-badge">${escapeHtml(lesson.exercise.filename)}</span>
           </div>
           ${
             lesson.exercise.guide
@@ -203,16 +211,15 @@ import { tutorial } from "./tutorial-data.js";
   }
 
   function renderExerciseFeedback(result) {
-    if (!result) return "<p>Run the check when you are ready. This checker looks for the contract, not exact formatting.</p>";
-    if (result.passed) {
-      return '<p><strong>Contract satisfied.</strong> Your annotations express the requested guarantee.</p>';
-    }
-    return `<p><strong>Almost there.</strong></p><ul>${result.messages.map((message) => `<li>${escapeHtml(message)}</li>`).join("")}</ul>`;
+    if (!result) return "<p>Check your Java code and refinements in your browser.</p>";
+    return result.diagnostics.map(({ title, message }) =>
+      `<p><strong>${escapeHtml(title)}</strong><br>${escapeHtml(message)}</p>`).join("");
   }
 
   function wireLesson(lesson) {
     const textarea = document.querySelector(`#code-${lesson.id}`);
     const feedback = document.querySelector(`#exercise-feedback-${lesson.id}`);
+    const checkButton = document.querySelector(`#check-${lesson.id}`);
     const solutionButton = document.querySelector(`#solution-${lesson.id}`);
     const solutionPanel = document.querySelector(`#solution-panel-${lesson.id}`);
 
@@ -250,6 +257,9 @@ import { tutorial } from "./tutorial-data.js";
     const focusEditor = () => (editor ? editor.focus() : textarea.focus());
 
     const handleCodeChange = () => {
+      checkToken++;
+      if (verifier.pending) verifier.cancel();
+      checkButton.textContent = "Check my work";
       state.code[lesson.id] = getCode();
       delete state.checkResults[lesson.id];
       feedback.className = "exercise-feedback";
@@ -259,13 +269,41 @@ import { tutorial } from "./tutorial-data.js";
     if (editor) editor.on("change", handleCodeChange);
     else textarea.addEventListener("input", handleCodeChange);
 
-    document.querySelector(`#check-${lesson.id}`).addEventListener("click", () => {
-      const failures = lesson.exercise.checks.filter((check) => !new RegExp(check.pattern, "m").test(getCode()));
-      const result = { passed: failures.length === 0, messages: failures.map((check) => check.message) };
-      state.checkResults[lesson.id] = result;
-      feedback.className = `exercise-feedback ${result.passed ? "is-success" : "is-error"}`;
-      feedback.innerHTML = renderExerciseFeedback(result);
-      feedback.scrollIntoView({ behavior: "smooth", block: "nearest" });
+    checkButton.addEventListener("click", async () => {
+      if (verifier.pending) {
+        checkToken++;
+        verifier.cancel();
+        checkButton.textContent = "Check my work";
+        feedback.className = "exercise-feedback";
+        feedback.innerHTML = renderExerciseFeedback({ diagnostics: [{ title: "Verification stopped", message: "Check again when you are ready." }] });
+        return;
+      }
+      const token = ++checkToken;
+      const code = getCode();
+      checkButton.textContent = "Stop";
+      feedback.className = "exercise-feedback";
+      try {
+        if (preparationError) throw new Error(preparationError);
+        const result = await verifier.verify({ [lesson.exercise.filename]: code }, message => {
+          if (token === checkToken) feedback.textContent = message;
+        });
+        if (token !== checkToken) return;
+        // exercise hints describe the requested contract, independently of verification
+        if (result.status === "success") {
+          const missing = lesson.exercise.checks.filter(check => !new RegExp(check.pattern, "m").test(code));
+          if (missing.length) result.diagnostics.push({ title: "Exercise incomplete", message: missing.map(check => check.message).join(" ") });
+          result.passed = missing.length === 0;
+        }
+        state.checkResults[lesson.id] = result;
+        feedback.className = `exercise-feedback ${result.passed ? "is-success" : "is-error"}`;
+        feedback.innerHTML = renderExerciseFeedback(result);
+      } catch (error) {
+        if (token !== checkToken || error.name === "AbortError") return;
+        feedback.className = "exercise-feedback is-error";
+        feedback.innerHTML = renderExerciseFeedback({ diagnostics: [{ title: "Verification could not complete", message: error.message }] });
+      } finally {
+        if (token === checkToken) checkButton.textContent = "Check my work";
+      }
     });
 
     document.querySelector(`#reset-${lesson.id}`).addEventListener("click", () => {

scripts/build-site.mjs

@@ -13,6 +13,8 @@ const staticEntries = [
   "styles.css",
   "images",
   "vendor",
+  "verifier",
+  "isolation.js",
 ];
 
 await access(resolve(root, "index.html"));

scripts/dev-server.mjs

@@ -11,6 +11,8 @@ const mimeTypes = {
   ".gif": "image/gif",
   ".html": "text/html; charset=utf-8",
   ".ico": "image/x-icon",
+  ".mjs": "text/javascript; charset=utf-8",
+  ".wasm": "application/wasm",
   ".js": "text/javascript; charset=utf-8",
   ".jpg": "image/jpeg",
   ".jpeg": "image/jpeg",
@@ -56,7 +58,27 @@ const server = createServer(async (request, response) => {
     }
   }
 
+  const range = request.headers.range?.match(/^bytes=(\d+)-(\d*)$/);
+  if (range) {
+    const start = Number(range[1]);
+    const end = Math.min(range[2] ? Number(range[2]) : file.size - 1, file.size - 1);
+    if (start > end || start >= file.size) {
+      response.writeHead(416, { "Content-Range": `bytes */${file.size}` }).end();
+      return;
+    }
+    response.writeHead(206, {
+      "Content-Type": mimeTypes[extname(target).toLowerCase()] || "application/octet-stream",
+      "Content-Range": `bytes ${start}-${end}/${file.size}`,
+      "Content-Length": end - start + 1,
+      "Accept-Ranges": "bytes",
+    });
+    if (request.method === "HEAD") response.end();
+    else createReadStream(target, { start, end }).pipe(response);
+    return;
+  }
   response.writeHead(200, {
+    "Accept-Ranges": "bytes",
+    "Content-Length": file.size,
     "Cache-Control": "no-store",
     "Content-Type": mimeTypes[extname(target).toLowerCase()] || "application/octet-stream",
   });

scripts/validate-content.mjs

@@ -12,6 +12,9 @@ if (!tutorial?.lessons?.length) {
 
 for (const lesson of tutorial?.lessons ?? []) {
   const label = lesson.id || "unnamed lesson";
+  if (!/^[A-Za-z_$][A-Za-z0-9_$]*\.java$/.test(lesson.exercise?.filename || "")) {
+    failures.push(`${label}: exercise needs a Java filename.`);
+  }
 
   for (const check of lesson.exercise?.checks ?? []) {
     if (!new RegExp(check.pattern, "m").test(lesson.exercise.solutionCode)) {

tutorial-data.js

@@ -37,6 +37,7 @@ export const tutorial = {
         ],
       },
       exercise: {
+        filename: "RGB.java",
         title: "Repair the red channel",
         prompt:
           "Add a refinement that limits red to 0–255, then replace the invalid value with any value that satisfies it.",
@@ -112,6 +113,7 @@ public static int divide(
         ],
       },
       exercise: {
+        filename: "Midpoint.java",
         title: "Complete the midpoint contract",
         prompt:
           "Replace both true refinements: low must be no greater than high, and the return value must stay between the two bounds.",
@@ -194,6 +196,7 @@ public class LightBulb {
         ],
       },
       exercise: {
+        filename: "SocketRefinements.java",
         title: "Complete the socket transitions",
         prompt:
           "Replace the true refinements so bind, connect, sendUrgentData, and close follow the socket protocol.",
@@ -323,6 +326,7 @@ public interface ArrayListRefinements<E> {
         ],
       },
       exercise: {
+        filename: "StackRefinements.java",
         title: "Complete the stack refinements",
         prompt:
           "Replace the true refinements so the constructor, push, pop, and peek maintain and check the size ghost variable.",