terraphim / terraphim/terraphim-ai
Create TypeScript bindings for TLA+ (@terraphim/tlaplus)
Dieses Issue hat noch niemand übernommen.
- Vorherrschende Sprache
- Rust
- Sterne
- 62
- Forks
- 5
- Ø Merge
- 2 Std. 27 Min.
- Gemergte PRs (30 T.)
- 1
Beschreibung
Summary
Create a TypeScript library @terraphim/tlaplus providing native TLA+ tooling: parsing via tree-sitter-tlaplus, typed AST, expression evaluation, formatting, and TLC model checking bridge. Implementation will be orchestrated by Symphony on bigbox with output to Gitea.
Research & Design Documents
- Research:
docs/src/research/tlaplus-typescript-bindings.md - Design:
docs/src/research/tlaplus-typescript-design.md
Key Findings
The TLA+ ecosystem already has significant TypeScript/JavaScript implementations:
- tree-sitter-tlaplus (
@tlaplus/tree-sitter-tlapluson npm) - production-ready parser - Spectacle - full JS TLA+ interpreter (~5000 LOC) by Will Schultz
- Quint - TypeScript-native TLA alternative by Informal Systems (1.2k stars)
- vscode-tlaplus - 97% TypeScript VS Code extension
Architecture
@terraphim/tlaplus
src/parser/ - tree-sitter wrapper, CST-to-AST transform
src/ast/ - TypeScript type definitions for TLA+ AST
src/eval/ - Expression evaluator (sets, logic, functions)
src/format/ - Pretty-printer
src/bridge/ - TLC model checking bridge (Java CLI)
src/cli/ - CLI tool (parse|format|validate|check)
Gitea Issue Decomposition (for Symphony)
| # | Title | Dependencies | Wave |
|---|---|---|---|
| 1 | Scaffold TypeScript project with build tooling | None | A |
| 2 | Define TypeScript types for TLA+ AST | None | A |
| 3 | Implement tree-sitter parser wrapper with CST-to-AST | #1, #2 | B |
| 4 | Implement basic expression evaluator | #2, #3 | C |
| 5 | Implement TLA+ formatter (pretty-printer) | #3 | C |
| 6 | Implement TLC CLI bridge for model checking | #1 | B |
| 7 | Create CLI tool (parse, format, validate, check) | #3, #4, #5, #6 | D |
| 8 | Documentation, examples, npm publish prep | #7 | E |
Symphony WORKFLOW.md
tracker:
kind: gitea
endpoint: https://git.terraphim.cloud
api_key: $GITEA_TOKEN
owner: terraphim
repo: tlaplus-ts
agent:
runner: claude-code
max_concurrent_agents: 2
max_turns: 15
claude_flags: "--dangerously-skip-permissions --allowedTools Bash,Read,Write,Edit,Glob,Grep"
settings: ~/.claude/symphony-settings.json
Next Steps
- Create Gitea repo
terraphim/tlaplus-ts - Create 8 Gitea issues with dependencies
- Deploy WORKFLOW.md to bigbox
- Run Symphony to dispatch Claude Code agents
See design document for full issue descriptions and acceptance criteria.
Beitragsleitfaden
Erste Schritte
- Lies das ganze Issue und danach den Beitragsleitfaden des Projekts.
- Schreib ins Issue, dass du es übernimmst — das erspart doppelte Arbeit.
- Forke das Repository und arbeite in einem Branch.
- Öffne einen Pull Request, der die Issue-Nummer nennt.
Rechercherichtung
Read docs/src/research/tlaplus-typescript-bindings.md and docs/src/research/tlaplus-typescript-design.md first, then compare the proposed src/parser, src/ast, src/eval, src/format, src/bridge, and src/cli areas with the eight decomposed Gitea tasks. Done means the @terraphim/tlaplus package and its documented tooling are implemented through the CLI and prepared for npm publication.
Vom Indexierungsmodell aus dem Issue-Text verfasst.
Bewertung
- Tech-Stack
- java, typescript
- Bereich
- cli, compilers, devtools
- Issue-Typ
- Feature
- Schwierigkeit
- 5/5
- Geschätzter Aufwand
- Über eine Woche
- Aktivitätsstatus
- Veraltet
- Klarheit
- Größtenteils klar
- Anfängerfreundlichkeit
- 25/100