Skip to content

Release 2.1.0: sync Lauren's pstack to 519d36a (statechart compiler) - #54

Merged
chhoumann merged 5 commits into
mainfrom
sync/7c7bde7
Oct 27, 2026
Merged

chhoumann merged 5 commits into
mainfrom
sync/7c7bde7

Conversation

@chhoumann

@chhoumann chhoumann commented Oct 27, 2026 •

Copy link
Copy Markdown
Owner

Release 2.1.0. t3-pstack moves to Lauren Tan's pstack at cursor/plugins 519d36a from e73df47, for all three components. Only pstack changed upstream (0.15.32 to 0.15.34). This is a minor release because it replaces a skill's capability. Some of the old capabilities are replaced, and some are gone with nothing in their place (listed below). No install needs an action for the plugin to keep loading, such as rerunning the installer or editing the model sheet. A host whose only runtime is Node 20 or 21 does need Bun, Deno, or a newer Node to run statechart, which otherwise exits 127, and CHANGES says so. Both reviewers argued for 3.0.0 on that ground (Review, below). 2.1.0 is the version the maintainer asked for, and 3.0.0 stays open.

Upstream commits and what T3 needed

Upstream What it does T3 adaptation
#977 port the statechart compiler Replaces the statechart Node scripts with a TypeScript compiler. One command, <skill dir>/scripts/statechart SPEC.tla [--config FILE] [--view FILE] [--out DIR], checks the model with TLC, draws the Mermaid statechart, and writes report.md with the shortest path to each broken rule. A POSIX launcher runs statechart.ts with no build step on Node 22.18 to 22.x or 23.6+, else Bun 1.1.5+, else Deno 2.0+, and exits 127 when none is on PATH. A check killed by a signal exits 2, and only exits 0 and 1 write output. The reader's labels move into a --view module. references/render.md gives the Pele SVG steps and a theme. create-formal-verification-skill and poteto-help describe the skill as the compiler works. Upstream's CI moves the skill tests to Node 22 and installs fast-check for a differential test. No skill text changes. The new text names no Cursor mechanism, so no rule was added. <skill dir> resolves on both harnesses (end-to-end run below), and the launcher keeps mode 100755 through both installs. The CI job follows upstream, with one change. Upstream installs fast-check@4.5.3 with npm outside a lockfile, which fails this repo's pedantic zizmor gate (adhoc-packages). So the root package.json and bun.lock pin that version, and the job runs bun install --frozen-lockfile.
#978 version bump Upstream manifests. Excluded paths.

bun tools/sync.mjs added 396 files, deleted 26, and updated 3, with no merge, conflict, denylist hit, or fork touched. The statechart directory is byte-identical to upstream at 7c7bde7, file modes included. cursor-team-kit and thermos have no changes and move their pins. #977's README row, its guide page, and its copies under harness/pstack/claude-code/ sit outside every synced component.

Capabilities the compiler drops

Nothing in 2.1.0 replaces these:

  • from-chart, which turned a chart the reader agreed to into a TLA+ skeleton and compared the two, and render CHART.mmd, which drew such a chart.
  • --against and --against-config, which audited a model of the code against an existing spec.
  • --fixed and --fixed-config, which colored the states a proposed fix repairs. With --fixed or --against, the run also listed each action condition with no \* file:line citation.
  • --png and its --theme. references/render.md gives the steps for an SVG through Pele instead.
  • --cover, --expect-broken, the mapping file's readerActions, cause, and detail, and the stories.md and summary.json outputs.
  • The per-bug charts (bug-N.mmd, bug-N-developer.mmd, bug-N-layered.mmd) and the tlc/ folder with its regions proof (regions-all.mmd, regions-proof.mmd, compare-charts.mjs).

The skill also does not run on native Windows. The launcher is an sh script, and the compiler stops TLC's process group by spawning /bin/sh (statechart.ts:117, run.ts:97). This is read from the source, and no Windows host ran it. It is Lauren's platform choice, not a Cursor mechanic, so the port documents it in CHANGES rather than forking the TypeScript. A Windows fix belongs upstream.

