diff --git a/CLAUDE.md b/CLAUDE.md index 3f3d547..ac5d973 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -8,6 +8,7 @@ - **Check the library:** `for f in library/arguments/*.theo; do ./build/theosc check $f; done` - **Fuzz (Clang 19):** `cmake -B build-fuzz -DCMAKE_CXX_COMPILER=clang++-19 -DTHEOS_FUZZ=ON -DTHEOS_BUILD_TESTS=OFF` - **WebAssembly (Emscripten 3.1.74):** `emcmake cmake -B build-wasm -DTHEOS_BUILD_TESTS=OFF && cmake --build build-wasm`, then `node tests/web/wasm_smoke.cjs` +- **README images:** `node tools/readme/render.cjs` regenerates `docs/assets/` from `build/theosc` and `web/dist` (needs ffmpeg and network) ## Layout - `src/core/`: lexer, parser, validator, types (sorts), checker (decision procedures + `proof_checker`), `s5`, `truth_table`, `logic` (substitution, alpha-equivalence, definitions), `dialectic`, `analysis`, `smt`, `binary`, `exporter`, `site`, `driver` (imports + pipeline). diff --git a/README.md b/README.md index 023523a..d9d2fd5 100644 --- a/README.md +++ b/README.md @@ -1,159 +1,331 @@ -# Theos Engine (`theosc`) +
+ + + + Theos: faith seeking understanding, machine-checked + + +
[![CI](https://github.com/JFrusher/theos-engine/actions/workflows/ci.yml/badge.svg)](https://github.com/JFrusher/theos-engine/actions/workflows/ci.yml) -[![Web](https://github.com/JFrusher/theos-engine/actions/workflows/web.yml/badge.svg)](https://github.com/JFrusher/theos-engine/actions/workflows/web.yml) +[![Pages](https://github.com/JFrusher/theos-engine/actions/workflows/web.yml/badge.svg)](https://github.com/JFrusher/theos-engine/actions/workflows/web.yml) +[![Release](https://img.shields.io/github/v/release/JFrusher/theos-engine?color=a8842a&label=release)](https://github.com/JFrusher/theos-engine/releases) +[![C++23](https://img.shields.io/badge/C%2B%2B-23-1f4e9c)](#build-from-source) +[![License: MIT](https://img.shields.io/badge/license-MIT-565463)](LICENSE) -A C++23 engine and CLI for writing, checking and visualizing formal theological and philosophical arguments. -New here? Start with the **[user guide](docs/guide.md)**. +**10** formalized arguments  ·  **38** inference rules  ·  **4** checking engines  ·  **87** tests  ·  fuzzed in CI ---- +Try it in your browser +  +Browse the gallery -## The Mission +
-Formal philosophy and historical theology, from scholastic proofs like Aquinas’s *Five Ways* to modern modal logic arguments, rely on rigorous chains of premises, deductions, and dependencies. Yet, these arguments are rarely treated as structured computational artifacts. +
-Theos bridges this gap. It provides a deterministic pipeline to turn human-readable philosophical arguments into statically checked, deeply validated graph structures, and serializes them into an optimized binary format for high-speed inspection and analysis. +Christians have argued for God with rigour since Anselm and Aquinas. **Theos makes that rigour checkable.** You write an argument the way a theologian would, each premise in plain words, grounded in Scripture, the Fathers or first principles. Next to the words you write the claim in formal logic, and the compiler `theosc` verifies that every step follows. When a step fails, it shows you why: the line that breaks, or a counterexample world where the premises hold and the conclusion doesn't. ---- +It is a real compiler written in modern C++23. It has its own natural-deduction proof checker, an S5 modal tableau and a Z3 bridge, a binary file format designed from the byte up, and a WebAssembly build that puts the whole checker in your browser. Gödel's ontological argument ships in the library, and every step of it is machine-checked. -## Pipeline +

+ theosc checking Gödel's argument, rejecting an overreaching edit and a fallacy, then compiling to .theos +

-``` -.theo source ─► Lexer ─► Parser ─► AST ─► Validator ─► Logic checker ─┬─► Mermaid exporter - └─► .theos binary (encode / decode) -``` +> [!NOTE] +> Theos checks **validity**, that the conclusion follows from the premises. Whether the premises are *true* is the debate the argument invites, so Theos records that too: every premise names its sources, and objections and replies are part of the file. -The logic checker proves that every deduction and conclusion follows from the nodes it cites: -propositional inferences are decided by truth table and propositional modal ones by an S5 tableau -(each with a counterexample when they fail), and anything richer is checked line by line as a Fitch-style natural-deduction proof covering -propositional, first-order, identity, S5 modal and higher-order (property) reasoning. The rules are -specified in [docs/spec/proofs.md](docs/spec/proofs.md). Any inference can also be handed to the -Z3 SMT solver (`by z3`, or `theosc prove` for a second opinion); see [docs/spec/smt.md](docs/spec/smt.md). +## Highlights -The library (`library/arguments/`) holds ten formalized arguments: Aquinas's First and Third Ways, -Anselm, the kalam argument, Leibniz's contingency argument, the moral argument, the resurrection, -Plantinga's modal ontological argument, Mackie's logical problem of evil, and **Gödel's ontological -argument in Scott's version**, every step of which is machine-checked in higher-order S5. -Objections and replies are evaluated with Dung's grounded semantics, so each page shows which -claims survive the recorded debate ([docs/spec/analysis.md](docs/spec/analysis.md)). + + + + + + + + + +
-Arguments can `import` each other and the standard library (`library/std/`), e.g. -`import "std/principles"` for the principle of sufficient reason. +### ⊢  A proof checker, not a linter +Fitch-style natural deduction covering propositional, first-order, identity, **S5 modal** and **higher-order** reasoning. Simple inferences need no proof at all: truth tables and an S5 tableau decide them, and print a countermodel when they fail. Any step can also be handed to the **Z3** SMT solver. -Each claim in a `.theo` file carries natural-language text and a formula: + -```theo -argument "Modus Ponens Demo" +### ✠  Grounded in Scripture and tradition +Premises cite `scripture(...)`, `source(...)` or `principle(...)`. References are checked against the **Protestant, Catholic and Orthodox** canons and the **Quran**, down to chapter and verse, so `John 22:1` is an error. -axiom Obs = source("Field notes", "p. 4") +
-premise P1 grounded_by [Obs] { - text: "If it rains, the street is wet." - formula: Rain -> Wet -} +### ⚔  Objections answered, in the open +Objections and replies are first-class. Theos evaluates the debate with **Dung's grounded semantics** and shows which claims still stand. A conclusion attacked by an unanswered objection is marked *contested*, never quietly passed. -premise P2 grounded_by [Obs] { - text: "It rains." - formula: Rain -} + + +### ◈  One engine, everywhere +The same C++ core runs as a CLI on **Linux and Windows**, as **WebAssembly** in the playground, and compiles arguments to **`.theos`**, a chunked, CRC-protected, fuzzed binary format with a full spec. + +
-conclusion C1 from [P1, P2] by imp_e { - text: "The street is wet." - formula: Wet +## Quickstart + +Grab a build for Linux or Windows from [**Releases**](https://github.com/JFrusher/theos-engine/releases), or [build from source](#build-from-source). Then: + +```sh +theosc check library/arguments/godel.theo # every step machine-checked +theosc check examples/affirming_the_consequent.theo # rejected, with a counterexample +theosc analyze library/arguments/kalam.theo # premises, chains, objections +``` + +Or skip the install and open the [**playground**](https://jfrusher.github.io/theos-engine/). New to the language? The [**user guide**](docs/guide.md) builds an argument from scratch in eight short steps. + +## Gödel, machine-checked + +Kurt Gödel left a short ontological proof in his notebooks, and Dana Scott later tidied it into a form logicians could work with. It reasons about properties of properties, in modal logic. That makes it famously hard to verify by hand, and it is the flagship of the Theos library. Here are the definitions and the first axiom, exactly as they appear in [`library/arguments/godel.theo`](library/arguments/godel.theo): + +```theo +define G(x) := forall F:prop. Positive(F) -> F(x) +define Ess(F:prop, x) := F(x) & (forall H:prop. H(x) -> []forall y. (F(y) -> H(y))) +define NE(x) := forall F:prop. Ess(F, x) -> []exists y. F(y) + +premise A1 grounded_by [Godel, Scott] { + text: "Necessarily, a property is positive exactly when its negation is not." + formula: [](forall F:prop. Positive(\x. ~F(x)) <-> ~Positive(F)) } ``` -The full language is specified in [docs/spec/language.md](docs/spec/language.md). +From five axioms, four natural-deduction proofs (T1, Cor, T2 and T3) reach the conclusion `□∃x. G(x)`, *necessarily, a God-like being exists*. The checker verifies each of their lines. Change any one of them and `theosc` names the line that no longer follows, as the recording above shows. Here is the structure of the argument, condensed from `theosc export --format mermaid` (the full export also carries every premise's wording and its sources): + +```mermaid +flowchart TD + classDef premise fill:#e7edf7,stroke:#1f4e9c,color:#23212b; + classDef deduction fill:#f3f4f1,stroke:#5b6b85,color:#23212b; + classDef conclusion fill:#d6e1f3,stroke:#1f4e9c,stroke-width:3px,color:#23212b; + classDef objection fill:#f7e3e1,stroke:#b3261e,color:#23212b; + classDef reply fill:#f6efd9,stroke:#a8842a,color:#23212b; + A1["A1 · negation
□∀F. Positive(¬F) ↔ ¬Positive(F)"]:::premise + A2["A2 · entailment
□∀F,H. Positive(F) ∧ □∀x(F(x) → H(x)) → Positive(H)"]:::premise + A3["A3 · God-likeness
□Positive(G)"]:::premise + A4["A4 · rigidity
□∀F. Positive(F) → □Positive(F)"]:::premise + A5["A5 · necessary existence
□Positive(NE)"]:::premise + T1["T1 · positive properties can be exemplified
∀F. Positive(F) → ◇∃x. F(x)"]:::deduction + Cor["Cor · a God-like being is possible
◇∃x. G(x)"]:::deduction + T2["T2 · God-likeness is an essence
□∀x. G(x) → Ess(G, x)"]:::deduction + T3["T3 · necessarily, a God-like being exists
□∃x. G(x)"]:::conclusion + O1{{"O1 · 'positive' is never defined"}}:::objection + R1{{"R1 · the axioms have models
(Benzmüller and Woltzenlogel Paleo, 2014)"}}:::reply + O2{{"O2 · modal collapse (Sobel)"}}:::objection + R2{{"R2 · Anderson's emended axioms"}}:::reply + A1 & A2 --> T1 + T1 & A3 --> Cor + A1 & A4 --> T2 + Cor & T2 & A5 --> T3 + O1 -. objects .-> A1 + R1 -. replies .-> O1 + O2 -. objects .-> T3 + R2 -. replies .-> O2 +``` ---- +## Write it, see it hold + +The [playground](https://jfrusher.github.io/theos-engine/) runs the checker in your browser as WebAssembly, with no server involved. As you type, it re-checks the argument, redraws the graph and marks failing lines. Here it rejects affirming the consequent, then accepts the repaired argument: + +

+ The Theos playground rejecting affirming the consequent, then accepting modus ponens after four edits +

+ +The [gallery](https://jfrusher.github.io/theos-engine/gallery/) gives every library argument its own page. Each page shows the graph, sources, Fitch-style proofs and objections, and is generated by `theosc site`. + +## The library + +Ten arguments, each passing `theosc check`. Theos does not flatter its own side: where a recorded objection still stands, the verdict says so. + +| Argument | Checked by | Grounded in | Verdict | +|---|---|---|---| +| [Gödel's ontological argument](library/arguments/godel.theo) (Scott's version) | 4 proofs, higher-order S5 | Gödel 1970, Scott 1972 | ✅ valid · 2 objections answered | +| [The modal ontological argument](library/arguments/plantinga.theo) (Plantinga) | S5 tableau, `box_e` | *The Nature of Necessity* | ✅ valid · objection answered | +| [The ontological argument](library/arguments/anselm.theo) (Anselm) | proof, first-order | *Proslogion* ch. 2 | ✅ valid · objection answered | +| [The kalam cosmological argument](library/arguments/kalam.theo) | 2 proofs, first-order | Genesis 1:1, al-Ghazali, Craig | ✅ valid · 2 objections answered | +| [The First Way](library/arguments/aquinas_first_way.theo) (Aquinas) | 2 proofs, first-order | *Summa* I q.2 a.3, Psalm 102, Hebrews 1 | ✅ valid | +| [The argument from contingency](library/arguments/leibniz.theo) (Leibniz) | 2 proofs, imports `std/principles` | *Monadology* §§ 36–38 | ✅ valid · objection answered | +| [The moral argument](library/arguments/moral_argument.theo) | truth table | Craig, *Reasonable Faith* | ✅ valid · objection answered | +| [The resurrection](library/arguments/resurrection.theo) (minimal facts) | truth table | 1 Corinthians 15, Mark 16, Luke 24 | ✅ valid · objection answered | +| [The Third Way](library/arguments/aquinas_third_way.theo) (Aquinas) | 2 proofs, first-order | *Summa* I q.2 a.3 | ⚠️ valid, but P1 falls to the quantifier-shift objection (Kenny) | +| [The logical problem of evil](library/arguments/problem_of_evil.theo) (Mackie) | truth table | Mackie 1955 | ⚠️ valid, but P2 falls to the free-will defence (Plantinga) | + +## How it works + +```mermaid +flowchart LR + src[".theo source"] --> lex[Lexer] --> parse[Parser] --> val["Validator
names · sorts · canons"] + val --> check{"Checker"} + check -->|propositional| tt["Truth table
+ countermodel"] + check -->|propositional modal| s5["S5 tableau
+ Kripke countermodel"] + check -->|"proof { … }"| nd["Natural deduction
38 rules"] + check -->|"by z3"| z3["Z3 via SMT-LIB"] + val --> dial["Grounded semantics
objections · replies"] + check --> out(("checked
argument")) + dial --> out + out --> bin[".theos binary"] + out --> mmd["Mermaid graph"] + out --> site["Static gallery"] + out --> wasm["WebAssembly playground"] +``` -## The `.theos` Binary Format +Each inferred node is justified in exactly one way. With no justification written, the checker *decides* the inference itself. `by rule` applies a single rule, `by z3` asks the solver, and `proof { … }` gives a full natural-deduction proof: -`theosc build` compiles a checked argument into a `.theos` file, specified in -[docs/spec/theos-v2.md](docs/spec/theos-v2.md): +| Fragment | Engine | When it fails you get | +|---|---|---| +| Propositional | Truth table (up to 20 atoms) | A counterexample row: `Rain = false, Wet = true` | +| Propositional S5 | Labelled tableau, constant domains | A Kripke countermodel: one valuation per world | +| First-order, identity, S5, higher-order | Your proof, checked line by line | The exact line and rule that does not apply | +| Anything in the SMT fragment | Z3 (optional) | Z3's countermodel | -- PNG-style signature (`89 54 48 45 4F 0D 0A 1A`) that detects text-mode corruption -- Tagged, CRC-32-protected chunks; unknown ancillary chunks are skipped, unknown critical chunks rejected -- Fixed-width little-endian records referencing each other by index, for O(1) access -- One deduplicated string table and one expression table with shared sub-formulas -- A reader that bounds-checks every offset and index, fuzzed with libFuzzer in CI +The rules, from `and_i` to `barcan`, are specified in [docs/spec/proofs.md](docs/spec/proofs.md). ---- +## The `.theos` binary format -## On the web +`theosc build` compiles a checked argument into `.theos`, a format designed at the byte level. It borrows PNG's signature and chunk layout and stores a formula DAG whose nodes always reference earlier ones, so a reader decodes it in a single pass. Every byte of a small file: -The `Web` workflow publishes two things to GitHub Pages: +

+ + + Byte map of a 452-byte .theos file, colored by chunk + +

-- **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`. +- **Corruption-evident.** The signature `89 54 48 45 4F 0D 0A 1A` catches 7-bit and line-ending damage, and CRC-32 covers the header and every chunk. +- **Evolvable.** As in PNG, a lowercase tag marks an ancillary chunk, which readers skip, and an uppercase tag marks a critical chunk, which they reject if unknown. +- **O(1) access.** Records are fixed-width and little-endian, reference each other by index, and keep payloads 4-byte aligned. +- **Hostile-input safe.** Every offset and index is bounds-checked and the padding must be zero. The reader is fuzzed with libFuzzer in CI. -See [web/README.md](web/README.md) to build them locally. +`theosc inspect --chunks` prints the chunk table of any file. The full spec, with an annotated hex walkthrough, is [docs/spec/theos-v2.md](docs/spec/theos-v2.md). ---- +## Going deeper -## CLI Usage +
+A tour of the language +
-```sh -theosc check library/arguments/aquinas_first_way.theo -theosc check examples/affirming_the_consequent.theo # rejected, with a counterexample -theosc export library/arguments/resurrection.theo --format mermaid -o resurrection.mmd -theosc build library/arguments/resurrection.theo -o resurrection.theos -theosc inspect resurrection.theos # decoded argument -theosc inspect resurrection.theos --chunks # chunk table and hex view -theosc analyze library/arguments/*.theo # dependencies, unused citations, objections -theosc prove library/arguments/godel.theo # second opinion from the Z3 SMT solver -theosc export library/arguments/kalam.theo --format smtlib # the SMT-LIB scripts -theosc site library/arguments -o site/gallery # static gallery pages +Every claim carries `text` for readers and a `formula` for the checker. Formulas accept ASCII or Unicode (`[]` or `□`, `forall` or `∀`). + +```theo +argument "The Kalam Cosmological Argument" by "William Lane Craig, after al-Ghazali" + +axiom ExNihilo = principle("Nothing comes from nothing.") +axiom Gen1 = scripture(protestant, "Genesis 1:1") + +premise P1 grounded_by [ExNihilo] { + text: "Whatever begins to exist has a cause." + formula: forall x. Began(x) -> exists y. Causes(y, x) +} + +premise P2 grounded_by [Gen1] { + text: "The universe began to exist." + formula: Began(universe) +} + +conclusion C1 from [P1, P2] { + text: "Therefore the universe has a cause." + formula: exists y. Causes(y, universe) + proof { + 1. forall x. Began(x) -> exists y. Causes(y, x) premise P1 + 2. Began(universe) premise P2 + 3. Began(universe) -> exists y. Causes(y, universe) forall_e 1 + 4. exists y. Causes(y, universe) imp_e 3, 2 + } +} + +objection O1 against P1 { + text: "Quantum events, such as radioactive decay, seem to begin without a cause." +} + +reply R1 to O1 { + text: "Quantum events arise within a vacuum governed by physical law, which is not nothing." +} ``` -Diagnostics go to stderr as `file:line:col: error: message` with the source line underneath; -exit code 0 = success, 1 = invalid input, 2 = usage error. +Arguments can `import` each other and the standard library, e.g. `import "std/principles"` for the principle of sufficient reason. The full grammar is in [docs/spec/language.md](docs/spec/language.md). ---- +
-## Project Structure +
+Scripture references are checked +
```text -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/ # User guide; language, proof, analysis, SMT and binary specifications -├── examples/ # Small teaching examples -├── library/ # Formalized arguments (the gallery) -├── fuzz/ # libFuzzer targets and seed corpora -└── tests/ # Catch2 unit tests and golden files +$ theosc check scripture.theo +scripture.theo:3:1: error: chapter out of range in 'John 22:1': John has 21 chapters + axiom J = scripture(protestant, "John 22:1") + ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +scripture.theo:4:1: error: verse out of range in '2:300' + axiom Q = scripture(quran, "2:300") + ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +scripture.theo:5:1: error: unknown book 'Tobit' in the protestant canon + axiom T = scripture(protestant, "Tobit 1:1") + ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ``` ---- +`Tobit 1:1` is fine under `catholic` or `orthodox`, the canons that include it. -## Installing +
-Release archives for Linux and Windows are attached to each -[GitHub release](https://github.com/JFrusher/theos-engine/releases). Unpack one and run -`bin/theosc`; the standard library ships alongside it in `share/theos/library`. +
+CLI reference +
---- +| Command | Does | +|---|---| +| `theosc check ` | Parse, validate and check every inference | +| `theosc analyze ...` | Premise load, longest chains, unused citations, objection status; shared premises across files | +| `theosc prove ` | Send every inference to Z3 for a second opinion | +| `theosc export --format mermaid\|smtlib [-o out]` | Argument graph, or the SMT-LIB scripts | +| `theosc build [-o out.theos]` | Compile to the binary format | +| `theosc inspect [--chunks]` | Decode a binary, or show its chunk table and hex | +| `theosc site ... -o ` | Generate the static gallery | + +`-L ` adds an import search directory. Diagnostics are printed as `file:line:col: error: message` with a caret under the source. Exit codes: `0` ok, `1` invalid input, `2` usage error. + +
-## Building from Source +
+Project layout +
+ +```text +include/theos/ public headers +src/core/ lexer, parser, validator, sorts, checker, S5 tableau, proof checker, + dialectic, analysis, SMT, binary format, exporter, site, driver +src/cli/ theosc +src/wasm/ WebAssembly entry point for the playground +web/ playground and gallery styles, site assembly +library/ the argument gallery and the importable standard library +docs/ user guide and the five specifications +fuzz/ libFuzzer targets and seed corpora +tests/ Catch2 unit tests, golden files, browser smoke tests +tools/readme/ regenerates the images in this README from the real tool +``` -Requires CMake 3.20+ and a C++23 compiler (GCC 13+, Clang 19+, or MinGW-w64 GCC 13+ via MSYS2). -Tests use Catch2, fetched automatically by CMake. [Z3](https://github.com/Z3Prover/z3) is optional: -it is needed for `by z3` and `theosc prove`, and its tests are skipped without it -(`apt install z3`, or `pacman -S mingw-w64-ucrt-x86_64-z3` in MSYS2). +
+ +## Build from source + +You need CMake 3.20+ and a C++23 compiler: GCC 13+, Clang 19+, or MinGW-w64 GCC 13+ via MSYS2. CMake fetches Catch2 for the tests. [Z3](https://github.com/Z3Prover/z3) is optional; it powers `by z3` and `theosc prove` (`apt install z3`, or `pacman -S mingw-w64-ucrt-x86_64-z3`). ```sh cmake -B build -DCMAKE_BUILD_TYPE=Release cmake --build build ctest --test-dir build --output-on-failure -./build/theosc ``` -Fuzzing (Clang 19+): `cmake -B build-fuzz -DCMAKE_CXX_COMPILER=clang++-19 -DTHEOS_FUZZ=ON -DTHEOS_BUILD_TESTS=OFF`, -then `./build-fuzz/fuzz/decode_fuzzer fuzz/corpus/decode`. +On Windows, run the same commands from an MSYS2 UCRT64 shell. For fuzzing, configure with `-DCMAKE_CXX_COMPILER=clang++-19 -DTHEOS_FUZZ=ON -DTHEOS_BUILD_TESTS=OFF`. The WebAssembly build is described in [web/README.md](web/README.md). The images in this README are regenerated from the real tool by `node tools/readme/render.cjs`. + +--- + +
+ +*Credo ut intelligam.* (I believe, that I may understand.) -On Windows, run the same commands from an MSYS2 UCRT64 shell (add `-G "MinGW Makefiles"` or `-G Ninja` if needed). +[Roadmap](ROADMAP.md) · [Changelog](CHANGELOG.md) · [User guide](docs/guide.md) · [MIT License](LICENSE) -See [ROADMAP.md](ROADMAP.md) for where the project is going. Licensed under the [MIT License](LICENSE). +
diff --git a/docs/assets/banner-dark.png b/docs/assets/banner-dark.png new file mode 100644 index 0000000..cb017a2 Binary files /dev/null and b/docs/assets/banner-dark.png differ diff --git a/docs/assets/banner-light.png b/docs/assets/banner-light.png new file mode 100644 index 0000000..a55d5e0 Binary files /dev/null and b/docs/assets/banner-light.png differ diff --git a/docs/assets/playground.gif b/docs/assets/playground.gif new file mode 100644 index 0000000..27d078d Binary files /dev/null and b/docs/assets/playground.gif differ diff --git a/docs/assets/terminal.gif b/docs/assets/terminal.gif new file mode 100644 index 0000000..842cd1c Binary files /dev/null and b/docs/assets/terminal.gif differ diff --git a/docs/assets/theos-format-dark.png b/docs/assets/theos-format-dark.png new file mode 100644 index 0000000..b137e2d Binary files /dev/null and b/docs/assets/theos-format-dark.png differ diff --git a/docs/assets/theos-format-light.png b/docs/assets/theos-format-light.png new file mode 100644 index 0000000..b34e843 Binary files /dev/null and b/docs/assets/theos-format-light.png differ diff --git a/tools/readme/render.cjs b/tools/readme/render.cjs new file mode 100644 index 0000000..3b292d7 --- /dev/null +++ b/tools/readme/render.cjs @@ -0,0 +1,297 @@ +// Renders the README images in docs/assets/ from the real tool: every terminal +// line is captured from build/theosc, the playground is the real WebAssembly site. +// Usage: node tools/readme/render.cjs [banner|format|terminal|playground ...] +// Needs: build/theosc, web/dist (WebAssembly build), ffmpeg, Playwright, network for fonts/CDN. +'use strict'; +const { execFileSync, execSync } = require('node:child_process'); +const fs = require('node:fs'); +const http = require('node:http'); +const os = require('node:os'); +const path = require('node:path'); +const { chromium } = require('playwright'); + +const ROOT = path.resolve(__dirname, '../..'); +const THEOSC = path.join(ROOT, 'build/theosc'); +const OUT = path.join(ROOT, 'docs/assets'); +const TMP = fs.mkdtempSync(path.join(os.tmpdir(), 'theos-readme-')); + +// Palette from web/theos.css +const THEMES = { + light: { page: '#f3f4f1', ink: '#23212b', soft: '#565463', lapis: '#1f4e9c', rubric: '#b3261e', gold: '#a8842a', rule: '#c9ccc6', surface: '#ffffff' }, + dark: { page: '#1c1b22', ink: '#e7e6ea', soft: '#a9a7b4', lapis: '#8fb0ea', rubric: '#f08a80', gold: '#d9b95b', rule: '#3a3944', surface: '#24232b' }, +}; +const FONTS = ''; + +const esc = s => s.replace(/&/g, '&').replace(//g, '>'); +const sleep = ms => new Promise(r => setTimeout(r, ms)); + +async function shoot(page, html, file, selector = '#frame') { + await page.setContent(html, { waitUntil: 'networkidle' }); + await page.evaluate(() => document.fonts.ready); + await page.locator(selector).screenshot({ path: path.join(OUT, file) }); + console.log('wrote', file); +} + +// frames: [{ file, ms }] -> optimized GIF +function gif(frames, file, width) { + const list = frames.map(f => `file '${f.file}'\nduration ${(f.ms / 1000).toFixed(3)}`).join('\n') + `\nfile '${frames.at(-1).file}'\n`; + const listFile = path.join(TMP, `${file}.txt`); + fs.writeFileSync(listFile, list); + const scale = `scale=${width}:-1:flags=lanczos`; + execFileSync('ffmpeg', ['-y', '-loglevel', 'error', '-f', 'concat', '-safe', '0', '-i', listFile, + '-vf', `${scale},split[a][b];[a]palettegen=stats_mode=diff:max_colors=128[p];[b][p]paletteuse=dither=none:diff_mode=rectangle`, + '-loop', '0', path.join(OUT, file)]); + console.log('wrote', file, `${(fs.statSync(path.join(OUT, file)).size / 1e6).toFixed(2)} MB`); +} + +// ---------------------------------------------------------------- banner + +function bannerHtml(t) { + return `${FONTS} +
+
T
+
+
Theos
+
Fides quaerens intellectum
+
Faith seeking understanding, machine-checked. Write the arguments of faith in formal logic; Theos verifies every step.
+
+
□∃x. G(x)godel.theo: ok
+
`; +} + +// ---------------------------------------------------------------- .theos byte map + +function chunks(bytes) { + const out = []; + let off = 24; + while (off < bytes.length) { + const tag = bytes.toString('latin1', off, off + 4); + const len = bytes.readUInt32LE(off + 4); + out.push({ tag, off, len, pad: (4 - (len % 4)) % 4 }); + off += 12 + len + ((4 - (len % 4)) % 4); + } + return out; +} + +function formatHtml(t, bytes) { + const colors = { META: '#b5527a', STRS: '#a8842a', FORM: '#1f4e9c', AXIM: '#b3261e', DEFN: '#5b6b85', NODE: '#2e7d5b', EDGE: '#6a4c93', DIAL: '#c2571a', PROF: '#3b7fa6' }; + const region = new Array(bytes.length); + for (let i = 0; i < 8; i++) region[i] = { c: t.ink, k: 'sig' }; + for (let i = 8; i < 24; i++) region[i] = { c: t.soft, k: 'hdr' }; + const list = chunks(bytes); + for (const ch of list) { + for (let i = ch.off; i < ch.off + 12; i++) region[i] = { c: colors[ch.tag], k: 'head' }; + for (let i = ch.off + 12; i < ch.off + 12 + ch.len; i++) region[i] = { c: colors[ch.tag], k: 'body' }; + for (let i = ch.off + 12 + ch.len; i < ch.off + 12 + ch.len + ch.pad; i++) region[i] = { c: t.rule, k: 'pad' }; + } + const cells = [...bytes].map((b, i) => { + const r = region[i]; + const hex = b.toString(16).toUpperCase().padStart(2, '0'); + const style = r.k === 'head' || r.k === 'sig' ? `background:${r.c};color:#fff` : r.k === 'pad' ? `color:${t.soft};border-color:${t.rule}` : `color:${r.c};border-color:${r.c}`; + return `${hex}`; + }); + const rows = []; + for (let i = 0; i < cells.length; i += 16) rows.push(`
${i.toString(16).toUpperCase().padStart(4, '0')}${cells.slice(i, i + 16).join('')}
`); + const legend = [ + `
  • Signature 89 THEO 0D 0A 1A
    • `, + `
  • Header version, chunk count, size, CRC-32
    • `, + ...list.map(ch => `
  • ${ch.tag} ${{ META: 'title, author, imports', STRS: 'deduplicated strings', FORM: 'formula DAG, children first', AXIM: 'axioms, scripture resolved', DEFN: 'definitions', NODE: 'premises and conclusions', EDGE: 'from and grounded_by edges', DIAL: 'objections and replies', PROF: 'Fitch proofs' }[ch.tag]} ${ch.len} B
    • `), + ].join(''); + return `${FONTS} +
    +

    Anatomy of a .theos file

    tests/golden/binary/tiny.theo, all ${bytes.length} bytes

    ${rows.join('')}
    +

    Filled cells: chunk tag, length and CRC-32. Outlined: payload. Dashed: padding to 4 bytes.

    +
    `; +} + +// ---------------------------------------------------------------- terminal + +const SCENES = [ + { cmd: 'theosc check godel.theo', hold: 1400 }, + { comment: '# T1 says a positive property is *possibly* exemplified. Claim more:' }, + { cmd: "sed 's/24. <>exists/24. exists/' godel.theo > overreach.theo", hold: 300 }, + { cmd: 'theosc check overreach.theo', hold: 3200 }, + { cmd: 'theosc check affirming_the_consequent.theo', hold: 3200 }, + { cmd: 'theosc build godel.theo && theosc inspect godel.theos --chunks | head -15', hold: 4000 }, +]; + +function colorize(line) { + const e = esc(line); + if (/^\s*\^~*$/.test(line)) return `${e}`; + if (/: error: /.test(line)) return e.replace(/^(.*?:\d+:\d+:) error: (.*)$/, '$1 error: $2'); + if (/: ok$/.test(line)) return e.replace(/ok$/, 'ok'); + if (/\s(ok)$/.test(line)) return e.replace(/ok$/, 'ok'); + if (/^\s+tag\s+offset/.test(line) || /^\.theos v/.test(line)) return `${e}`; + if (/^\s+[0-9A-F]{8}\s/.test(line)) return `${e}`; + return e; +} + +function terminalHtml(t) { + return `${FONTS} +
    theosc
    `;
+}
+
+async function terminal(page) {
+  const work = path.join(TMP, 'term');
+  fs.mkdirSync(work);
+  fs.copyFileSync(path.join(ROOT, 'library/arguments/godel.theo'), path.join(work, 'godel.theo'));
+  fs.copyFileSync(path.join(ROOT, 'examples/affirming_the_consequent.theo'), path.join(work, 'affirming_the_consequent.theo'));
+  const env = { ...process.env, PATH: `${path.dirname(THEOSC)}:${process.env.PATH}` };
+
+  await page.setViewportSize({ width: 1140, height: 700 });
+  await page.setContent(terminalHtml(THEMES.dark), { waitUntil: 'networkidle' });
+  await page.evaluate(() => document.fonts.ready);
+
+  const done = [];      // rendered lines so far
+  const frames = [];
+  const frame = async (lines, ms) => {
+    const file = path.join(TMP, `t${String(frames.length).padStart(4, '0')}.png`);
+    await page.evaluate(html => { document.getElementById('screen').innerHTML = html; }, lines.slice(-22).map(l => `
    ${l || ' '}
    `).join(''));
+    await page.locator('#frame').screenshot({ path: file });
+    frames.push({ file, ms });
+  };
+  const prompt = '❯ ';
+  await frame([prompt + ' '], 700);
+  for (const s of SCENES) {
+    if (s.comment) {
+      done.push(prompt + `${esc(s.comment)}`);
+      await frame([...done, prompt + ' '], 1800);
+      continue;
+    }
+    for (let i = 2; i <= s.cmd.length + 1; i += 2) {
+      await frame([...done, prompt + esc(s.cmd.slice(0, i)) + ' '], 45);
+    }
+    await frame([...done, prompt + esc(s.cmd)], 350);
+    let out = '';
+    try { out = execSync(`${s.cmd} 2>&1`, { cwd: work, env, encoding: 'utf8', shell: '/bin/sh' }); } catch (err) { out = err.stdout; }
+    done.push(prompt + esc(s.cmd), ...out.replace(/\n$/, '').split('\n').filter(l => out !== '').map(colorize));
+    await frame([...done, prompt + ' '], s.hold);
+  }
+  frames.at(-1).ms = 4500;
+  gif(frames, 'terminal.gif', 1100);
+}
+
+// ---------------------------------------------------------------- playground
+
+async function playground(browser) {
+  const site = path.join(TMP, 'site');
+  execFileSync(path.join(ROOT, 'web/build-site.sh'), [THEOSC, site], { stdio: 'ignore' });
+  const types = { '.html': 'text/html', '.js': 'text/javascript', '.css': 'text/css', '.wasm': 'application/wasm' };
+  const server = http.createServer((req, res) => {
+    const file = path.join(site, decodeURIComponent(req.url.split('?')[0]));
+    if (!file.startsWith(site) || !fs.existsSync(file) || fs.statSync(file).isDirectory()) { res.writeHead(404); res.end(); return; }
+    res.writeHead(200, { 'content-type': types[path.extname(file)] ?? 'application/octet-stream' });
+    fs.createReadStream(file).pipe(res);
+  });
+  await new Promise(r => server.listen(0, r));
+  const page = await browser.newPage({ viewport: { width: 1280, height: 720 }, deviceScaleFactor: 1.5 });
+  await page.goto(`http://localhost:${server.address().port}/index.html`);
+  await page.waitForSelector('#graph svg', { timeout: 30000 });
+  await page.evaluate(() => document.fonts.ready);
+  await sleep(500);
+
+  // Screenshot continuously while the script drives the page; each frame lasts until the next.
+  const frames = [];
+  let recording = true;
+  const recorder = (async () => {
+    while (recording) {
+      const file = path.join(TMP, `p${String(frames.length).padStart(4, '0')}.png`);
+      const t = Date.now();
+      await page.screenshot({ path: file });
+      frames.push({ file, t });
+    }
+  })();
+
+  const replace = async (line, from, to) => {
+    await page.evaluate(([line, from]) => {
+      const cm = document.querySelector('.CodeMirror').CodeMirror;
+      const ch = cm.getLine(line).lastIndexOf(from);
+      cm.focus();
+      cm.setSelection({ line, ch }, { line, ch: ch + from.length });
+    }, [line, from]);
+    await sleep(350);
+    await page.keyboard.type(to, { delay: 110 });
+    await sleep(500);
+  };
+
+  await sleep(1800);
+  await page.selectOption('#examples', 'examples/affirming_the_consequent.theo');
+  await page.waitForSelector('#verdict.fails');
+  await sleep(3200);
+  // Turn affirming the consequent into modus ponens, one edit at a time
+  await replace(13, 'The street is wet.', 'It rains.');
+  await replace(18, 'It rains.', 'The street is wet.');
+  await replace(14, 'Wet', 'Rain');
+  await replace(19, 'Rain', 'Wet');
+  await page.waitForFunction(() => document.getElementById('verdict').textContent === 'The argument is valid.');
+  await sleep(4000);
+  recording = false;
+  await recorder;
+  server.close();
+
+  const timed = frames.map((f, i) => ({ file: f.file, ms: i + 1 < frames.length ? frames[i + 1].t - f.t : 2500 }));
+  gif(timed, 'playground.gif', 1200);
+}
+
+// ---------------------------------------------------------------- main
+
+(async () => {
+  const which = process.argv.slice(2);
+  const want = name => which.length === 0 || which.includes(name);
+  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({ deviceScaleFactor: 2, viewport: { width: 1400, height: 1000 } });
+    if (want('banner')) {
+      for (const [name, t] of Object.entries(THEMES)) await shoot(page, bannerHtml(t), `banner-${name}.png`);
+    }
+    if (want('format')) {
+      const file = path.join(TMP, 'tiny.theos');
+      execFileSync(THEOSC, ['build', 'tests/golden/binary/tiny.theo', '-o', file], { cwd: ROOT });  // relative path, as in docs/spec/theos-v2.md
+      const bytes = fs.readFileSync(file);
+      for (const [name, t] of Object.entries(THEMES)) await shoot(page, formatHtml(t, bytes), `theos-format-${name}.png`);
+    }
+    if (want('terminal')) await terminal(await browser.newPage({ deviceScaleFactor: 1.5 }));
+    if (want('playground')) await playground(browser);
+  } finally {
+    await browser.close();
+    fs.rmSync(TMP, { recursive: true, force: true });
+  }
+})().catch(err => { console.error(err); process.exit(1); });