Repository navigation
port pstack 0.15.32 (#791 through #807) - #26
Merged
Merged
Conversation
Port the upstream pstack commits since 4ec7ffa1. cursor-team-kit stays 1.2.0. Co-authored-by: Kaitian Xie <caelaxie@users.noreply.github.com>
caelaxie
commented
Oct 24, 2026
caelaxie
left a comment
caelaxie
left a comment
Contributor
Author
There was a problem hiding this comment.
changes requested (comment review, since author = reviewer account).
checked at head 3d70ed2 against upstream e73df471:
- minimum changes:
skills/statechart,ketchup-video,poteto-mode/scripts/watch-pr,poteto-mode/scripts/orch,check-plan.mjs+ test, andcreate-formal-verification-skill/SKILL.mdare git-sha identical to upstream. readme, guide, and poteto-help rows match upstream text. reflect (#800) swaps onlyplugins/cache/and.cursor/skills/for the grok paths, swarm (#807) and worktree-audit (#805) apply the upstream hunks on the existing grok wording. ok. - layout/target: no
.cursor/paths added. ok. - parity: no upstream skill file missing from the port;
plugin.jsonat 0.15.32, kit 1.2.0. ok. - ci:
Validate plugingreen. ok. - linkage: no open issue to close. ok.
blocking:
- harness proof missing. this pr adds a skill and ships new statechart scripts, so it needs the real grok run on this exact head:
grok plugin install --trustfrom3d70ed2(or whatever head you land), thengrok plugin list/ validate showing pstack 0.15.32, plus evidenceketchup-videoand the newstatechart/scripts/*are in the installed copy. post it as a pr comment or in the body and i'll re-review.
Contributor
Author
|
Harness proof for head Grok CLI installed the same way
A headless model turn against that install exited 1, blocked on auth: |
caelaxie
commented
Oct 24, 2026
|
harness proof for head
installed script tests: watch-pr, orch, and check-plan, 82 pass, 0 fail. statechart from the installed copy: 150 tests, 147 pass, 0 fail, 3 skipped (no mise, so the real-mise test skips; no Type 1 font and no Nimbus Sans). tla2tools 1.7.4 at The command transcript below is the installed copy at that head, before statechart result from the same installed run: |
|
statechart tests from the installed copy at result: 150 tests, 147 pass, 0 fail, 3 skipped. skipped:
every other test passed, including the TLC from-spec and from-chart runs. duration 357183 ms. the line-by-line TAP is 150 |
|
installed text of the changed and new skills, from
full installed text: skills/ketchup-video/SKILL.md---
name: ketchup-video
description: "Catch the user up like /ketchup, with a short silent video of slides for what happened and the waiting calls as text under it. Use for /ketchup-video."
disable-model-invocation: true
---
# Ketchup video
Follow [`/ketchup`](../ketchup/SKILL.md), but show what happened in a short silent video instead of its summary and visuals. Its window starts at the last message the user wrote before `/ketchup-video`, not before any earlier `/ketchup`. Writing and rendering the video, outside the repo, is the one exception to its read-only rule. The reply is ketchup's opening sentence, the embedded video, one line naming any work left that you can do yourself, and the action items. When the video shows a call's options, call each option by the name the video gives it. If the render fails, say so in one line and give only the calls.
## Slides
Use the screenshots, recordings, diffs, and data the work produced, not the chat's prose about them. Before you draw, write the one sentence the user should leave with and one line per slide. Drop each slide that does not change what the user knows. Use at most 10 slides, and fewer is better. Neither note goes in the reply.
Each slide makes one point. Build the slides on one picture and change it from slide to slide, rather than cut to an unrelated one. A color or shape means the same thing on every slide. Show the work in pictures, such as how a system works, a PR stack with each PR's state, a before and after of a fix, or options side by side. Point at what changed with arrows, highlights, and motion. A slide is never a bullet list, a status list, a table, or boxes with nothing connecting them.
Keep text to the minimum. Put each label on the thing it names, in plain words a person would say, not tags like "Tests: pass". Never caption what a picture shows, and never give a fact twice, across slides or in the text under them.
Show what came of each thing the user asked for, and whether it is done, still running, failed, or not checked. Never show something done that still waits on the user. Show any bug found and fixed on the way. If a visible change has no screenshot, say so on its slide and name what changed on screen. Draw only from facts you have. Never invent a number, and never draw a screen you did not capture.
## Render
Render one silent landscape video, such as an mp4, with motion between slides. Every frame is the slide itself, edge to edge. Make the frames from the slides, never by recording a screen. Hold each slide long enough to read its words, at least one second for each three words it adds. Words inside a screenshot do not count. Before you embed the video, look at one frame from each slide in the rendered file, and count the words it adds against its hold in that file. Fix any slide you cannot read in that time, render again, and check again.skills/statechart/SKILL.mdThe installed file is the upstream skill at ---
name: statechart
description: "Draw how any system moves between states, such as a product flow, a protocol, or a service, as a Mermaid statechart from a TLA+ model. Each bug is a numbered path with blue borders to a state that breaks a rule. Use for /statechart, to show a bug as a path through states, or to turn an agreed chart into a TLA+ skeleton."
disable-model-invocation: true
---
# Statechart
The chart shows how a system moves between states, in the words of the person who reads it. The scripts call that person the reader, as in `readerActions` and reader steps. The reader decides whether the behavior is right. The reader can be a PM who reads a product flow, an engineer who reads a protocol or a service, or a reviewer who reads a design. Label each state with what the reader can observe or cares about, such as "Paying" in an app or "Lease held, write pending" in a lock service. Label each step with the event that moves the system, such as "tap Pay" in an app, "the request reads the count" in a service, or "the lease expires" in a lock service. Keep variable and action names out of labels.
Run `node <skill dir>/scripts/statechart.mjs --help` for the commands and for how to read a chart. Work in a scratch folder outside the repo. The command writes its files next to its input. The first run installs TLC and Java with mise, which downloads about 305 MB and needs the network. The help's TLC section tells how to use a TLC and Java that you have.
skills/reflect/SKILL.mdthe new apply paragraph, from the installed file: Never edit a skill under `installed-plugins/`. Before approval, show its destination, `.grok/skills/<skill>/` or `~/.grok/skills/<skill>/`. After approval, copy the skill folder there and edit the copy. Never open a PR or push.skills/swarm/SKILL.mdinstalled phase A and the report line: 1. State the done predicate and the artifact or report the swarm must return.
2. Choose the shape. Partition into slices, race N workers on identical briefs, or mix both. For a race or mixed shape, declare `first pass`, `rank all`, or `best-of` before spawning.
3. Pick the worker model from the `swarm workers` line in `~/.grok/rules/pstack-models.md`. If the rule or that line is missing, use `grok-4.6` at `xhigh`. For `auto` or `inherit-parent`, omit `model` so the workers run on the parent model. If `spawn_subagent` has no `model` argument, omit it for this session so the child inherits the parent, and apply step 1 of **setup-pstack** so the next session can pass `model`. If it rejects a slug, use the closest slug from `grok models` and say so. For a model race, name each arm's model up front. Pick each subagent's reasoning effort for the job, per the Subagents section.
4. Give each worker its own writable output when it writes. When workers verify or measure commits, each brief names the exact SHAs. A measurement brief also names the method (sample count, what one sample is, order). The worker records both in its result.fan-out uses skills/poteto-help/SKILL.mdinstalled row: | Catch up like `/ketchup`, in a short silent video of slides, with the waiting calls as text under it | [`/ketchup-video`](../ketchup-video/SKILL.md) |skills/create-formal-verification-skill/SKILL.mdinstalled paragraph: If the check is a TLA+ model, tell the next agent to read every result with the pstack [`/statechart`](../statechart/SKILL.md) skill. It shows each invariant violation the checker finds as its shortest path in plain words, and which of those violations a change fixes. When the check passes, `/statechart` draws a chart of how the system moves between states. Refer to `/statechart` by name. Its commands, options, and file paths change between releases and machines, so copy none of them into the generated skill or its scripts. |
|
full installed skill files from
skills/statechart/SKILL.md---
name: statechart
description: "Draw how any system moves between states, such as a product flow, a protocol, or a service, as a Mermaid statechart from a TLA+ model. Each bug is a numbered path with blue borders to a state that breaks a rule. Use for /statechart, to show a bug as a path through states, or to turn an agreed chart into a TLA+ skeleton."
disable-model-invocation: true
---
# Statechart
The chart shows how a system moves between states, in the words of the person who reads it. The scripts call that person the reader, as in `readerActions` and reader steps. The reader decides whether the behavior is right. The reader can be a PM who reads a product flow, an engineer who reads a protocol or a service, or a reviewer who reads a design. Label each state with what the reader can observe or cares about, such as "Paying" in an app or "Lease held, write pending" in a lock service. Label each step with the event that moves the system, such as "tap Pay" in an app, "the request reads the count" in a service, or "the lease expires" in a lock service. Keep variable and action names out of labels.
Run `node <skill dir>/scripts/statechart.mjs --help` for the commands and for how to read a chart. Work in a scratch folder outside the repo. The command writes its files next to its input. The first run installs TLC and Java with mise, which downloads about 305 MB and needs the network. The help's TLC section tells how to use a TLC and Java that you have.
## Pick the direction
Use `from-spec` when a TLA+ model exists, or when the code or design is concrete enough to model. Use `from-chart` when there is no model, and the people who own the behavior should agree on it before anyone builds or changes it.
If the code already has a TLA+ spec, start from a copy of that spec. Add the variables that the labels and rules need, and keep the spec's existing invariants. To audit the code against that spec, make the copy model what the code does, and pass the spec unchanged as `--against`. Check it with the config that its authors say it passes, and pass that config as `--against-config` unless it has the spec's file name. One mapping labels both models, so label states and steps from variables that both have. A label that reads a variable that only the copy has must test `"name" in v` first, and label the spec's states another way. When a model describes code, tie every variable and action to code that a reviewer can open, and take its name from that code. Make each action one indivisible step in the code. Put the file and line of the code that checks each condition of an action in a comment on that condition, as in `\* pay.ts:120`.
## Spec to chart
1. Choose the chart's states. When the reader cares about something that a label would hide, put it in the label, such as "Paying, charged twice" when the screen still says "Paying" after a second charge. Start with few states. Split a state when the split separates two bugs, or when the reader must see a step that leaves the label the same, such as a request that reads a count, because the chart does not draw such a step.
2. Write each rule that the reader agrees to as one invariant, with the reader's sentence as its comment. A rule can be about any state in the model: what a screen shows, what a request returns, a stored value, or a message between parts. When the model describes code, the rule also names the code that can change that state. If the model has no variable for what a rule is about, add the variable. Do not drop the rule. For a rule that applies once everything settles, define `Settled == ~ENABLED System`, where `System` is the disjunction of the actions that happen without the reader. For a rule that applies at a narrower point, such as after each request finishes, write a predicate for that point and make the rule hold where it is true. For a goal that the system must be able to reach, write a rule that says the goal never happens, and pass that rule with `--expect-broken`. The path that breaks it is then a way to the goal. The chart still draws the goal as a state that breaks a rule, and `stories.md` tells it as a bug, so name each goal rule in the hand-off. Report each other broken rule as a bug. Never weaken a rule to make the chart pass.
3. Run `from-spec`, then fill in the mapping file it writes. Put the labels in `state` and `step`. When the chart must separate what the reader does from what happens around the reader, list the reader's actions in `readerActions` by action name. Leave the list empty when every action counts the same. When the overview is too large to read, add `--cover`. The overview then keeps only the shortest path to each settled state, plus every bug path, and the command lists what it leaves out. When two bugs end in the same state for different reasons, add `cause` and make it name each reason. To color the states by what the reader cares about, such as "Order shipped", return that group from `group`. The legend names the groups, and in the PNG a state that breaks a rule is red in place of its group color.
4. If there is a proposed fix, model it and pass that model as `--fixed`.
5. Render each chart with `--png` and look at every PNG. Check that each numbered path reads in order. If a label reads like code, fix `state` or `step` and run the command again.
6. When the model describes code, replay each bug's story against the real code, as a test or a live repro, one step per model action. Drive only entry points that a user, a client, or another part of the system reaches, and assert only what they can observe. A test that asserts a flag that it sets, or that searches the source text, proves nothing. When a run proves part of the story and reading the code proves the rest, say which part each proves. When the test copies code that it cannot import, give the commit and line range of the copy, and list what the copy leaves out. If a bug does not reproduce, assume the model is wrong until you show otherwise. Fix the model, not the rule. For a design with no code yet, the TLC trace is the evidence, and the hand-off must say so.
## Chart to spec
1. Draw the chart that the reader agrees to. Use one region for each part that changes independently, such as a device's connection and the job that the device runs. Add one `%% never` line per rule, with the reader's sentence. Draw an event that stops or restarts a part, such as "the app closes" or "the process restarts", as an edge to the state that comes next. Run `render CHART.mmd` to get a PNG of the chart for the reader.
2. Run `from-chart`. If a rule breaks, the agreed chart has a design bug. Take the bug to the people who agreed to the chart.
3. Add the real code's guards and variables to the spec that `from-chart` wrote, and run `from-chart` again. For each difference it prints, ask the reader whether the code is wrong or the chart needs a correction.
## Hand off
Give the PNG and the Mermaid source of each chart to the person who must decide. Add one line per bug with the rule it breaks, its steps as the chart numbers them, whether it reproduced, and whether the proposed fix fixes it. A broken PROPERTY has no path on the chart, so give the TLC counterexample that `stories.md` names for it. With `--against`, also say whether the spec already lists it: in the configs that `stories.md` names, in the spec's notes on what the model leaves out, or not at all. When the model describes code, do not report that a rule holds while the command lists conditions with no file and line. Take every count you quote from `summary.json`. Attach `stories.md` and the command that regenerates everything. Say what the model leaves out. |
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.
port upstream pstack from
4ec7ffa1(#779) throughe73df471(#807). version goes from 0.15.30 to 0.15.32. cursor-team-kit stays 1.2.0.upstream commits on
pstack/:076f4b2ffeat(pstack): bring the statechart skill up to date, with the Pele renderer (#791)642289e6chore(pstack): bump to 0.15.31 (#792)00d5deccfeat(pstack): tell generated verify skills to read each model-check result with /statechart (#794)3c0fdb4efeat(pstack): add the ketchup-video skill (#797)b1a12989chore(pstack): bump to 0.15.32 (#798)7054003cfix(pstack): route reflect edits out of the plugin cache (#800)96dec8eefix(watch-pr): distinguish fork heads during stack discovery (#801)fe096ef3fix(watch-pr): cap polling sleeps at the deadline (#802)86c2448dfix(pstack): recognize matching inline code delimiters (#803)3c596e70fix(orch): prefer active PR over branch history (#804)f83fbe69fix(pstack): read transcript mtimes with GNU stat and date in worktree-audit (#805)a0b0ad99docs(pstack): note Claude Code auto-update is off for third-party marketplaces (#806)e73df471fix(pstack): renumber swarm's Phase A and fix its dangling table reference (#807)cursor-team-kit/has no commits in this range. kit stays 1.2.0. commits outsidepstack/were not ported.grok-only:
plugin.json. this port has no.cursor-plugin/plugin.json. the #792 and #798 bumps land as 0.15.32 there.e73df471cd4bd918367e99f3dd9c51bd53ddf5f0for pstack and for cursor-team-kit.installed-plugins/, and to copy into.grok/skills/<skill>/or~/.grok/skills/<skill>/. upstream saysplugins/cache/,.cursor/skills/, and~/.cursor/skills/.stat/datefix sits on the existing grok transcript path.harness, grok 1.0.67, head
3d70ed216c75c67959e5668b3e03e1abdb61b71e. installed fromhttps://github.com/pstack-ports/grok-pstack@cursor/port-pstack-0.15.32-cef8.grok plugin listshows pstack 0.15.32. installedHEADis that commit.grok inspectloadsketchup-video,statechart,reflect,swarm,poteto-help, andcreate-formal-verification-skill(userInvocable: true), 61 skills. installed watch-pr, orch, and check-plan tests: 82 pass, 0 fail. installed statechart tests: 147 pass, 0 fail, 3 skipped (no mise, no Type 1 font, no Nimbus Sans), tla2tools 1.7.4. local ci: validated 61 skills, 2 agents, 23 playbooks, and 82 script tests. github ci: https://github.com/pstack-ports/grok-pstack/actions/runs/40049656350full command output: #26 (comment)
statechart result from that installed copy: #26 (comment)
installed text of the changed and new skills: #26 (comment)
installed
skills/statechart/SKILL.mdin full: #26 (comment)