CI

Skill script tests now runs on Node 22. It installs root dependencies with bun install --frozen-lockfile and runs node --disable-warning=ExperimentalWarning --test plugins/pstack/skills/*/scripts/test/*.test.ts. The old *.test.mjs glob matches nothing after this sync, and node --test exits 0 on a glob that matches nothing ("tests 0"). So the step sets bash's failglob, and an empty glob fails it. The new setup-bun step pins Bun 1.4.4, the version #52 moves the other jobs to for CVE-2026-111497, so this PR adds no new use of 1.3.14. Until #52 lands, this job runs a newer Bun than the others. CONTRIBUTING's dependency section now says to move the root fast-check pin when upstream's package.json moves it.

Commits

  1. Sync Lauren's pstack to 7c7bde7 (#977, #978). The three syncs, the CI job, the root fast-check pin, and the CONTRIBUTING sentence.
  2. Release 2.1.0: docs, notices, and manifests. VERSION, manifests, package.json, the CHANGES entry with its behavior-delta table, the NOTICE pins, and the README's pin and tag. The skill count stays at 66.
  3. Name statechart's Windows limit and dropped outputs, and pin the new job's Bun. Review round 1 fixes, below.

Verification

  • bun tools/generate.mjs --check passes.
  • GIT_CONFIG_GLOBAL=/dev/null bun test tests/ --timeout 30000 passes 550, skips 46, and fails 0.
  • The skill script tests as CI runs them (Node 22.23.4, no TLC, fast-check from the root node_modules) pass 262, skip 66, and fail 1 on macOS 27. With Node 24.22.1, TLC 1.7.4 (its checksum matches the pin), and Java 21, 360 of 361 pass. The one failure is the same test both times, "a SIGKILL of the command while the view draws the chart leaves no folder behind". After the SIGKILL it probes the killed process group once with kill(-pgid, 0) and expects ESRCH, macOS returned EPERM, and a copy of the test that keeps polling on EPERM passed 3 of 3 runs. CI runs on Linux.
  • The macOS runs need two environment settings that are not defects. TMPDIR must be the physical /private/var/... path, because the launcher symlink test builds a relative link from the logical /var path. npm must allow Pele 1.9.0, published 2026-10-22, past any min-release-age setting.
  • T3_PSTACK_E2E=1 GIT_CONFIG_GLOBAL=/dev/null bun test tests/install-e2e.test.mjs --timeout 300000 passes 9 and fails 3. The same 3 fail on unmodified origin/main on the same Mac with Codex CLI 0.164: "install reinstalls a plugin whose files are gone, and enables a disabled one", "doctor flags a plain copy of a plugin skill, not a user's own skill that shares a name", and "trusts nothing from a hooks file that is a symlink, even to the pinned text". This PR touches neither the installer nor the hooks.
  • uvx zizmor@1.29.0 --persona pedantic --min-severity low --collect all -- . reports no findings, and actionlint passes. shellcheck passes on the launcher.
  • bun tools/sync.mjs <component> 7c7bde7 --dry-run exits 0 for pstack, cursor-team-kit, and thermos.

Neither hooks file changes.

End to end on the installed plugin

The installer put this branch into a throwaway HOME from a clean clone (install --source <clone>): Claude Code 2.1.311 and Codex 0.164. Every check passed, with one warning for the missing model sheet. Both installed copies of skills/statechart match the clone byte for byte, with the launcher at mode 755 in .claude/plugins/cache/t3-pstack/t3-pstack/2.1.0/ and .codex/plugins/cache/t3-pstack/t3-pstack/2.1.0/. In that home, codex debug prompt-input lists the skill as r1/statechart/SKILL.md, where r1 is the installed plugin's skills folder, so <skill dir>/scripts/statechart names the installed launcher. Claude Code prints a skill's base directory when it loads the skill.

A two-rule door model in a scratch folder, run from each installed path with TLA2TOOLS set to TLC 1.7.4 and JAVA to Java 21:

  • The model whose YouOpen ignores the lock exits 1. report.md gives the two-step path to NeverOpenWhileLocked (Closed, "you turn the lock", Closed, locked, "you open the door", Open, locked), and lists TypeOK and NoDeadlock as holding. chart.mmd marks Open, locked as breaks and the path as bugPath.
  • The fixed model exits 0 with all three rules holding and a three-state chart.
  • On the broken model, the Claude Code copy, the Codex copy, and the Codex copy on a PATH with only Bun write the same chart.mmd and report.md. Their tlc.out differs only in TLC's seed, pid, and timestamps.
  • With no mise on PATH and no TLA2TOOLS, the command exits 2 with "Cannot find TLC: mise install failed: spawn mise ENOENT", says how to set TLA2TOOLS and JAVA, and writes no output folder.

Upstream after this pin

Upstream #982 (740d2c0) and #983 (0.15.34) landed after 7c7bde7 and are now in this PR (commit 858a898). Without #982, a broken property whose trace ran through an INSTANCE action lost its counterexample path: frontends/trace.ts read C!Up as C, so report.md said only "TLC found a counterexample" and the chart lost its bugPath and repeats marks (Astra reproduced this against 125c4ab). With it, upstream's new CounterInstance test passes locally, and the statechart folder is byte-identical to upstream at 164ced1. Then #981 (commit on top of 858a898) makes the SIGKILL view test wait for macOS to reap the killed group, which was the one macOS-only failure; pins move to 519d36a.

Review

Round 1 ran Fable 5.1 (xhigh) and GPT-6-Astra (xhigh) on the whole change. Neither found a critical issue, and both found zero mentions of the user's workplace.

  • Astra, high, and Fable, low. The skill needs /bin/sh, so it does not run on native Windows, which the installer and session hooks support. Resolved in CHANGES and above. The code is Lauren's, and the limit is a platform choice rather than a Cursor mechanic, so no fork.
  • Astra, medium, and Fable, medium. 2.1.0 should be 3.0.0, because capabilities are removed and a Node 20 host needs Bun or Deno for this skill. Not changed. The release follows the requested minor version and CONTRIBUTING's examples of a major release (an installer rerun, a sheet edit). CHANGES already names the Node 20 and 21 runtime need. This is open for the maintainer.
  • Fable, medium. Upstream #982 fixes qualified action names after the pin. Folded in afterwards (commit 858a898).
  • Fable, low. The dropped-capability list missed --theme, detail(), the per-bug charts, and the tlc/ folder. Added.
  • Fable, low. The new setup-bun step pinned 1.3.14 while Pin CI Bun to 1.4.4 for CVE-2026-111497 #52 moves CI to 1.4.4. Now 1.4.4.
  • Fable, low (a guess). "Show chart.mmd as a mermaid code block" assumes the chat renders Mermaid. It does. T3 Code's ChatMarkdown.tsx renders a mermaid block through MermaidDiagram (t3code 101f8b2). No change.
  • Fable, nit. The behavior table said "Node 22.18+", but the launcher refuses Node 23.0 to 23.5. Corrected to "Node 22.18 to 22.x or 23.6+".

Round 2 ran fresh Fable 5.1 (xhigh) and GPT-6-Astra (xhigh) delegates on the fix commit and the new PR body text. Neither found a critical or high issue, and both found zero mentions of the user's workplace. Both verified Bun 1.4.4 installs the root lockfile unchanged, and the generator, actionlint, Markdown lint, and zizmor checks pass.

  • Both, medium. The first paragraph said no install needs an action, which a Node 20 or 21 host without Bun or Deno contradicts for statechart. Reworded above.
  • Astra, low, and Fable, medium. The #982 impact was understated. The section above now describes the lost path and marks, from Astra's replay.
  • Fable, nit. CI's shellcheck job lints only *.sh, so it skips the extensionless launcher, which passes shellcheck when run by hand. That predates this PR, and the file is Lauren's, so no change.
  • Fable, nit. The README names only the installer's Node 20 floor. CHANGES carries the statechart runtime need and the Windows limit, as it does for TLC and mise. No change.

All three components move from e73df47 to 7c7bde7. Upstream changed only
pstack. statechart's scripts are replaced with Lauren's TypeScript
compiler (#977). One command, statechart SPEC.tla, checks a TLA+ model
with TLC, draws the Mermaid statechart, and reports the shortest path to
each rule that breaks. A POSIX launcher runs the TypeScript on Node
22.18+, Bun 1.1.5+, or Deno 2.0+ with no build step. A view module,
given with --view, holds the reader's labels. The chart-to-TLA+
skeleton (from-chart), the code audit against a spec (--against), the
fixed marks (--fixed), --png, --cover, and --expect-broken are gone, and
references/render.md says how to draw an SVG with Pele.
create-formal-verification-skill and poteto-help describe the skill as
the compiler works. #978 bumps upstream's manifests, an excluded path.

bun tools/sync.mjs added, deleted, or updated each file cleanly through
existing rules, with no denylist hit and no fork touched. The statechart
directory is byte-identical to upstream, and the launcher keeps mode
100755.

The Skill script tests job follows upstream's CI change. It runs on Node
22 and runs the *.test.ts files. Upstream installs fast-check@4.5.3 with
npm outside a lockfile, which fails zizmor's pedantic adhoc-packages
audit here, so the root package.json and bun.lock pin the version the
statechart scripts' package.json names, and the job runs bun install
--frozen-lockfile. The old *.test.mjs glob now matches nothing, and node
--test passes on zero files, so the step sets failglob. CONTRIBUTING's
dependency section says to move the root pin with upstream's.
VERSION, the manifests, and package.json move to 2.1.0, a minor release
because the statechart skill's capabilities change. CHANGES.md gets the
entry with the capabilities the compiler drops, its behavior-delta
table, the end-to-end install run, and the test runs at 7c7bde7.
NOTICE.md, NOTICE-skills.md, poteto-mode's copy of the notice, and the
README point at upstream 7c7bde7, and the README's pinned installer
command names the new tag. The skill count stays at 66.
@cursor

cursor Bot commented Oct 27, 2026

Copy link
Copy Markdown

This PR is too large for Bugbot to review. It changes 32,004 lines and 3,322,954 characters. Split the change into smaller pull requests to get a review.

…job's Bun

Review round 1. The 2.1.0 entry now says the skill does not run on
native Windows: the launcher is an sh script and the compiler stops
TLC's process group through /bin/sh. Its list of dropped capabilities
gains --theme, the mapping's detail(), the per-bug charts, and the tlc/
folder with the regions proof. The behavior table gives the launcher's
Node range as 22.18 to 22.x or 23.6+. The Skill script tests job's new
setup-bun step pins Bun 1.4.4 rather than adding one more use of 1.3.14.
Lauren's #982 landed after 7c7bde7: a broken temporal property's report
kept no path when an action came from an INSTANCEd module. pstack moves
to 0.15.34; the statechart folder stays byte-identical to upstream. The
2.1.0 CHANGES entry, notices, and README pin move to 164ced1.
@chhoumann chhoumann changed the title 2.1.0: Lauren's 7c7bde7, statechart becomes one command that checks a TLA+ model and charts it Release 2.1.0: sync Lauren's pstack to 164ced1 (statechart compiler) Oct 27, 2026
#981 makes the statechart SIGKILL view test wait for macOS to reap the
killed process group, the one test that failed on macOS. Test-only; the
statechart folder stays byte-identical to upstream.
@chhoumann chhoumann changed the title Release 2.1.0: sync Lauren's pstack to 164ced1 (statechart compiler) Release 2.1.0: sync Lauren's pstack to 519d36a (statechart compiler) Oct 27, 2026
@chhoumann
chhoumann merged commit 25f859b into main Oct 27, 2026
11 checks passed
@chhoumann
chhoumann deleted the sync/7c7bde7 branch October 27, 2026 06:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant