diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index 5ec61cb..2faf1ac 100644 --- a/.github/workflows/pages.yml +++ b/.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 diff --git a/.gitignore b/.gitignore index 872d5f6..dcbd144 100644 --- a/.gitignore +++ b/.gitignore @@ -141,3 +141,8 @@ dist vite.config.js.timestamp-* vite.config.ts.timestamp-* .vite/ + +# generated shared browser verifier +verifier/ +isolation.js +.browser-source/ diff --git a/README.md b/README.md index 2672259..9f74473 100644 --- a/README.md +++ b/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. diff --git a/app.js b/app.js index 7cc878f..cda8940 100644 --- a/app.js +++ b/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";

${escapeHtml(lesson.exercise.title)}

${escapeHtml(lesson.exercise.prompt)}

- Java + ${escapeHtml(lesson.exercise.filename)} ${ lesson.exercise.guide @@ -203,16 +211,15 @@ import { tutorial } from "./tutorial-data.js"; } function renderExerciseFeedback(result) { - if (!result) return "

Run the check when you are ready. This checker looks for the contract, not exact formatting.

"; - if (result.passed) { - return '

Contract satisfied. Your annotations express the requested guarantee.

'; - } - return `

Almost there.

`; + if (!result) return "

Check your Java code and refinements in your browser.

"; + return result.diagnostics.map(({ title, message }) => + `

${escapeHtml(title)}
${escapeHtml(message)}

`).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", () => { diff --git a/scripts/build-site.mjs b/scripts/build-site.mjs index 88d875b..194a43e 100644 --- a/scripts/build-site.mjs +++ b/scripts/build-site.mjs @@ -13,6 +13,8 @@ const staticEntries = [ "styles.css", "images", "vendor", + "verifier", + "isolation.js", ]; await access(resolve(root, "index.html")); diff --git a/scripts/dev-server.mjs b/scripts/dev-server.mjs index 5ed438d..a186014 100644 --- a/scripts/dev-server.mjs +++ b/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", }); diff --git a/scripts/validate-content.mjs b/scripts/validate-content.mjs index c172165..081b987 100644 --- a/scripts/validate-content.mjs +++ b/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)) { diff --git a/tutorial-data.js b/tutorial-data.js index 018fb38..09da7ac 100644 --- a/tutorial-data.js +++ b/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 { ], }, 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.",