diff --git a/.github/workflows/web.yml b/.github/workflows/web.yml new file mode 100644 index 0000000..51065ee --- /dev/null +++ b/.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 diff --git a/.gitignore b/.gitignore index beca4ac..dff0bc1 100644 --- a/.gitignore +++ b/.gitignore @@ -56,3 +56,7 @@ crash-* leak-* timeout-* oom-* +/web/dist/ +/site/ +/node_modules/ +/package-lock.json diff --git a/CMakeLists.txt b/CMakeLists.txt index d8c2e08..5ad8364 100644 --- a/CMakeLists.txt +++ b/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) diff --git a/README.md b/README.md index fd18217..b9c135d 100644 --- a/README.md +++ b/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 diff --git a/ROADMAP.md b/ROADMAP.md index 6b6b160..a6f4ab3 100644 --- a/ROADMAP.md +++ b/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 | diff --git a/include/theos/site.hpp b/include/theos/site.hpp new file mode 100644 index 0000000..5c15bcf --- /dev/null +++ b/include/theos/site.hpp @@ -0,0 +1,22 @@ +#pragma once + +#include "theos/driver.hpp" +#include +#include +#include + +// Static HTML gallery of checked arguments +namespace Theos::Site { + +struct Entry { + std::string slug; // file name without extension; the page is .html + Driver::Result result; + std::string source; +}; + +std::string argument_page(const Entry& entry); +std::string index_page(const std::vector& entries); + +std::string base64(std::string_view bytes); + +} // namespace Theos::Site diff --git a/src/cli/main.cpp b/src/cli/main.cpp index 8d151fc..4e11c5a 100644 --- a/src/cli/main.cpp +++ b/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 #include #include #include @@ -21,11 +23,13 @@ constexpr const char* usage = " theosc check \n" " theosc export --format mermaid [-o ]\n" " theosc build [-o ]\n" - " theosc inspect [--chunks]\n"; + " theosc inspect [--chunks]\n" + " theosc site ... -o \n"; struct Args { std::string command; std::string input; + std::vector extra_inputs; // site accepts several std::string format; std::string output; bool chunks = false; @@ -41,6 +45,7 @@ std::optional 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(bytes.data()), bytes.size()); +} + +int site(const Args& args) { + namespace fs = std::filesystem; + if (args.output.empty()) return EXIT_USAGE; + std::vector files; + std::vector 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 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; diff --git a/src/core/exporter.cpp b/src/core/exporter.cpp index 0ad0625..271678d 100644 --- a/src/core/exporter.cpp +++ b/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 << "[\"" << n.id << ": " << escape(n.text) << "
" - << escape(print(*n.formula, Notation::Unicode)) << "\"]:::" << AST::to_string(n.kind) << "\n"; + ss << " " << n.id << "[\"" << n.id << ": " << escape(wrap(n.text, 40)) << "
" + << escape(wrap(print(*n.formula, Notation::Unicode), 48)) << "\"]:::" << AST::to_string(n.kind) << "\n"; if (n.imported) ss << " class " << n.id << " imported\n"; } for (const auto& d : doc.dialectics) { - ss << " " << d.id << "{{\"" << d.id << ": " << escape(d.text) << "\"}}:::" << AST::to_string(d.kind) << "\n"; + ss << " " << d.id << "{{\"" << d.id << ": " << escape(wrap(d.text, 40)) << "\"}}:::" << AST::to_string(d.kind) << "\n"; } for (const auto& n : doc.nodes) { diff --git a/src/core/site.cpp b/src/core/site.cpp new file mode 100644 index 0000000..27a0c0d --- /dev/null +++ b/src/core/site.cpp @@ -0,0 +1,192 @@ +#include "theos/site.hpp" +#include "theos/canon.hpp" +#include "theos/exporter.hpp" + +namespace Theos::Site { + +namespace { + +std::string html(std::string_view s) { + std::string out; + for (char c : s) { + switch (c) { + case '&': out += "&"; break; + case '<': out += "<"; break; + case '>': out += ">"; break; + case '"': out += """; break; + default: out += c; + } + } + return out; +} + +std::string head(const std::string& title) { + return "\n\n\n\n" + "\n" + "" + html(title) + "\n" + "\n" + "\n\n\n\n"; +} + +std::string title_of(const Entry& e) { + if (e.result.doc && e.result.doc->title) return *e.result.doc->title; + return e.slug; +} + +std::string refs(const std::vector& list) { + std::string out; + for (size_t i = 0; i < list.size(); ++i) out += (i ? ", " : "") + html(list[i].name); + return out; +} + +std::string axiom_text(const AST::Axiom& ax) { + switch (ax.kind) { + case AST::AxiomKind::Scripture: + return html(ax.scripture.chapter ? Scripture::format(ax.scripture) : ax.citation) + " (" + html(ax.canon) + " canon)"; + case AST::AxiomKind::Source: return "" + html(ax.citation) + ", " + html(ax.locator); + case AST::AxiomKind::Principle: return html(ax.citation); + } + return ""; +} + +// Flat Fitch layout: a number column, then one bar per enclosing subproof, then the formula +void proof_items(const std::vector& items, std::vector& open, std::string& out) { + for (size_t i = 0; i < items.size(); ++i) { + if (const auto* line = std::get_if(&items[i])) { + std::string just = html(line->rule.name); + for (size_t k = 0; k < line->refs.size(); ++k) { + const auto& r = line->refs[k]; + just += k ? ", " : " "; + if (r.kind == AST::ProofRef::Kind::Name) just += html(r.name); + else if (r.kind == AST::ProofRef::Kind::Line) just += std::to_string(r.first); + else just += std::to_string(r.first) + "–" + std::to_string(r.last); + } + std::string bars; + for (const auto* sub : open) bars += std::string("strict ? " strict" : "") + "\">"; + const bool opens = i == 0 && !open.empty(); + std::string tag; + if (opens && open.back()->strict) tag = "□"; + if (opens && open.back()->fresh) tag = "" + html(open.back()->fresh->name) + ""; + const bool assumption = line->rule.name == "assume"; + out += "
" + std::to_string(line->number) + "" + bars + tag + + "" + html(print(*line->formula, Notation::Unicode)) + + "" + just + "
\n"; + } else { + const auto& sub = std::get(items[i]); + open.push_back(&sub); + proof_items(sub.items, open, out); + open.pop_back(); + } + } +} + +} // namespace + +std::string base64(std::string_view bytes) { + static constexpr char table[] = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"; + std::string out; + size_t i = 0; + for (; i + 2 < bytes.size(); i += 3) { + const uint32_t n = (uint8_t(bytes[i]) << 16) | (uint8_t(bytes[i + 1]) << 8) | uint8_t(bytes[i + 2]); + for (int k = 18; k >= 0; k -= 6) out += table[(n >> k) & 63]; + } + if (i < bytes.size()) { + uint32_t n = uint8_t(bytes[i]) << 16; + if (i + 1 < bytes.size()) n |= uint8_t(bytes[i + 1]) << 8; + out += table[(n >> 18) & 63]; + out += table[(n >> 12) & 63]; + out += i + 1 < bytes.size() ? table[(n >> 6) & 63] : '='; + out += '='; + } + return out; +} + +std::string argument_page(const Entry& e) { + const auto& r = e.result; + std::string out = head(title_of(e) + " — Theos"); + out += "
\n\n"; + out += "

" + html(title_of(e)) + "

\n"; + if (r.doc && !r.doc->author.empty()) out += "

" + html(r.doc->author) + "

\n"; + out += r.ok() ? "

The argument holds.

\n

Every inference was checked by machine.

\n" + : "

The argument does not hold.

\n"; + out += "

Open in the playground

\n"; + + if (!r.ok()) out += "
" + html(Driver::render_diagnostics(r)) + "
\n"; + if (!r.doc) return out + "
\n\n\n"; + const auto& doc = *r.doc; + + out += "
\n" + html(Exporter::to_mermaid(doc)) + "
\n"; + + if (!doc.axioms.empty()) { + out += "

Sources

\n
\n"; + for (const auto& ax : doc.axioms) out += "
" + html(ax.id) + "
" + axiom_text(ax) + "
\n"; + out += "
\n"; + } + if (!doc.definitions.empty()) { + out += "

Definitions

\n
\n"; + for (const auto& d : doc.definitions) { + std::string params; + for (size_t i = 0; i < d.params.size(); ++i) params += (i ? ", " : "") + d.params[i].name; + out += "
" + html(d.id) + (params.empty() ? "" : "(" + html(params) + ")") + "
" + + html(print(*d.body, Notation::Unicode)) + "
\n"; + } + out += "
\n"; + } + + out += "

The argument

\n"; + for (const auto& n : doc.nodes) { + const std::string kind(AST::to_string(n.kind)); + out += "
\n

" + html(n.id) + " " + kind + "

\n"; + out += "

" + html(n.text) + "

\n

" + html(print(*n.formula, Notation::Unicode)) + "

\n"; + if (!n.grounded_by.empty()) out += "

Grounded by " + refs(n.grounded_by) + "

\n"; + if (!n.from.empty()) { + out += "

From " + refs(n.from); + if (n.rule) out += " by " + html(n.rule->name) + ""; + else if (!n.proof) out += ", decided by truth table"; + out += "

\n"; + } + if (n.proof) { + out += "
Proof\n"; + std::vector open; + proof_items(n.proof->items, open, out); + out += "
\n"; + } + out += "
\n"; + } + + if (!doc.dialectics.empty()) { + out += "

Objections and replies

\n"; + for (const auto& d : doc.dialectics) { + const bool objection = d.kind == AST::DialecticKind::Objection; + out += std::string("
\n

" + + html(d.id) + " " + (objection ? "objection to " : "reply to ") + html(d.target.name) + "

\n

" + html(d.text) + "

\n"; + if (d.formula) out += "

" + html(print(*d.formula, Notation::Unicode)) + "

\n"; + out += "
\n"; + } + } + + out += "\n\n" + "\n\n\n"; + return out; +} + +std::string index_page(const std::vector& entries) { + std::string out = head("Theos Gallery"); + out += "
\n\n

Arguments

\n" + "

Classical arguments, formalized and checked by machine. Each page shows the graph, the sources, every proof, and the objections.

\n
    \n"; + for (const auto& e : entries) { + out += "
  • " + html(title_of(e)) + ""; + if (e.result.doc && !e.result.doc->author.empty()) out += " " + html(e.result.doc->author) + ""; + out += e.result.ok() ? " holds" : " does not hold"; + if (e.result.doc) { + for (const auto& n : e.result.doc->nodes) { + if (n.kind == AST::NodeKind::Conclusion && !n.imported) out += "

    " + html(n.text) + "

    "; + } + } + out += "
    • \n"; + } + return out + "
\n
\n\n\n"; +} + +} // namespace Theos::Site diff --git a/src/wasm/theos_wasm.cpp b/src/wasm/theos_wasm.cpp new file mode 100644 index 0000000..6b039c8 --- /dev/null +++ b/src/wasm/theos_wasm.cpp @@ -0,0 +1,70 @@ +// WebAssembly entry point for the playground: check(source) returns a JSON report +#include "theos/driver.hpp" +#include "theos/exporter.hpp" +#include +#include + +namespace { + +std::string json_string(std::string_view s) { + std::string out = "\""; + for (char c : s) { + switch (c) { + case '"': out += "\\\""; break; + case '\\': out += "\\\\"; break; + case '\n': out += "\\n"; break; + case '\r': out += "\\r"; break; + case '\t': out += "\\t"; break; + default: + if (static_cast(c) < 0x20) { + char buf[8]; + std::snprintf(buf, sizeof buf, "\\u%04x", c); + out += buf; + } else { + out += c; + } + } + } + return out + "\""; +} + +// Nodes whose source range contains an error, so the graph can mark them +bool has_error_inside(const Theos::Driver::Result& r, const Theos::Span& span) { + for (const auto& d : r.diagnostics) { + if (d.severity == Theos::Severity::Error && d.span.offset >= span.offset && d.span.offset < span.offset + span.length) return true; + } + return false; +} + +std::string check(const std::string& source) { + auto r = Theos::Driver::check_source(source, "playground.theo"); + std::string out = "{\"ok\":" + std::string(r.ok() ? "true" : "false") + ",\"diagnostics\":["; + for (size_t i = 0; i < r.diagnostics.size(); ++i) { + const auto& d = r.diagnostics[i]; + out += (i ? "," : "") + std::string("{\"severity\":") + (d.severity == Theos::Severity::Error ? "\"error\"" : "\"warning\"") + + ",\"line\":" + std::to_string(d.span.line) + ",\"col\":" + std::to_string(d.span.col) + + ",\"message\":" + json_string(d.message) + "}"; + } + out += "],\"rendered\":" + json_string(Theos::Driver::render_diagnostics(r)); + if (r.doc) { + std::string mermaid = Theos::Exporter::to_mermaid(*r.doc); + mermaid += " classDef invalid stroke:#d50000,stroke-width:4px;\n"; + out += ",\"nodes\":["; + for (size_t i = 0; i < r.doc->nodes.size(); ++i) { + const auto& n = r.doc->nodes[i]; + const bool bad = has_error_inside(r, n.span); + if (bad) mermaid += " class " + n.id + " invalid\n"; + out += (i ? "," : "") + std::string("{\"id\":") + json_string(n.id) + ",\"kind\":" + json_string(Theos::AST::to_string(n.kind)) + + ",\"text\":" + json_string(n.text) + ",\"formula\":" + json_string(Theos::print(*n.formula, Theos::Notation::Unicode)) + + ",\"error\":" + (bad ? "true" : "false") + "}"; + } + out += "],\"mermaid\":" + json_string(mermaid); + } + return out + "}"; +} + +} // namespace + +EMSCRIPTEN_BINDINGS(theos) { + emscripten::function("check", &check); +} diff --git a/tests/test_exporter.cpp b/tests/test_exporter.cpp index f94677b..de88da8 100644 --- a/tests/test_exporter.cpp +++ b/tests/test_exporter.cpp @@ -22,3 +22,30 @@ objection O1 against P1 { text: "no" } REQUIRE(out.find("P1 --> C1") != std::string::npos); REQUIRE(out.find("O1 -. objects .-> P1") != std::string::npos); } + +#include "theos/site.hpp" + +TEST_CASE("Base64 matches RFC 4648 vectors", "[site]") { + REQUIRE(Site::base64("") == ""); + REQUIRE(Site::base64("f") == "Zg=="); + REQUIRE(Site::base64("fo") == "Zm8="); + REQUIRE(Site::base64("foo") == "Zm9v"); + REQUIRE(Site::base64("foobar") == "Zm9vYmFy"); +} + +TEST_CASE("Gallery pages show verdict, proofs and escaped text", "[site]") { + const std::string src = R"(argument "A " by "Me" +premise P1 { text: "x & y" formula: A } +conclusion C1 from [P1] { text: "c" formula: A proof { 1. A premise P1 } } +)"; + Site::Entry e{"demo", Driver::check_source(src, "demo.theo"), src}; + REQUIRE(e.result.ok()); + const auto page = Site::argument_page(e); + REQUIRE(page.find("

