Phase 4: WebAssembly playground and static gallery

.github/workflows/web.yml

@@ -0,0 +1,52 @@
+name: Web
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+permissions:
+  contents: read
+
+jobs:
+  build:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v4
+      - uses: mymindstorm/setup-emsdk@v14
+        with:
+          version: 3.1.74
+      - name: Build theosc
+        run: |
+          cmake -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DTHEOS_BUILD_TESTS=OFF
+          cmake --build build
+      - name: Build WebAssembly
+        run: |
+          emcmake cmake -B build-wasm -G Ninja -DCMAKE_BUILD_TYPE=Release -DTHEOS_BUILD_TESTS=OFF
+          cmake --build build-wasm
+      - name: WebAssembly smoke test
+        run: node tests/web/wasm_smoke.cjs
+      - name: Assemble site
+        run: web/build-site.sh ./build/theosc site
+      - name: Browser smoke test
+        run: |
+          npm install --no-save playwright@1.49.1
+          npx playwright install --with-deps chromium
+          node tests/web/playground_smoke.cjs site
+      - uses: actions/upload-pages-artifact@v3
+        with:
+          path: site
+
+  deploy:
+    if: github.event_name == 'push' && github.ref == 'refs/heads/main'
+    needs: build
+    runs-on: ubuntu-24.04
+    permissions:
+      pages: write
+      id-token: write
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - id: deployment
+        uses: actions/deploy-pages@v4

.gitignore

@@ -56,3 +56,7 @@ crash-*
 leak-*
 timeout-*
 oom-*
+/web/dist/
+/site/
+/node_modules/
+/package-lock.json

CMakeLists.txt

@@ -36,12 +36,25 @@ add_library(theos_core STATIC
     src/core/logic.cpp
     src/core/parser.cpp
     src/core/proof_checker.cpp
+    src/core/site.cpp
     src/core/truth_table.cpp
     src/core/validator.cpp
 )
 target_include_directories(theos_core PUBLIC include)
 target_link_libraries(theos_core PRIVATE theos_warnings)
 
+if(EMSCRIPTEN)
+    # Browser build: emcmake cmake -B build-wasm -DTHEOS_BUILD_TESTS=OFF && cmake --build build-wasm
+    target_compile_options(theos_core PRIVATE -fwasm-exceptions)
+    add_executable(theos_wasm src/wasm/theos_wasm.cpp)
+    target_compile_options(theos_wasm PRIVATE -fwasm-exceptions)
+    target_link_libraries(theos_wasm PRIVATE theos_core theos_warnings embind)
+    target_link_options(theos_wasm PRIVATE -fwasm-exceptions -sMODULARIZE=1 -sEXPORT_NAME=createTheos
+                        -sENVIRONMENT=web,node -sALLOW_MEMORY_GROWTH=1)
+    set_target_properties(theos_wasm PROPERTIES OUTPUT_NAME theos RUNTIME_OUTPUT_DIRECTORY ${PROJECT_SOURCE_DIR}/web/dist)
+    return()
+endif()
+
 add_executable(theosc src/cli/main.cpp)
 target_link_libraries(theosc PRIVATE theos_core theos_warnings)
 

README.md

@@ -65,6 +65,17 @@ The full language is specified in [docs/spec/language.md](docs/spec/language.md)
 
 ---
 
+## On the web
+
+The `Web` workflow publishes two things to GitHub Pages:
+
+- **Playground**: write an argument in the browser and see the verdict, the graph and every diagnostic as you type. The checker runs locally as WebAssembly.
+- **Gallery**: one page per argument with its graph, sources, Fitch-style proofs, and objections, generated by `theosc site`.
+
+See [web/README.md](web/README.md) to build them locally.
+
+---
+
 ## CLI Usage
 
 ```sh
@@ -73,6 +84,7 @@ theosc export  examples/resurrection.theo --format mermaid -o resurrection.mmd
 theosc build   examples/resurrection.theo -o resurrection.theos
 theosc inspect resurrection.theos            # decoded argument
 theosc inspect resurrection.theos --chunks   # chunk table and hex view
+theosc site    examples -o site/gallery      # static gallery pages
 ```
 
 Diagnostics go to stderr as `file:line:col: error: message` with the source line underneath;
@@ -87,6 +99,8 @@ theos-engine/
 ├── include/theos/   # Public headers
 ├── src/core/        # Core library (lexer, parser, validator, logic checker, exporter, binary format)
 ├── src/cli/         # theosc command-line tool
+├── src/wasm/        # WebAssembly entry point for the playground
+├── web/             # Playground, gallery styles, site assembly
 ├── docs/spec/       # Language, proof rules and binary format specifications
 ├── examples/        # Sample .theo arguments
 ├── fuzz/            # libFuzzer targets and seed corpora

ROADMAP.md

