tlaplus · FedericoPonzi · Feb 28, 2026 · Feb 27, 2026 · Feb 27, 2026
diff --git a/.github/workflows/cd.yml b/.github/workflows/cd.yml
@@ -15,6 +15,12 @@ jobs:
       - name: Checkout code
         uses: actions/checkout@v4
 
+      - name: Checkout Examples repo
+        uses: actions/checkout@v4
+        with:
+          repository: tlaplus/Examples
+          path: Examples
+
       - name: Setup Node.js
         uses: actions/setup-node@v4
         with:

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -6,13 +6,23 @@ on:
   pull_request:
     branches: [main]
 
+permissions:
+  contents: read
+  pull-requests: write
+
 jobs:
   build:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout code
         uses: actions/checkout@v4
 
+      - name: Checkout Examples repo
+        uses: actions/checkout@v4
+        with:
+          repository: tlaplus/Examples
+          path: Examples
+
       - name: Setup Node.js
         uses: actions/setup-node@v4
         with:
@@ -27,3 +37,41 @@ jobs:
 
       - name: Build
         run: npm run build
+
+      - name: Upload build preview
+        if: github.event_name == 'pull_request'
+        uses: actions/upload-artifact@v4
+        with:
+          name: site-preview-pr-${{ github.event.number }}
+          path: out/
+          retention-days: 14
+
+      - name: Comment on PR with preview link
+        if: github.event_name == 'pull_request'
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const marker = '<!-- site-preview-comment -->';
+            const runUrl = `${context.serverUrl}/${context.repo.owner}/${context.repo.repo}/actions/runs/${context.runId}`;
+            const body = `${marker}\n📦 **Site preview built!** Download the artifact to preview locally:\n\n[**Download preview**](${runUrl}#artifacts)\n\nTo view: unzip, \`cd\` into the folder, then serve with a local HTTP server:\n\`\`\`\nnpx serve .\n# or\npython3 -m http.server\n\`\`\``;
+            const { data: comments } = await github.rest.issues.listComments({
+              owner: context.repo.owner,
+              repo: context.repo.repo,
+              issue_number: context.issue.number,
+            });
+            const existing = comments.find(c => c.body.includes(marker));
+            if (existing) {
+              await github.rest.issues.updateComment({
+                owner: context.repo.owner,
+                repo: context.repo.repo,
+                comment_id: existing.id,
+                body,
+              });
+            } else {
+              await github.rest.issues.createComment({
+                owner: context.repo.owner,
+                repo: context.repo.repo,
+                issue_number: context.issue.number,
+                body,
+              });
+            }
diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml
@@ -21,6 +21,12 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v4
 
+      - name: Checkout Examples repo
+        uses: actions/checkout@v4
+        with:
+          repository: tlaplus/Examples
+          path: Examples
+
       - name: Setup Node.js
         uses: actions/setup-node@v4
         with:

diff --git a/.gitignore b/.gitignore
@@ -1,5 +1,6 @@
 node_modules/
 .next/
 out/
+Examples/
 *.tsbuildinfo
 next-env.d.ts
diff --git a/public/tlc-worker.html b/public/tlc-worker.html
@@ -8,6 +8,7 @@
 <body>
 <script>
   let TlcRunnerClass = null;
+  let cheerpjLib = null;
   let initError = null;
   let capturing = false;
 
@@ -36,6 +37,7 @@
       // Resolve jar path relative to this HTML file's location
       const jarPath = `/app${location.pathname.replace(/\/[^/]*$/, '')}/tlaplus-web-cheerpj.jar`;
       const lib = await cheerpjRunLibrary(jarPath);
