terraphim / terraphim/terraphim-ai
Create TypeScript bindings for TLA+ (@terraphim/tlaplus)
Nessuno ha ancora preso questa issue.
- Lingua principale
- Rust
- Stelle
- 62
- Fork
- 5
- Merge medio
- 2h 27m
- PR unite (30g)
- 1
Descrizione
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.
Guida per i contributori
Apri la guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Direzione di ricerca
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.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Valutazione
- Stack tecnologico
- java, typescript
- Ambito
- cli, compilers, devtools
- Tipo di issue
- Funzionalità
- Difficoltà
- 5/5
- Tempo stimato
- Più di una settimana
- Stato di attività
- Ferma
- Chiarezza
- Abbastanza chiara
- Idoneità per principianti
- 25/100