@@ -262,3 +262,4 @@ Answers to the original open questions (2026-10-24) and decisions made while bui
 | 1 Language v2 | done — formulas are fully parsed already (needed to find where they end); the v1 binary format was removed here rather than in M2.2 because it was tied to the old AST; syntax errors stop at the first error, static-rule errors are all reported; Clang CI uses Clang 19, the first Clang that can use `std::expected` from libstdc++ 13 |
 | 2 Binary v2 | done — formulas, proofs and objections are serialized here (M3.4 folded in, since the AST already carries them); padding must be zero so every single-byte corruption is detected (verified by flipping every byte); nesting depth is capped in parser (256) and decoder (512) |
 | 3 Propositional logic | done — the natural-deduction checker already implements the full rule set (quantifiers, identity, S5, definitions, property variables) because the substitution machinery is shared and the Aquinas example needs first-order proofs to pass; formulas are immutable shared trees rather than hash-consed (structural sharing happens in the binary encoder); 39 exercises plus misuse tests; recursive definitions are rejected so expansion terminates |
+| 4 Web | done — Emscripten 3.1.74 build with wasm exceptions (embind `check` returning JSON); playground with live verdict, graph, glosses keyed to lines, shareable `#src=` links; `theosc site` gallery with Fitch-style proof rendering; Node and Playwright smoke tests; Pages deployment needs Pages enabled ("GitHub Actions" source) in repository settings |

include/theos/site.hpp

@@ -0,0 +1,22 @@
+#pragma once
+
+#include "theos/driver.hpp"
+#include <string>
+#include <string_view>
+#include <vector>
+
+// Static HTML gallery of checked arguments
+namespace Theos::Site {
+
+struct Entry {
+    std::string slug;            // file name without extension; the page is <slug>.html
+    Driver::Result result;
+    std::string source;
+};
+
+std::string argument_page(const Entry& entry);
+std::string index_page(const std::vector<Entry>& entries);
+
+std::string base64(std::string_view bytes);
+
+} // namespace Theos::Site

src/cli/main.cpp

@@ -1,6 +1,8 @@
 #include "theos/binary.hpp"
 #include "theos/driver.hpp"
 #include "theos/exporter.hpp"
+#include "theos/site.hpp"
+#include <algorithm>
 #include <cstdio>
 #include <cstring>
 #include <filesystem>
@@ -21,11 +23,13 @@ constexpr const char* usage =
     "  theosc check   <file.theo>\n"
     "  theosc export  <file.theo> --format mermaid [-o <out>]\n"
     "  theosc build   <file.theo> [-o <out.theos>]\n"