+      cheerpjLib = lib;
       TlcRunnerClass = await lib.me.fponzi.tlaplusweb.TlcRunner;
       parent.postMessage({ type: "ready" }, "*");
     } catch (e) {
@@ -54,7 +56,18 @@
         return;
       }
       try {
-        const { spec, cfg, workers, checkDeadlock } = event.data;
+        const { spec, cfg, workers, checkDeadlock, extraModules } = event.data;
+        // Write extra .tla modules to /files/ so TLC can resolve EXTENDS
+        if (extraModules && extraModules.length > 0 && cheerpjLib) {
+          const JFile = await cheerpjLib.java.io.File;
+          const JFileWriter = await cheerpjLib.java.io.FileWriter;
+          for (const mod of extraModules) {
+            const f = await new JFile("/files/" + mod.name);
+            const fw = await new JFileWriter(f);
+            await fw.write(mod.content);
+            await fw.close();
+          }
+        }
         capturing = true;
         const result = await TlcRunnerClass.run(spec, cfg, workers, checkDeadlock);
         capturing = false;

diff --git a/src/app/intro/tla-intuition/TlaIntuitionClient.tsx b/src/app/intro/tla-intuition/TlaIntuitionClient.tsx
@@ -252,7 +252,14 @@ export default function TlaIntuitionClient({ description, spec, prev, next }: Pr
 
   return (
     <div className="flex flex-col h-screen">
-      <Navbar current={current} prev={prev} next={next} />
+      <Navbar
+        breadcrumbs={[
+          { label: "How to Write TLA+" },
+          { label: current.title },
+        ]}
+        prev={prev ? { label: prev.title, href: `/intro/${prev.slug}` } : undefined}
+        next={next ? { label: next.title, href: `/intro/${next.slug}` } : undefined}
+      />
 
       <div className="flex flex-1 min-h-0">
         {/* Left: narrative */}

diff --git a/src/app/page.tsx b/src/app/page.tsx
@@ -2,8 +2,11 @@ import Link from "next/link";
 import Footer from "@/components/Footer";
 import { introLessons } from "@/content/intro";
 import { blockingQueueLessons } from "@/content/blocking-queue";
+import { getBeginnerSpecs } from "@/lib/specs";
 
 export default function Home() {
+  const beginnerSpecs = getBeginnerSpecs();
+
   return (
     <div className="min-h-screen flex flex-col">
       {/* Hero */}
@@ -92,6 +95,33 @@ export default function Home() {
             ))}
           </div>
         </section>
+
+        {/* Community Specifications */}
+        <section id="specifications" className="mt-16">
+          <h2 className="text-2xl font-bold text-gray-900 mb-2">
+            Community Specifications
+          </h2>
+          <p className="text-gray-600 mb-6">
+            Beginner-friendly TLA+ specifications from the community. Browse the source,
+            read the explanation, and explore the models.
+          </p>
+          <div className="grid gap-3 sm:grid-cols-2 lg:grid-cols-3">
+            {beginnerSpecs.map((spec) => (
+              <Link
+                key={spec.slug}
+                href={`/specs/${spec.slug}`}
+                className="group rounded-lg border border-gray-200 p-4 hover:border-purple-300 hover:bg-purple-50/50 transition-colors"
+              >
+                <h3 className="font-medium text-gray-900 group-hover:text-purple-700">
+                  {spec.name}
+                </h3>
+                <p className="mt-1 text-xs text-gray-500">
+                  {spec.authors.join(", ")}
+                </p>
+              </Link>
+            ))}
+          </div>
+        </section>
       </main>
 
       <Footer />

diff --git a/src/app/specs/[slug]/SpecPageClient.tsx b/src/app/specs/[slug]/SpecPageClient.tsx
@@ -0,0 +1,77 @@
+"use client";
+
+import Navbar from "@/components/Navbar";
+import MarkdownContent from "@/components/MarkdownContent";
+import SplitLayout from "@/components/SplitLayout";
+import dynamic from "next/dynamic";
+import type { SpecModule } from "@/lib/specs";
+import type { PlaygroundTab, PlaygroundTlcConfig } from "@/components/Playground";
+
+const Playground = dynamic(() => import("@/components/Playground"), { ssr: false });
+
+function buildSpecTabs(modules: SpecModule[]): PlaygroundTab[] {
+  const tabs: PlaygroundTab[] = [];
+  for (const mod of modules) {
+    tabs.push({
+      id: `tla-${mod.filename}`,
+      label: mod.filename,
+      initialContent: mod.content,
+      lang: "tla",
+    });
+    for (const cfg of mod.cfgFiles) {
+      tabs.push({
+        id: `cfg-${cfg.filename}`,
+        label: cfg.filename,
+        initialContent: cfg.content,
+        lang: "cfg",
+      });
+    }
+  }
+  return tabs;
+}
+
+function buildSpecTlcConfigs(modules: SpecModule[]): PlaygroundTlcConfig[] {
+  const configs: PlaygroundTlcConfig[] = [];
+  for (const mod of modules) {
+    for (const cfg of mod.cfgFiles) {
+      const extraModuleTabIds = modules
+        .filter((m) => m.filename !== mod.filename)
+        .map((m) => `tla-${m.filename}`);
+      const isMC = mod.filename.startsWith("MC") || mod.filename.startsWith("MC_");
+      configs.push({
+        label: cfg.filename,
+        specTabId: `tla-${mod.filename}`,
+        cfgTabId: `cfg-${cfg.filename}`,
+        extraModuleTabIds,
+        isDefault: isMC,
+      });
+    }
+  }
+  return configs;
+}
+
+interface SpecPageClientProps {
+  name: string;
+  readme: string;
+  modules: SpecModule[];
+}
+
+export default function SpecPageClient({ name, readme, modules }: SpecPageClientProps) {
+  const tabs = buildSpecTabs(modules);
+  const tlcConfigs = buildSpecTlcConfigs(modules);
+
+  return (
+    <SplitLayout
+      navbar={
+        <Navbar
+          breadcrumbs={[
+            { label: "Specifications", href: "/#specifications" },
+            { label: name },
+          ]}
+        />
+      }
+      left={<MarkdownContent content={readme} />}
+      right={<Playground tabs={tabs} tlcConfigs={tlcConfigs} />}
+    />
+  );
+}
diff --git a/src/app/specs/[slug]/page.tsx b/src/app/specs/[slug]/page.tsx
@@ -0,0 +1,30 @@
+import { getBeginnerSpecs, getSpecBySlug } from "@/lib/specs";
+import { notFound } from "next/navigation";
+import SpecPageClient from "./SpecPageClient";
+
+interface PageProps {
+  params: { slug: string };
+}
+
+export function generateStaticParams() {
+  return getBeginnerSpecs().map((s) => ({ slug: s.slug }));
+}
+
+export function generateMetadata({ params }: PageProps) {
+  const spec = getSpecBySlug(params.slug);
+  if (!spec) return {};
+  return { title: `${spec.name} - TLA+ By Example` };
+}
+
+export default function SpecPage({ params }: PageProps) {
+  const spec = getSpecBySlug(params.slug);
+  if (!spec) notFound();
+
+  return (
+    <SpecPageClient
+      name={spec.name}
+      readme={spec.readme}
+      modules={spec.modules}
+    />
+  );
+}