A <b>

") != std::string::npos); + REQUIRE(page.find("The argument holds.") != std::string::npos); + REQUIRE(page.find("x & y") != std::string::npos); + REQUIRE(page.find("premise P1") != std::string::npos); + REQUIRE(page.find("#src=" + Site::base64(src)) != std::string::npos); + const auto index = Site::index_page({e}); + REQUIRE(index.find("href=\"demo.html\"") != std::string::npos); +} diff --git a/tests/web/playground_smoke.cjs b/tests/web/playground_smoke.cjs new file mode 100644 index 0000000..3fc0e7c --- /dev/null +++ b/tests/web/playground_smoke.cjs @@ -0,0 +1,60 @@ +// Browser smoke test for the assembled site. +// Usage: node tests/web/playground_smoke.cjs (needs network for the CDN scripts) +const assert = require('node:assert/strict'); +const http = require('node:http'); +const fs = require('node:fs'); +const path = require('node:path'); +const { chromium } = require('playwright'); + +const root = path.resolve(process.argv[2] ?? 'site'); +const types = { '.html': 'text/html', '.js': 'text/javascript', '.css': 'text/css', '.wasm': 'application/wasm', '.theo': 'text/plain' }; + +const server = http.createServer((req, res) => { + const url = decodeURIComponent(req.url.split('?')[0]); + let file = path.join(root, url.endsWith('/') ? url + 'index.html' : url); + if (!file.startsWith(root) || !fs.existsSync(file)) { res.writeHead(404); res.end(); return; } + res.writeHead(200, { 'content-type': types[path.extname(file)] ?? 'application/octet-stream' }); + fs.createReadStream(file).pipe(res); +}); + +const INVALID = `premise P1 { text: "If A then B" formula: A -> B } +premise P2 { text: "B" formula: B } +conclusion C from [P1, P2] { text: "A" formula: A } +`; + +(async () => { + await new Promise(resolve => server.listen(0, resolve)); + const base = `http://localhost:${server.address().port}`; + const proxy = process.env.HTTPS_PROXY ? { server: process.env.HTTPS_PROXY, bypass: 'localhost,127.0.0.1' } : undefined; + const browser = await chromium.launch({ proxy }); + try { + const page = await browser.newPage(); + const errors = []; + page.on('pageerror', e => errors.push(e.message)); + + await page.goto(`${base}/index.html`); + await page.waitForSelector('#graph svg', { timeout: 30000 }); + assert.equal(await page.textContent('#verdict'), 'The argument holds.'); + + // Affirming the consequent: the checker must reject it with a counterexample + await page.evaluate(src => document.querySelector('.CodeMirror').CodeMirror.setValue(src), INVALID); + await page.waitForFunction(() => document.querySelector('#verdict').textContent.includes('does not hold'), null, { timeout: 10000 }); + const note = await page.textContent('#notes li.error'); + assert.match(note, /counterexample A = false, B = true/); + + // Fixing the conclusion makes it hold again + await page.evaluate(src => document.querySelector('.CodeMirror').CodeMirror.setValue(src), INVALID.replace('formula: A }\n', 'formula: B }\n').replace('premise P2 { text: "B" formula: B }', 'premise P2 { text: "A" formula: A }')); + await page.waitForFunction(() => document.querySelector('#verdict').textContent === 'The argument holds.', null, { timeout: 10000 }); + + await page.goto(`${base}/gallery/index.html`); + assert.ok((await page.locator('.entries li').count()) >= 2); + await page.click('text=The First Way'); + await page.waitForSelector('.mermaid svg', { timeout: 30000 }); + + assert.deepEqual(errors, []); + console.log('playground smoke test passed'); + } finally { + await browser.close(); + server.close(); + } +})().catch(err => { console.error(err); process.exit(1); }); diff --git a/tests/web/wasm_smoke.cjs b/tests/web/wasm_smoke.cjs new file mode 100644 index 0000000..14c8cef --- /dev/null +++ b/tests/web/wasm_smoke.cjs @@ -0,0 +1,29 @@ +// Loads the WebAssembly build and checks one valid and one invalid argument. +// Usage: node tests/web/wasm_smoke.cjs (after building web/dist with Emscripten) +const assert = require('node:assert/strict'); +const fs = require('node:fs'); +const path = require('node:path'); +const createTheos = require(path.join(__dirname, '../../web/dist/theos.js')); + +(async () => { + const theos = await createTheos(); + + const good = JSON.parse(theos.check(fs.readFileSync(path.join(__dirname, '../../examples/aquinas_first_way.theo'), 'utf8'))); + assert.equal(good.ok, true, good.rendered); + assert.ok(good.mermaid.startsWith('flowchart TD')); + assert.equal(good.nodes.length, 7); + + const bad = JSON.parse(theos.check('premise P1 { text: "a" formula: A -> B }\npremise P2 { text: "b" formula: B }\n' + + 'conclusion C from [P1, P2] { text: "c" formula: A }\n')); + assert.equal(bad.ok, false); + assert.match(bad.rendered, /counterexample A = false, B = true/); + assert.equal(bad.nodes.find(n => n.id === 'C').error, true); + assert.match(bad.mermaid, /class C invalid/); + + const syntax = JSON.parse(theos.check('premise {')); + assert.equal(syntax.ok, false); + assert.equal(syntax.diagnostics[0].line, 1); + assert.equal(syntax.mermaid, undefined); + + console.log('wasm smoke test passed'); +})(); diff --git a/web/README.md b/web/README.md new file mode 100644 index 0000000..10b2890 --- /dev/null +++ b/web/README.md @@ -0,0 +1,18 @@ +# Theos on the web + +- `index.html`, `app.js`, `playground.css` — the playground: edit an argument, see the verdict, graph and diagnostics live. The checker runs in the browser as WebAssembly (`src/wasm/theos_wasm.cpp`). +- `gallery.css` — styles for the gallery pages generated by `theosc site`. +- `theos.css` — shared palette and type. +- `build-site.sh` — assembles the deployable site (playground at the root, gallery under `gallery/`). + +Build locally (Emscripten 3.1.74): + +```sh +emcmake cmake -B build-wasm -G Ninja -DCMAKE_BUILD_TYPE=Release -DTHEOS_BUILD_TESTS=OFF +cmake --build build-wasm # writes web/dist/theos.{js,wasm} +web/build-site.sh ./build/theosc site # needs a native theosc build +python3 -m http.server -d site +``` + +The `Web` workflow builds and tests all of this and deploys `site/` to GitHub Pages on pushes to `main` +(GitHub Pages must be enabled with "GitHub Actions" as the source in the repository settings). diff --git a/web/app.js b/web/app.js new file mode 100644 index 0000000..e6a0b0e --- /dev/null +++ b/web/app.js @@ -0,0 +1,170 @@ +// Theos playground: live checking in the browser through the WebAssembly build. +'use strict'; + +const EXAMPLES = [ + ['The First Way (Aquinas)', 'examples/aquinas_first_way.theo'], + ['Resurrection (minimal facts)', 'examples/resurrection.theo'], +]; + +const STARTER = `argument "Modus Ponens" + +axiom Obs = source("Field notes", "p. 4") + +premise P1 grounded_by [Obs] { + text: "If it rains, the street is wet." + formula: Rain -> Wet +} + +premise P2 grounded_by [Obs] { + text: "It rains." + formula: Rain +} + +conclusion C1 from [P1, P2] by imp_e { + text: "The street is wet." + formula: Wet +} +`; + +CodeMirror.defineSimpleMode('theo', { + start: [ + { regex: /\/\/.*/, token: 'comment' }, + { regex: /\/\*/, token: 'comment', next: 'comment' }, + { regex: /"(?:[^\\"]|\\.)*"/, token: 'string' }, + { regex: /\b(?:argument|by|import|axiom|scripture|source|principle|define|premise|deduction|conclusion|from|grounded_by|text|formula|proof|box|objection|reply|against|to|forall|exists|lambda|bot|ind|prop)\b/, token: 'keyword' }, + { regex: /<->|->|<>|\[\]|:=|!=|[~&|∧∨¬→↔□◇∀∃λ⊥≠\\]/, token: 'operator' }, + { regex: /\b\d+\b/, token: 'number' }, + ], + comment: [ + { regex: /.*?\*\//, token: 'comment', next: 'start' }, + { regex: /.*/, token: 'comment' }, + ], +}); + +const editor = CodeMirror.fromTextArea(document.getElementById('source'), { + mode: 'theo', + lineNumbers: true, + indentUnit: 4, + viewportMargin: Infinity, +}); + +const verdict = document.getElementById('verdict'); +const detail = document.getElementById('verdict-detail'); +const graph = document.getElementById('graph'); +const notes = document.getElementById('notes'); +const picker = document.getElementById('examples'); + +mermaid.initialize({ startOnLoad: false, securityLevel: 'strict', theme: 'base', flowchart: { useMaxWidth: false }, + themeVariables: { fontFamily: 'Alegreya Sans, sans-serif', lineColor: '#565463' } }); + +let theos = null; +let marked = []; +let renderCount = 0; + +function encodeSource(text) { + return btoa(String.fromCharCode(...new TextEncoder().encode(text))); +} + +function decodeSource(b64) { + return new TextDecoder().decode(Uint8Array.from(atob(b64), c => c.charCodeAt(0))); +} + +function plural(n, word) { + return `${n} ${word}${n === 1 ? '' : 's'}`; +} + +function showVerdict(report) { + const errors = report.diagnostics.filter(d => d.severity === 'error'); + const warnings = report.diagnostics.length - errors.length; + verdict.classList.toggle('fails', !report.ok); + if (report.ok) { + verdict.textContent = 'The argument holds.'; + detail.textContent = warnings + ? `Every inference is valid. ${plural(warnings, 'warning')} below.` + : 'Every inference is valid.'; + } else if (!report.mermaid) { + verdict.textContent = 'The text could not be read.'; + detail.textContent = errors[0].message; + } else { + verdict.textContent = 'The argument does not hold yet.'; + detail.textContent = `${plural(errors.length, 'problem')}${warnings ? `, ${plural(warnings, 'warning')}` : ''}. Select a note to jump to its line.`; + } +} + +function showNotes(report) { + marked.forEach(line => editor.removeLineClass(line, 'background')); + marked = []; + notes.replaceChildren(...report.diagnostics.map(d => { + const li = document.createElement('li'); + li.className = d.severity; + li.tabIndex = 0; + const where = document.createElement('span'); + where.className = 'where'; + where.textContent = d.line ? `line ${d.line}` : 'file'; + const message = document.createElement('span'); + message.textContent = d.message; + li.append(where, message); + const jump = () => { + if (!d.line) return; + editor.focus(); + editor.setCursor({ line: d.line - 1, ch: Math.max(d.col - 1, 0) }); + }; + li.addEventListener('click', jump); + li.addEventListener('keydown', e => { if (e.key === 'Enter') jump(); }); + if (d.line) { + const handle = editor.addLineClass(d.line - 1, 'background', d.severity === 'error' ? 'line-error' : 'line-warning'); + marked.push(handle); + } + return li; + })); +} + +async function showGraph(report) { + if (!report.mermaid) { + graph.replaceChildren(); + return; + } + const id = `graph-${++renderCount}`; + try { + const { svg } = await mermaid.render(id, report.mermaid); + if (id === `graph-${renderCount}`) graph.innerHTML = svg; + } catch (err) { + graph.textContent = `The graph could not be drawn: ${err.message ?? err}`; + } +} + +function check() { + if (!theos) return; + const source = editor.getValue(); + const report = JSON.parse(theos.check(source)); + showVerdict(report); + showNotes(report); + showGraph(report); + history.replaceState(null, '', `#src=${encodeSource(source)}`); +} + +let timer = null; +editor.on('change', () => { + clearTimeout(timer); + timer = setTimeout(check, 250); +}); + +async function loadExample(path) { + const response = await fetch(path); + if (!response.ok) throw new Error(`${path}: ${response.status}`); + editor.setValue(await response.text()); +} + +picker.append(new Option('Modus ponens', ''), ...EXAMPLES.map(([name, path]) => new Option(name, path))); +picker.addEventListener('change', () => { + if (picker.value) loadExample(picker.value).catch(err => { detail.textContent = `Could not load the example: ${err.message}`; }); + else editor.setValue(STARTER); +}); + +const shared = location.hash.startsWith('#src=') ? location.hash.slice(5) : null; +editor.setValue(shared ? decodeSource(shared) : STARTER); + +createTheos().then(module => { + theos = module; + check(); +}); diff --git a/web/build-site.sh b/web/build-site.sh new file mode 100755 index 0000000..6eb1833 --- /dev/null +++ b/web/build-site.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env sh +# Assembles the static site: playground at the root, gallery under gallery/. +# Usage: web/build-site.sh (web/dist must already hold the WebAssembly build) +set -eu +THEOSC="$1" +OUT="$2" +ROOT="$(cd "$(dirname "$0")/.." && pwd)" + +rm -rf "$OUT" +mkdir -p "$OUT/gallery" "$OUT/examples" +cp "$ROOT/web/index.html" "$ROOT/web/app.js" "$ROOT/web/theos.css" "$ROOT/web/playground.css" "$OUT/" +cp -r "$ROOT/web/dist" "$OUT/dist" +cp "$ROOT"/examples/*.theo "$OUT/examples/" +cp "$ROOT/web/theos.css" "$ROOT/web/gallery.css" "$OUT/gallery/" +"$THEOSC" site "$ROOT/examples" -o "$OUT/gallery" diff --git a/web/gallery.css b/web/gallery.css new file mode 100644 index 0000000..a429501 --- /dev/null +++ b/web/gallery.css @@ -0,0 +1,53 @@ +main.argument, main.gallery { max-width: 68rem; margin: 0 auto; padding: 1.5rem 1.5rem 4rem; } +main.argument nav, main.gallery nav { margin-bottom: 1.5rem; } +main h1 { font-family: var(--font-display); font-weight: 400; font-size: clamp(2.2rem, 5vw, 3.4rem); line-height: 1.05; margin: 0; } +main h2 { font-family: var(--font-display); font-weight: 400; font-size: 1.6rem; margin: 2.5rem 0 0.75rem; } +.author { color: var(--ink-soft); margin: 0.25rem 0 1.25rem; } +main.argument .verdict { margin-top: 1rem; } +.lede { max-width: 60ch; color: var(--ink-soft); } + +.entries { list-style: none; padding: 0; margin: 2rem 0 0; } +.entries li { padding: 1rem 0; border-top: 1px solid var(--rule); } +.entries a { font-family: var(--font-display); font-size: 1.5rem; text-decoration: none; } +.entries a:hover { text-decoration: underline; } +.entries p { margin: 0.25rem 0 0; max-width: 65ch; } +.status { font-size: 0.9rem; margin-left: 0.5rem; } +.status.holds { color: var(--lapis); } +.status.fails { color: var(--rubric); } + +.axioms, .definitions { display: grid; grid-template-columns: max-content 1fr; gap: 0.35rem 1.25rem; } +.axioms dt { color: var(--gold); font-weight: 700; } +.axioms dd, .definitions dd { margin: 0; } +.canon { color: var(--ink-soft); } + +.claim { max-width: 72ch; padding: 0.9rem 0 0.9rem 1.1rem; border-left: 3px solid var(--rule); margin: 0 0 0.75rem; } +.claim.premise { border-left-color: var(--lapis); } +.claim.conclusion { border-left-color: var(--lapis); border-left-width: 6px; } +.claim.objection { border-left-color: var(--rubric); } +.claim.reply { border-left-color: var(--gold); } +.claim h3 { margin: 0; font-weight: 500; color: var(--ink-soft); font-size: 1rem; } +.claim .id { font-family: var(--font-display); font-size: 1.35rem; color: var(--ink); margin-right: 0.35rem; } +.claim p { margin: 0.3rem 0; } +.basis { color: var(--ink-soft); font-size: 0.95rem; } + +/* Fitch proofs: one vertical bar per open subproof (double for strict), assumptions underlined */ +.proof { margin-top: 0.5rem; } +.proof summary { cursor: pointer; color: var(--lapis); } +.pl { display: grid; grid-template-columns: 2.5rem 1fr auto; gap: 0 0.75rem; } +.pl .n { color: var(--ink-soft); text-align: right; padding: 0.15rem 0; } +.pl .body { display: flex; align-items: stretch; min-width: 0; } +.pl .bar { flex: none; width: 1rem; border-left: 2px solid var(--lapis); } +.pl .bar.strict { border-left: 4px double var(--lapis); } +.pl .tag { color: var(--lapis); font-family: var(--font-code); font-size: 0.8rem; margin-right: 0.4rem; padding-top: 0.2rem; } +.pl .formula { padding: 0.15rem 0; } +.pl .formula.assumption { border-bottom: 1px solid var(--lapis); align-self: flex-start; } +.pl .j { color: var(--ink-soft); font-size: 0.9rem; padding: 0.15rem 0; white-space: nowrap; } + +.diagnostics { background: var(--surface); border-left: 3px solid var(--rubric); padding: 1rem; overflow-x: auto; font-family: var(--font-code); font-size: 0.85rem; } +.graph { background: #f3f4f1; padding: 1rem; overflow-x: auto; } + +@media (max-width: 640px) { + .pl { grid-template-columns: 2rem 1fr; } + .pl .j { grid-column: 2; } + .axioms, .definitions { grid-template-columns: 1fr; } +} diff --git a/web/index.html b/web/index.html new file mode 100644 index 0000000..4b6ac1d --- /dev/null +++ b/web/index.html @@ -0,0 +1,44 @@ + + + + + +Theos Playground + + + + + + + + +
+

