Create TypeScript bindings for TLA+ (@terraphim/tlaplus)

[AlexMikhalev]

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-tlaplus on 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

1. Create Gitea repo terraphim/tlaplus-ts
2. Create 8 Gitea issues with dependencies
3. Deploy WORKFLOW.md to bigbox
4. Run Symphony to dispatch Claude Code agents

See design document for full issue descriptions and acceptance criteria.

[AlexMikhalev]

Re-run Plan (2026-03-14)

Lessons Learned from First Run

The first Symphony run of tlaplus-ts failed due to 5 root causes, all now fixed:

#	Root Cause	Fix Applied
1	No dependency enforcement -- blocked_by was empty, all 8 issues dispatched simultaneously	fetch_dependencies() populates blocked_by, dispatch.rs Todo blocker rule prevents dispatch until all blockers are terminal
2	All agents pushed to main -- merge conflicts	Branch-per-issue hooks: SYMPHONY_* env vars create symphony/issue-${NUMBER} branches
3	No agent guidance -- generic auto-commit messages	after_create hook generates CLAUDE.md with issue context
4	No concurrency limits -- all issues dispatched at once	Per-state concurrency limits in orchestrator config
5	No blocker state refresh -- stale dependency data	Reconciliation loop refreshes blocker states before each dispatch cycle

Additional improvement: PageRank-aware dispatch via Gitea Robot API integration -- issues with more downstream impact dispatch first.

Evidence from First Run

• 8/8 issues closed but code is incomplete (missing src/parser/, src/ast/)
• 0/11 dependency edges were defined (all issues had flat PageRank 0.15)
• 14 commits, 11 were "symphony: auto-commit" (no issue context)
• 116 dispatch attempts for 8 issues (no dispatch gating)
• No PRs created, all pushed directly to main

Re-run Steps

