Repository navigation
Theos 1.0: phases 0–9 into main - #12
Merged
Merged
Conversation
- Catch2 via FetchContent; tests wired into CTest; real validator, parser, exporter and binary-format tests - CI on Linux GCC, Linux Clang and Windows MSYS2/MinGW - C++23, warnings as errors on our targets, static runtime only on MinGW - Bounds-checked v1 binary reader: malformed files now throw instead of reading past the buffer - Mermaid labels escaped, duplicate edges removed - No debug output; diagnostics to stderr with exit codes 0/1/2 - MIT license; README/CLAUDE.md corrected; stale aquinas.md removed Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
- docs/spec/language.md: EBNF grammar for arguments, axioms, definitions, nodes, objections/replies, natural-deduction proofs and formulas (propositional, first-order, modal, property variables and lambda) - Lexer with code-point columns; diagnostics rendered as file:line:col with a caret line - Recursive-descent parser producing a typed AST; formulas parsed to an immutable expression tree with a canonical ASCII/Unicode printer - Canon registry: Protestant (66), Catholic (73), Orthodox (77) books with chapter counts; Quran surah/ayah bounds - Validator v2: name kinds, node-kind rules, cycles, grounding and relevance warnings, scripture resolution - Mermaid exporter v2 with axioms, formulas, objections and replies - CLI: theosc check / theosc export --format mermaid - Examples ported; resurrection now states its inference-to-the-best- explanation premise explicitly and carries an objection and reply - Golden tests (THEOS_UPDATE_GOLDEN=1 to refresh); Clang CI uses libc++ - v1 binary format removed (replaced by .theos v2 in Phase 2) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
- docs/spec/theos-v2.md: signature, CRC-protected header and chunks, critical/ancillary chunk rule, fixed-width little-endian records, annotated hex example - Encoder/decoder in src/core/binary.cpp: deduplicated string table, expression DAG with children-before-parents ordering, nodes, edges, axioms, definitions, objections and proofs - Reader rejects any out-of-range offset or index, bad CRC, non-zero padding, repeated or unknown critical chunks, and over-deep nesting - theosc build / inspect / inspect --chunks (chunk table + hex view) - Tests: round trip of every example, byte-stable golden file, every single-byte corruption and every truncation detected, line-ending conversion caught by the signature, chunk forward-compatibility rules - libFuzzer targets for the decoder and the parser, run 60 s each in CI - Clang CI moves to Clang 19 (libstdc++ std::expected support) - context.md removed (superseded by the v2 spec) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
Windows CI checked the golden .theo files out with CRLF; the renderer copied the trailing \r into the excerpt line, so output differed from the LF golden files. Strip it in the renderer (CRLF sources are normal on Windows) and pin text files to LF with .gitattributes so golden comparisons are byte-identical on every platform; .theos is binary. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
- docs/spec/proofs.md: justification forms, proof structure, rule catalogue (propositional, derived, quantifier, identity, S5 modal, definitions) - Logic core: alpha-equivalence, capture-avoiding substitution with beta-reduction for property variables, instance matching, definition expansion, fully-modalized test, fragment classification - Truth-table entailment with counterexamples for unjustified propositional inferences - Fitch-style proof checker: scopes, closed-subproof citation, fresh-name side conditions, strict (box) subproofs admitting only fully modalized formulas; 'by rule' as a one-step proof - Aquinas example now carries complete first-order proofs - Validator rejects recursive or forward-referencing definitions - 39 textbook exercises and rule/structure misuse tests Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
- Emscripten target (src/wasm/theos_wasm.cpp): embind check(source) returning diagnostics, node list and a Mermaid graph as JSON - Playground (web/): CodeMirror editor with .theo highlighting, live verdict, graph with failing nodes marked, diagnostics as glosses that jump to their line, shareable #src= links, examples - theosc site: gallery pages with graph, sources, definitions, claims, Fitch-style proofs (bars per subproof, strict double bars, underlined assumptions), objections and replies; index page - Manuscript palette shared by playground, gallery and Mermaid classDefs; long graph labels wrapped - Web workflow: native + wasm builds, Node wasm smoke test, Playwright browser smoke test, GitHub Pages deployment on main Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
- Sort checker: every free name gets one type (individual, proposition, predicate over individuals/properties, property) across node formulas, proof lines, objections and definitions; runs before proof checking - Spec section on sorts; tests for inference and each class of clash - library/arguments/: Aquinas's First Way, the kalam cosmological argument (new, with two objections and replies) and the resurrection argument - examples/: modus ponens and a deliberately invalid argument showing the counterexample output - Gallery, playground, tests and README follow the new layout Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
- S5 labelled tableau for propositional modal inferences: NNF, global necessities, one witness world per possibility, non-branching rules first, 200k-step budget; invalid inferences get a Kripke countermodel with duplicate worlds removed - Plantinga's modal ontological argument, checked by the tableau - Gödel's ontological argument (Scott's version) in higher-order S5: definitions of God-likeness, essence and necessary existence; T1, the corollary, T2 and T3 fully proved in natural deduction; objections on positivity and modal collapse - Tests: K, T, 4, 5, B, the S5 collapse, invalid forms, countermodel shape, and the step budget on a pigeonhole instance Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
- Import resolution: relative to the importing file, then -L dirs, then the bundled library; cycles reported with the chain; diamond imports merged once; every imported file checked in its own right - Standard library: library/std/principles.theo (non-contradiction, PSR, causal principle); bundled into the browser build as well - Dung grounded semantics over objections and replies, defeat propagated along inferences; statuses shown in Mermaid, the playground and the gallery - theosc analyze: what each conclusion rests on, premise load, unused nodes/axioms/citations (via proofs or re-deciding without a premise), objection outcomes, premises shared across files - Verdicts now say 'valid' and report contested conclusions separately - Library grows to ten arguments: Anselm, Aquinas's Third Way, Leibniz, the moral argument and Mackie's problem of evil join the existing five - docs/spec/analysis.md Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
- Translation to SMT-LIB 2: individuals, worlds for modal formulas (S5 as universal quantification over worlds, constant domains, rigid identity), properties with an application predicate and a comprehension axiom per lambda (Henkin semantics) - Z3 runs as an external program ( or z3 on the PATH), with a time limit; no link dependency, so MinGW builds are unaffected; the browser build reports that Z3 is unavailable - 'by z3' justification, theosc prove, theosc export --format smtlib - Z3 confirms every inference in the library except Goedel's T3, which it cannot decide in 20 s and which stands on its natural-deduction proof - Tests: script structure, valid and invalid inferences (so the encoding is not trivially inconsistent), 'by z3'; skipped when Z3 is absent - CI installs Z3 on Linux and in MSYS2 - docs/spec/smt.md Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
- Version 1.0.0 (theosc --version)
- Install layout: bin/theosc, share/theos/{library,docs}; theosc finds its
library relative to its own executable, so release archives work anywhere
- Release workflow: on a v* tag, build and test on Linux and Windows
(MSYS2), package archives, publish a GitHub release with the changelog
- docs/guide.md: tutorial building the fine-tuning argument step by step;
its finished file (examples/fine_tuning.theo) is part of the test suite
and every quoted output was taken from real runs
- Language, proof and binary specifications marked frozen for 1.0
- CHANGELOG, README (badges, installing), CLAUDE.md (commands, layout),
roadmap status
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019WEmxyo9CRKSbjbEdCuJTG
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars.
 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Brings Phases 0–9 to
mainin one merge.The stacked PRs each target the previous phase's branch, so merging them one by one lands each phase in its parent branch rather than
main. #2 merged intoroadmapand #3 intophase-0-foundation, which leftmainwith only #1.phase-9-releasecontains every phase, so this single PR is the complete change. It merges cleanly (checked withgit merge-tree), and CI on this head was green on every job: Linux GCC, Linux Clang 19, Windows MinGW, the fuzzers and the web build.Contents are exactly #2–#11; see those PRs for per-phase descriptions. After this merges, #4–#11 can be closed.
Generated by Claude Code