Theos

+

Write an argument. See whether it holds.

+ + Gallery +
+ +
+
+ +
+ +
+

Loading the checker…

+

+
+
    +
    +
    + + + + + + + + diff --git a/web/playground.css b/web/playground.css new file mode 100644 index 0000000..f7c886b --- /dev/null +++ b/web/playground.css @@ -0,0 +1,73 @@ +.bar { + display: flex; + align-items: baseline; + gap: 1.25rem; + flex-wrap: wrap; + padding: 0.9rem 1.5rem; + border-bottom: 1px solid var(--rule); +} +.wordmark { + font-family: var(--font-display); + font-weight: 400; + font-size: 2rem; + margin: 0; + line-height: 1; +} +.tagline { margin: 0; color: var(--ink-soft); flex: 1; min-width: 12rem; } +.picker { display: flex; gap: 0.5rem; align-items: baseline; color: var(--ink-soft); } +.picker select { + font: inherit; + color: var(--ink); + background: var(--surface); + border: 1px solid var(--rule); + border-radius: 4px; + padding: 0.2rem 0.4rem; +} +.nav { font-weight: 500; } + +.workspace { + display: grid; + grid-template-columns: minmax(0, 1fr) minmax(0, 1fr); + height: calc(100vh - 4.2rem); +} +.source { border-right: 1px solid var(--rule); min-height: 0; } +.source .CodeMirror { + height: 100%; + font-family: var(--font-code); + font-size: 14px; + background: var(--surface); + color: var(--ink); +} +.CodeMirror-gutters { background: var(--vellum); border-right: 1px solid var(--rule); } +.CodeMirror-linenumber { color: var(--ink-soft); } +.CodeMirror-cursor { border-left-color: var(--ink); } +.cm-s-default .cm-keyword { color: var(--lapis); font-weight: 600; } +.cm-s-default .cm-string { color: #5f7a2e; } +.cm-s-default .cm-comment { color: var(--ink-soft); font-style: italic; } +.cm-s-default .cm-operator { color: var(--gold); } +.cm-s-default .cm-number { color: var(--ink-soft); } +.line-error { background: rgba(179, 38, 30, 0.10); } +.line-warning { background: rgba(168, 132, 42, 0.12); } + +.result { overflow: auto; padding: 1.75rem 2rem 3rem; } +.graph { margin: 1.5rem 0; overflow-x: auto; } + +/* Diagnostics read as glosses in the margin, keyed to their line */ +.notes { list-style: none; margin: 0; padding: 0; max-width: 72ch; } +.notes li { + display: grid; + grid-template-columns: 4.5rem 1fr; + gap: 0.75rem; + padding: 0.5rem 0; + border-top: 1px solid var(--rule); + cursor: pointer; +} +.notes li:hover .where { text-decoration: underline; } +.notes .where { font-family: var(--font-display); font-size: 1.05rem; color: var(--rubric); } +.notes .warning .where { color: var(--gold); } + +@media (max-width: 800px) { + .workspace { grid-template-columns: 1fr; height: auto; } + .source { border-right: 0; border-bottom: 1px solid var(--rule); height: 55vh; } + .result { padding: 1.25rem 1rem 2rem; } +} diff --git a/web/theos.css b/web/theos.css new file mode 100644 index 0000000..c0b8ffb --- /dev/null +++ b/web/theos.css @@ -0,0 +1,70 @@ +/* Theos — shared by the playground and the gallery. Palette drawn from manuscript pigments. */ +:root { + --vellum: #f3f4f1; + --ink: #23212b; + --ink-soft: #565463; + --lapis: #1f4e9c; + --rubric: #b3261e; + --gold: #a8842a; + --rule: #c9ccc6; + --surface: #ffffff; + --page: var(--vellum); + --font-display: "IM Fell English", Georgia, serif; + --font-ui: "Alegreya Sans", "Segoe UI", sans-serif; + --font-code: "JetBrains Mono", Consolas, monospace; + color-scheme: light; +} + +@media (prefers-color-scheme: dark) { + :root:not([data-theme="light"]) { + --vellum: #1c1b22; + --ink: #e7e6ea; + --ink-soft: #a9a7b4; + --lapis: #8fb0ea; + --rubric: #f08a80; + --gold: #d9b95b; + --rule: #3a3944; + --surface: #24232b; + color-scheme: dark; + } +} + +* { box-sizing: border-box; } + +body { + margin: 0; + background: var(--vellum); + color: var(--ink); + font: 17px/1.5 var(--font-ui); +} + +a { color: var(--lapis); } +a:focus-visible, button:focus-visible, select:focus-visible, li[tabindex]:focus-visible { + outline: 3px solid var(--lapis); + outline-offset: 2px; +} + +code, .formula { font-family: var(--font-code); font-size: 0.9em; } + +/* The page: graph and gloss always sit on lit vellum, even in dark mode */ +.page { + background: #f3f4f1; + color: #23212b; + --ink: #23212b; + --ink-soft: #565463; + --lapis: #1f4e9c; + --rubric: #b3261e; + --gold: #a8842a; + --rule: #c9ccc6; +} + +.verdict { + font-family: var(--font-display); + font-size: clamp(1.9rem, 3.2vw, 2.8rem); + line-height: 1.1; + margin: 0; + color: var(--lapis); +} +.verdict.fails { color: var(--rubric); } +.verdict-detail { margin: 0.4rem 0 0; color: var(--ink-soft); max-width: 60ch; } +