-    "  theosc inspect <file.theos> [--chunks]\n";
+    "  theosc inspect <file.theos> [--chunks]\n"
+    "  theosc site    <file-or-dir>... -o <out-dir>\n";
 
 struct Args {
     std::string command;
     std::string input;
+    std::vector<std::string> extra_inputs;   // site accepts several
     std::string format;
     std::string output;
     bool chunks = false;
@@ -41,6 +45,7 @@ std::optional<Args> parse_args(int argc, char* argv[]) {
         else if (arg == "-o" && i + 1 < argc) a.output = argv[++i];
         else if (arg == "--chunks") a.chunks = true;
         else if (a.input.empty() && !arg.starts_with("-")) a.input = arg;
+        else if (a.command == "site" && !arg.starts_with("-")) a.extra_inputs.push_back(arg);
         else return std::nullopt;
     }
     if (a.input.empty()) return std::nullopt;
@@ -117,8 +122,48 @@ int inspect(const Args& args) {
     return 0;
 }
 
+std::string read_text(const std::filesystem::path& p) {
+    const auto bytes = read_bytes(p.string());
+    return std::string(reinterpret_cast<const char*>(bytes.data()), bytes.size());
+}
+
+int site(const Args& args) {
+    namespace fs = std::filesystem;
+    if (args.output.empty()) return EXIT_USAGE;
+    std::vector<fs::path> files;
+    std::vector<std::string> inputs = args.extra_inputs;
+    inputs.insert(inputs.begin(), args.input);
+    for (const auto& in : inputs) {
+        if (fs::is_directory(in)) {
+            for (const auto& e : fs::recursive_directory_iterator(in)) {
+                if (e.path().extension() == ".theo") files.push_back(e.path());
+            }
+        } else {
+            files.emplace_back(in);
+        }
+    }
+    std::ranges::sort(files);
+
+    fs::create_directories(args.output);
+    std::vector<Theos::Site::Entry> entries;
+    int failures = 0;
+    for (const auto& f : files) {
+        Theos::Site::Entry e{f.stem().string(), Theos::Driver::check_file(f.string()), read_text(f)};
+        if (!e.result.ok()) {
+            ++failures;
+            std::cerr << Theos::Driver::render_diagnostics(e.result);
+        }
+        write_text((fs::path(args.output) / (e.slug + ".html")).string(), Theos::Site::argument_page(e));
+        entries.push_back(std::move(e));
+    }
+    write_text((fs::path(args.output) / "index.html").string(), Theos::Site::index_page(entries));
+    std::cerr << "wrote " << entries.size() << " argument pages to " << args.output << "\n";
+    return failures ? EXIT_INVALID : 0;
+}
+
 int run(const Args& args) {
     if (args.command == "inspect") return inspect(args);
+    if (args.command == "site") return site(args);
     if (args.command != "check" && args.command != "export" && args.command != "build") return EXIT_USAGE;
     if (args.command == "export" && args.format != "mermaid") return EXIT_USAGE;
 

src/core/exporter.cpp

@@ -21,6 +21,29 @@ std::string escape(const std::string& text) {
     return out;
 }
 
+// Breaks long labels at spaces so wide nodes do not stretch the whole graph
+std::string wrap(const std::string& text, size_t width) {
+    std::string out;
+    size_t column = 0;
+    size_t start = 0;
+    while (start < text.size()) {
+        size_t end = text.find(' ', start);
+        if (end == std::string::npos) end = text.size();
+        const std::string word = text.substr(start, end - start);
+        if (column > 0 && column + 1 + word.size() > width) {
+            out += "\n";
+            column = 0;
+        } else if (column > 0) {
+            out += ' ';
+            ++column;
+        }
+        out += word;
+        column += word.size();
+        start = end + 1;
+    }
+    return out;
+}
+
 std::string axiom_label(const AST::Axiom& ax) {
     switch (ax.kind) {
         case AST::AxiomKind::Scripture: return ax.scripture.chapter ? Scripture::format(ax.scripture) : ax.citation;
@@ -35,24 +58,25 @@ std::string axiom_label(const AST::Axiom& ax) {
 std::string to_mermaid(const AST::Document& doc) {
     std::ostringstream ss;
     ss << "flowchart TD\n";
-    ss << "    classDef axiom fill:#f3e5f5,stroke:#6a1b9a;\n";
-    ss << "    classDef premise fill:#e1f5fe,stroke:#01579b,stroke-width:2px;\n";
-    ss << "    classDef deduction fill:#fff9c4,stroke:#f9a825,stroke-width:2px;\n";
-    ss << "    classDef conclusion fill:#e8f5e9,stroke:#2e7d32,stroke-width:3px;\n";
-    ss << "    classDef objection fill:#ffebee,stroke:#c62828;\n";
-    ss << "    classDef reply fill:#fff3e0,stroke:#ef6c00;\n";
+    // Manuscript palette: gold leaf for axioms, lapis for claims, rubric red for objections
+    ss << "    classDef axiom fill:#f6efd9,stroke:#a8842a,color:#23212b;\n";
+    ss << "    classDef premise fill:#e7edf7,stroke:#1f4e9c,color:#23212b;\n";
+    ss << "    classDef deduction fill:#f3f4f1,stroke:#5b6b85,color:#23212b;\n";
+    ss << "    classDef conclusion fill:#d6e1f3,stroke:#1f4e9c,stroke-width:3px,color:#23212b;\n";
+    ss << "    classDef objection fill:#f7e3e1,stroke:#b3261e,color:#23212b;\n";
+    ss << "    classDef reply fill:#f3f4f1,stroke:#7a5c2e,color:#23212b;\n";
     ss << "    classDef imported stroke-dasharray:4 3;\n";
 
     for (const auto& ax : doc.axioms) {
-        ss << "    " << ax.id << "([\"" << ax.id << ": " << escape(axiom_label(ax)) << "\"]):::axiom\n";
+        ss << "    " << ax.id << "([\"" << ax.id << ": " << escape(wrap(axiom_label(ax), 40)) << "\"]):::axiom\n";
     }
     for (const auto& n : doc.nodes) {
-        ss << "    " << n.id << "[\"<b>" << n.id << "</b>: " << escape(n.text) << "<br/><i>"
-           << escape(print(*n.formula, Notation::Unicode)) << "</i>\"]:::" << AST::to_string(n.kind) << "\n";
+        ss << "    " << n.id << "[\"<b>" << n.id << "</b>: " << escape(wrap(n.text, 40)) << "<br/><i>"
+           << escape(wrap(print(*n.formula, Notation::Unicode), 48)) << "</i>\"]:::" << AST::to_string(n.kind) << "\n";
         if (n.imported) ss << "    class " << n.id << " imported\n";
     }
     for (const auto& d : doc.dialectics) {
-        ss << "    " << d.id << "{{\"<b>" << d.id << "</b>: " << escape(d.text) << "\"}}:::" << AST::to_string(d.kind) << "\n";
+        ss << "    " << d.id << "{{\"<b>" << d.id << "</b>: " << escape(wrap(d.text, 40)) << "\"}}:::" << AST::to_string(d.kind) << "\n";
     }
 
     for (const auto& n : doc.nodes) {