1. Commit Symphony fixes (dependency enforcement + PageRank integration) -- 5ee5c5ef
2. Build Symphony binary with all fixes
3. Reopen all 8 tlaplus-ts issues
4. Deploy Gitea API fix (dependency REST API was a stub, now implemented)
5. Add 11 dependency edges via gitea-robot add-dep
6. Verify graph with gitea-robot graph (should show 11 edges, PageRank > 0.15 for New persistance #1, Config #2)
7. Run Symphony on bigbox

Dependency Graph (Wave Structure)

Wave A (no deps):     #1 Scaffold    #2 AST Types
Wave B (blocked):     #3 Parser      #6 TLC Bridge
Wave C (blocked):     #4 Evaluator   #5 Formatter
Wave D (blocked):     #7 CLI
Wave E (blocked):     #8 Documentation

Gitea Fixes Required

The Gitea dependency REST API (/api/v1/repos/{owner}/{repo}/issues/{index}/dependencies) was a stub returning 201 without persisting. Fixed in:

• routers/api/v1/repo/issue_dep.go -- Full implementation of Create/Get/Delete for dependencies and blocks
• models/issues/dependency.go -- Added GetDependenciesByIssueID() and GetBlockedByDependencies() query functions

Gitea rebuild in progress on bigbox.

[AlexMikhalev]

Re-run Complete: All 8 Issues Dispatched and Closed

Symphony successfully re-ran the tlaplus-ts project with full dependency enforcement. All 8 issues were dispatched in topological order and completed.

Execution Timeline

Time (UTC)	Event	Details
18:11:14	Dispatch #1, #2	Root issues (unblocked)
18:12:33	#2 completed	16 turns, auto-closed
18:26:32	#1 completed	Retry attempt 1, 16 turns, auto-closed
18:26:44	Dispatch #3	Unblocked (#1, #2 closed)
18:27:46	#3 completed	16 turns, auto-closed
18:28:14	Dispatch #4, #5	Both unblocked (#3 closed), parallel
18:30:50	#5 completed	16 turns
18:32:57	#4 completed	16 turns
18:33:14	Dispatch #6	Unblocked (#1, #4, #5 all closed)
18:35:09	#6 completed	16 turns
18:35:14	Dispatch #7	Unblocked (#4, #5, #6 all closed)
18:37:00	#7 completed	11 turns
18:37:14	Dispatch #8	Unblocked (#6, #7 both closed)
18:41:18	#8 completed	16 turns, all done

Total wall-clock time: ~30 minutes for all 8 issues.

What Worked

1. Dependency enforcement: Issues dispatched only when all blockers reached terminal state
2. Parallel dispatch: Issues Axum server #4 and Pulling everything together - part 1 #5 ran concurrently (both depend only on Persistance config #3)
3. Branch-per-issue: Each issue got its own symphony/issue-N branch
4. Auto-close: after_run hook closes issues via Gitea API after push
5. Gitea Robot API: Dependencies persisted correctly after fixing issue_dep.go

Fixes Applied During Re-run

1. Gitea issue_dep.go -- Full implementation replacing stub (was returning 201 without persisting)
2. Form binding: Changed ctx.Data["form"] to web.GetForm(ctx) for Gitea API handlers
3. gitea-robot main.go -- Fixed request body to {"index": N} matching IssueMeta struct
4. Workflow after_run hook -- Added curl call to close issues via Gitea API

Branches Created

• symphony/issue-1 through symphony/issue-8 on git.terraphim.cloud/terraphim/tlaplus-ts

[AlexMikhalev]

Re-run #2 Results (2026-03-14)

Summary

All 8 issues dispatched and completed in ~9.5 minutes with correct dependency ordering.

Key Improvement: Agent Task Tracking via Gitea

Agents now use gitea-robot and tea CLI for task management:

• CLAUDE.md injected at workspace creation with issue-specific instructions
• tea comment N "message" used by 7/8 agents to post progress on their issues
• gitea-robot ready/triage available for agents to check project status
• CLAUDE.md added to .gitignore to prevent accidental commits

Dispatch Timeline

Time	Event
20:21:12	#1, #2 dispatched (parallel roots)
20:22:24	#1 completed (72s, 16 turns)
20:22:35	#2 completed (83s, 16 turns)
20:22:42	#3 dispatched
20:24:21	#3 completed (99s, 16 turns)
20:24:42	#4, #5 dispatched (parallel)
20:26:00	#4 completed (78s, 16 turns)
20:26:11	#5 completed (89s, 16 turns)
20:26:12	#6 dispatched
20:27:26	#6 completed (74s, 16 turns)
20:27:42	#7 dispatched
20:28:55	#7 completed (73s, 16 turns)
20:29:12	#8 dispatched
20:30:38	#8 completed (86s, 16 turns)

Remaining Issue

PageRank scores remain uniform at 0.15 despite 12 dependency edges. This is a bug in the Robot API's power iteration computation. Separate issue being filed.

[AlexMikhalev]

PageRank Bug Fixed and Verified

The Gitea Robot API PageRank computation was returning uniform 0.15 scores for all issues. Root cause identified and fixed:

Bugs Found and Fixed

1. Bug 3 (ROOT CAUSE): xorm struct tags with table-qualified names (xorm:"issue_dependency.issue_id") fail silently -- xorm cannot match dotted column names to result set columns, so all dependency data read as zero values. Fixed by using raw SQL with simple column names.
2. Bug 1: Adjacency matrix direction inverted -- rank was flowing to blocked issues instead of blockers. Fixed by reversing edge direction.
3. Bug 2: Duplicate dependency edges from two overlapping queries. Fixed with single SELECT DISTINCT query.
4. Bug 4: Ready and Graph endpoints never triggered PageRank computation. Fixed by adding EnsureRepoPageRankComputed() calls.

Verified Results

All three endpoints now return differentiated PageRank scores:

Issue	Title	PageRank
#3	Parser wrapper (CST-to-AST)	0.0800 (highest -- most depended on)
#1	Scaffold project	0.0625
#2	AST type definitions	0.0528
#4	Expression evaluator	0.0360
#5	Formatter	0.0360
#6	TLC bridge	0.0343
#7	CLI tool	0.0267
#8	Documentation/npm	0.0188 (lowest -- leaf node)

Issue #3 ranks highest because issues #4, #5, and #6 all depend on it. Issue #8 ranks lowest as a terminal leaf. This matches the dependency graph structure.

Commits

• Gitea fork: af94d42118 (graph_cache.go fix), 46ea68328c (ready_graph.go fix)
• Research: docs/src/research/pagerank-bug-investigation.md
• Design: docs/src/research/pagerank-bug-design.md