Create TypeScript bindings for TLA+ (@terraphim/tlaplus)
还没有人认领这个 Issue。
评估
- 难度
- 5/5
- 预计耗时
- 一周以上
- 新手友好度
- 25/100
- Issue 类型
- 功能
- 描述清晰度
- 基本清楚
- 活跃度
- 停滞
- 技术栈
- java, typescript
调研方向
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.
由索引模型根据 Issue 内容生成。
描述
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.
- 主要语言
- Rust
- 星标
- 62
- 派生
- 5
- 平均合并
- 2 小时 27 分钟
- 30 天内合并 PR
- 1
贡献指南
从这里开始
- 先读完整个 Issue,再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库,在一个分支上完成修改。
- 提交 Pull Request,并在描述里引用这个 Issue 编号。
terraphim/terraphim-ai 的其他 Issue
-
难度 5/5 一周以上 新手友好度 25/100
terraphim/terraphim-ai#885 ·
-
难度 4/5 3-5 天 新手友好度 55/100
terraphim/terraphim-ai#871 ·
-
enhancement
难度 5/5 一周以上 新手友好度 25/100
terraphim/terraphim-ai#810 · 2 条评论 ·
-
enhancement
难度 5/5 一周以上 新手友好度 35/100
terraphim/terraphim-ai#729 ·
-
enhancement
难度 5/5 一周以上 新手友好度 35/100
terraphim/terraphim-ai#728 ·
查看 terraphim/terraphim-ai 的全部 Issue
相似的 Issue
-
难度 2/5 1-3 小时 新手友好度 88/100
-
难度 2/5 1-3 小时 新手友好度 74/100
ontola/atomic-server#1625 ·
-
难度 2/5 1-3 小时 新手友好度 68/100
VirusTotal/yara-x#777 ·
-
难度 2/5 1-3 小时 新手友好度 82/100
stratum-mining/stratum#2404 ·
-
bug ci good first issue
难度 2/5 1-3 小时 新手友好度 88/100