Repository navigation
Release 2.1.0: sync Lauren's pstack to 519d36a (statechart compiler) - #54
Merged
Merged
Conversation
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.
|
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.
#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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Release 2.1.0. t3-pstack moves to Lauren Tan's pstack at cursor/plugins
519d36afrome73df47, 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 runstatechart, 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
<skill dir>/scripts/statechart SPEC.tla [--config FILE] [--view FILE] [--out DIR], checks the model with TLC, draws the Mermaid statechart, and writesreport.mdwith the shortest path to each broken rule. A POSIX launcher runsstatechart.tswith 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 onPATH. A check killed by a signal exits 2, and only exits 0 and 1 write output. The reader's labels move into a--viewmodule.references/render.mdgives the Pele SVG steps and a theme.create-formal-verification-skilland 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.<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 installsfast-check@4.5.3with npm outside a lockfile, which fails this repo's pedantic zizmor gate (adhoc-packages). So the rootpackage.jsonandbun.lockpin that version, and the job runsbun install --frozen-lockfile.bun tools/sync.mjsadded 396 files, deleted 26, and updated 3, with no merge, conflict, denylist hit, or fork touched. Thestatechartdirectory is byte-identical to upstream at7c7bde7, 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 underharness/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, andrender CHART.mmd, which drew such a chart.--againstand--against-config, which audited a model of the code against an existing spec.--fixedand--fixed-config, which colored the states a proposed fix repairs. With--fixedor--against, the run also listed each action condition with no\* file:linecitation.--pngand its--theme.references/render.mdgives the steps for an SVG through Pele instead.--cover,--expect-broken, the mapping file'sreaderActions,cause, anddetail, and thestories.mdandsummary.jsonoutputs.bug-N.mmd,bug-N-developer.mmd,bug-N-layered.mmd) and thetlc/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
shscript, 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-lockfileand runsnode --disable-warning=ExperimentalWarning --test plugins/pstack/skills/*/scripts/test/*.test.ts. The old*.test.mjsglob matches nothing after this sync, andnode --testexits 0 on a glob that matches nothing ("tests 0"). So the step sets bash'sfailglob, and an empty glob fails it. The newsetup-bunstep 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'spackage.jsonmoves it.Commits
Sync Lauren's pstack to 7c7bde7 (#977, #978). The three syncs, the CI job, the root fast-check pin, and the CONTRIBUTING sentence.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.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 --checkpasses.GIT_CONFIG_GLOBAL=/dev/null bun test tests/ --timeout 30000passes 550, skips 46, and fails 0.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 withkill(-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.TMPDIRmust be the physical/private/var/...path, because the launcher symlink test builds a relative link from the logical/varpath. npm must allow Pele 1.9.0, published 2026-10-22, past anymin-release-agesetting.T3_PSTACK_E2E=1 GIT_CONFIG_GLOBAL=/dev/null bun test tests/install-e2e.test.mjs --timeout 300000passes 9 and fails 3. The same 3 fail on unmodifiedorigin/mainon 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, andactionlintpasses. shellcheck passes on the launcher.bun tools/sync.mjs <component> 7c7bde7 --dry-runexits 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
HOMEfrom 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 ofskills/statechartmatch 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-inputlists the skill asr1/statechart/SKILL.md, wherer1is the installed plugin'sskillsfolder, so<skill dir>/scripts/statechartnames 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
TLA2TOOLSset to TLC 1.7.4 andJAVAto Java 21:YouOpenignores the lock exits 1.report.mdgives the two-step path toNeverOpenWhileLocked(Closed, "you turn the lock", Closed, locked, "you open the door", Open, locked), and listsTypeOKandNoDeadlockas holding.chart.mmdmarksOpen, lockedasbreaksand the path asbugPath.PATHwith only Bun write the samechart.mmdandreport.md. Theirtlc.outdiffers only in TLC's seed, pid, and timestamps.PATHand noTLA2TOOLS, the command exits 2 with "Cannot find TLC: mise install failed: spawn mise ENOENT", says how to setTLA2TOOLSandJAVA, and writes no output folder.Upstream after this pin
Upstream #982 (
740d2c0) and #983 (0.15.34) landed after7c7bde7and are now in this PR (commit858a898). Without #982, a broken property whose trace ran through an INSTANCE action lost its counterexample path:frontends/trace.tsreadC!UpasC, soreport.mdsaid only "TLC found a counterexample" and the chart lost itsbugPathandrepeatsmarks (Astra reproduced this against125c4ab). With it, upstream's newCounterInstancetest passes locally, and thestatechartfolder is byte-identical to upstream at164ced1. Then #981 (commit on top of858a898) makes the SIGKILL view test wait for macOS to reap the killed group, which was the one macOS-only failure; pins move to519d36a.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.
/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.858a898).--theme,detail(), the per-bug charts, and thetlc/folder. Added.setup-bunstep 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.chart.mmdas amermaidcode block" assumes the chat renders Mermaid. It does. T3 Code'sChatMarkdown.tsxrenders amermaidblock throughMermaidDiagram(t3code101f8b2). No change.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.
statechart. Reworded above.*.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.