port upstream pstack through 0.15.32 by caelaxie · Pull Request #27 · pstack-ports/devin-pstack

caelaxie · 2026-10-24T01:32:04Z

synced to e73df47. compared 4ec7ffa..e73df47 for pstack/. origin/main is that commit. version is 0.15.32 in plugin.json, .devin-plugin/plugin.json, and the readme marker.

ported:

076f4b2 (#791) statechart skill update and the pele renderer. scripts copied verbatim, including the removal of the outputfolder model. SKILL.md keeps /pstack:statechart and triggers: [user].
642289e (#792) bump to 0.15.31, folded into the 0.15.32 bump in plugin.json and .devin-plugin/plugin.json.
00d5dec (#794) generated verify skills read each model-check result with /pstack:statechart.
3c0fdb4 (#797) add the ketchup-video skill. poteto-help, the readme skill table, and guide page 10 match. slash commands keep the /pstack: prefix. disable-model-invocation: true stays triggers: [user].
b1a1298 (#798) bump to 0.15.32, in plugin.json, .devin-plugin/plugin.json, and the readme marker.
7054003 (#800) reflect edits leave plugins/cache/ (devin's checkout is ~/.local/share/devin/cli/plugins/cache). the destination is .devin/skills/<skill>/ or ~/.config/devin/skills/<skill>/. no pr and no push.
96dec8e (#801) watch-pr distinguishes fork heads. the pstack scripts were copied verbatim.
fe096ef (#802) watch-pr caps polling sleeps at the deadline. scripts copied verbatim.
86c2448 (#803) check-plan recognizes matching inline code delimiters. scripts copied verbatim.
3c596e7 (#804) orch prefers the active pr. the changed files are under pstack/skills/poteto-mode/scripts/orch/ and were copied verbatim.
f83fbe6 (#805) worktree-audit reads transcript mtimes with gnu stat and date. kept rg -a and the devin sessions.db directory.
e73df47 (#807) swarm phase a is numbered 1 to 4, phase b points at step 3, and phase d asks for a result table.

skipped:

a0b0ad9 (#806) claude code auto-update note. it sits in the claude code install section, and this readme has no such section.
harness/pstack/claude-code/ copies in every commit above. this port does not carry the generated claude code tree.
#792 and #798 pstack/.cursor-plugin/plugin.json. cursor packaging. the version bump lands in .devin-plugin/plugin.json instead.

harness proof (devin plugins install, devin plugins list, /pstack:statechart, /pstack:ketchup-video, /pstack:poteto-mode) will follow as a comment. the devin cli can't log in from this cloud environment.

sync pstack/ from cursor/plugins 4ec7ffa..e73df47. keep the devin path, slash-command, and worktree-audit adaptations already in this repo. Co-authored-by: Kaitian Xie <caelaxie@users.noreply.github.com>

caelaxie

changes requested (posted as comment, same account authors and reviews).

blocking: no harness proof yet. the body says devin proof "will follow as a comment", and nothing is on the pr. this pr touches skill content and scripts (statechart rewrite, new ketchup-video, watch-pr, orch, check-plan, worktree-audit), so green ci alone isn't enough.

need on head 1c35735:

devin plugins install pinned to the full head sha (the --local wrapper that lets devin fetch the repo itself is fine; symlink-only proofs aren't)
devin plugins list showing pstack 0.15.32
installed copy showing skills/ketchup-video/SKILL.md and the new skills/statechart/scripts/*.mjs, and OutputFolder.* gone
a live /pstack:statechart or /pstack:ketchup-video turn if devin auth allows; if auth blocks it, say so and the install+list+installed-copy proof is accepted for these changes

non-blocking: the skipped list (claude code tree, #806 readme note, .cursor-plugin/plugin.json) reads right. no issue linkage needed unless this fixes an open issue; if it does, add Closes #N.

ping me when the proof comment lands and i'll re-review.

caelaxie · 2026-10-24T02:01:25Z

harness proof

Real Devin CLI on a local box (no cloud agent, no git clone). PR head 1c35735b02729e5f9409bdbcea841fd5c810a18d, which I checked with git ls-remote refs/pull/27/head before installing and again before cleanup. Expected version: 0.15.32 (upstream through e73df47: ketchup-video, new statechart scripts, OutputFolder.* removed).

CLI: devin 3000.11.92 (7f4e64980e22), devin auth status → Logged in (via Devin). The CLI updated itself to 3000.11.205 (6dea39440ae3) at 09:54 UTC+8, partway through the run. Steps 1–7 ran on 3000.11.92. The live turn (step 8) and cleanup ran on 3000.11.205.
Everything was read-only. The live turn ran in a scratch dir whose allowlist only permits reads (Write(**)/Edit(**) denied), with the default auto permission mode. I added no allowlist entries. The one setup change was answering the CLI's first-run "trust this directory?" prompt for the scratch dir, which -p requires.

#	step	result
1	`devin plugins list` before: only `thermos v1.0.0`	✅ recorded
2	`--local` wrapper pinned to the full head sha (no symlinks)	✅ PASS
3	`devin plugins list` shows `pstack v0.15.32 (required)`, and both plugin.json files say 0.15.32	✅ PASS
4	`skills/ketchup-video/SKILL.md` is a regular file and byte-identical to head (`cmp`)	✅ PASS
5	all 27 files under `skills/statechart/` (SKILL.md + 21 `scripts/.mjs` + 5 `scripts/test/`) are byte-identical to head	✅ PASS
6	`skills/statechart/scripts/model/OutputFolder.*` is gone (and so is `model/`). No symlinks. The installed file list matches the head tree exactly (200 = 200, no diff)	✅ PASS
7	CLI lists statechart, ketchup-video, create-formal-verification-skill, reflect, swarm, poteto-help, and poteto-mode from the 0.15.32 cache. poteto-help links ketchup-video. worktree-audit.sh has `rg -l -a`, and its only `stat -f` is a comment plus the BSD branch behind a GNU check	✅ PASS
8	live `devin -p` turn invoking `/pstack:statechart` (describe-only)	✅ PASS
9	head sha unchanged at the end. Wrapper and pstack removed, thermos left	✅ PASS

1–3. before list, install, after list

$ devin plugins list          # before
Installed plugins

  • thermos v1.0.0

$ cat /workspace/devin-harness/wrap-pr27/.devin-plugin/plugin.json
{ "name": "pstack-harness-pr27", "version": "0.0.0",
  "requiredPlugins": [ { "source": "github", "repo": "pstack-ports/devin-pstack",
                         "sha": "1c35735b02729e5f9409bdbcea841fd5c810a18d" } ] }
$ find wrap-pr27
wrap-pr27
wrap-pr27/.devin-plugin
wrap-pr27/.devin-plugin/plugin.json
wrap-pr27/skills
$ devin plugins install --local -y /workspace/devin-harness/wrap-pr27
This install will add:
  • pstack-harness-pr27 v0.0.0
  • pstack v0.15.32 (required)
      ...
      /pstack:create-formal-verification-skill
      /pstack:statechart
      ...
      /pstack:reflect
      ...
      /pstack:poteto-mode
      ...
      /pstack:poteto-help
      ...
      /pstack:ketchup-video
      ...
      /pstack:swarm
      ...
✓ Installed pstack-harness-pr27.
  auto-installed required plugins: pstack
$ devin plugins list
Installed plugins

  • thermos v1.0.0
  • pstack-harness-pr27 v0.0.0
  • pstack v0.15.32 (required)

3–6. installed cache copy

$ cd ~/.local/share/devin/cli/plugins/cache/github.com_pstack-ports_devin-pstack-816793bb/0.15.32
$ grep -n '"version"' .devin-plugin/plugin.json plugin.json
.devin-plugin/plugin.json:3:  "version": "0.15.32",
plugin.json:4:  "version": "0.15.32",
$ stat -c '%F %s %n' skills/ketchup-video/SKILL.md
regular file 2901 skills/ketchup-video/SKILL.md
$ find skills/statechart -type f | sort
skills/statechart/SKILL.md
skills/statechart/scripts/bug-states.mjs
skills/statechart/scripts/chart-edges.mjs
skills/statechart/scripts/chart-parts.mjs
skills/statechart/scripts/chart-to-tla.mjs
skills/statechart/scripts/compare-charts.mjs
skills/statechart/scripts/lib.mjs
skills/statechart/scripts/map-view.mjs
skills/statechart/scripts/property-loop.mjs
skills/statechart/scripts/read-check.mjs
skills/statechart/scripts/regions-chart.mjs
skills/statechart/scripts/render.mjs
skills/statechart/scripts/rule-book.mjs
skills/statechart/scripts/second-replay.mjs
skills/statechart/scripts/snapshot.mjs
skills/statechart/scripts/spec-text.mjs
skills/statechart/scripts/statechart-help.mjs
skills/statechart/scripts/statechart.mjs
skills/statechart/scripts/test/band.mmd
skills/statechart/scripts/test/regions.mmd
skills/statechart/scripts/test/statechart.test.mjs
skills/statechart/scripts/test/sync.mmd
skills/statechart/scripts/test/upload.mmd
skills/statechart/scripts/tlc-to-chart-args.mjs
skills/statechart/scripts/tlc-to-chart.mjs
skills/statechart/scripts/tlc-tools.mjs
skills/statechart/scripts/ways-in.mjs
$ for f in skills/ketchup-video/SKILL.md $(find skills/statechart -type f | sort); do
    curl -fsSL https://raw.githubusercontent.com/pstack-ports/devin-pstack/1c35735b02729e5f9409bdbcea841fd5c810a18d/$f -o /tmp/pr27/$f &&
    cmp -s $f /tmp/pr27/$f && echo "IDENTICAL $f" || echo "DIFF/ERR $f"; done
IDENTICAL skills/ketchup-video/SKILL.md
IDENTICAL skills/statechart/SKILL.md
IDENTICAL skills/statechart/scripts/bug-states.mjs
IDENTICAL skills/statechart/scripts/chart-edges.mjs
...                                  # every one of the 28 files: IDENTICAL, zero DIFF/ERR
IDENTICAL skills/statechart/scripts/tlc-tools.mjs
IDENTICAL skills/statechart/scripts/ways-in.mjs
$ find skills/statechart -name 'OutputFolder*'
$ test ! -e skills/statechart/scripts/model/OutputFolder.tla && echo GONE
GONE
$ ls skills/statechart/scripts/model
ls: cannot access 'skills/statechart/scripts/model': No such file or directory
$ find . -type l | wc -l
0
$ curl -fsSL "https://api.github.com/repos/pstack-ports/devin-pstack/git/trees/1c35735b02729e5f9409bdbcea841fd5c810a18d?recursive=1"   # blobs -> head.txt
truncated False
symlinks/submodules in tree: []
$ find . -type f | sed 's|^\./||' | sort > inst.txt; wc -l head.txt inst.txt
  200 head.txt
  200 inst.txt
$ comm -3 head.txt inst.txt      # only-in-head / only-installed
(empty)

Devin installed every blob in the head tree and added nothing, so I didn't have to exclude any paths.

7. skills from the 0.15.32 cache + spot checks

$ devin skills list | grep -E '/pstack:(statechart|ketchup-video|poteto-mode|create-formal-verification-skill|reflect|swarm|poteto-help) '
  /pstack:create-formal-verification-skill [user] (~/.local/share/devin/cli/plugins/cache/github.com_pstack-ports_devin-pstack-816793bb/0.15.32/skills/create-formal-verification-skill) - Generate a project-local skill th...
  /pstack:statechart [user] (~/.local/share/devin/cli/plugins/cache/github.com_pstack-ports_devin-pstack-816793bb/0.15.32/skills/statechart) - Draw how any system moves between states, such as a product flow, a protocol, ...
  /pstack:reflect [user] (~/.local/share/devin/cli/plugins/cache/github.com_pstack-ports_devin-pstack-816793bb/0.15.32/skills/reflect) - Spawn three parallel review subagents over the active transcript, surface learnings ...
  /pstack:poteto-mode [user] (~/.local/share/devin/cli/plugins/cache/github.com_pstack-ports_devin-pstack-816793bb/0.15.32/skills/poteto-mode) - poteto's agent style for concise, detailed responses, deliberate subagents, ...
  /pstack:poteto-help [user] (~/.local/share/devin/cli/plugins/cache/github.com_pstack-ports_devin-pstack-816793bb/0.15.32/skills/poteto-help) - Guides users through pstack setup, /pstack:poteto-mode, and picking the ski...
  /pstack:ketchup-video [user] (~/.local/share/devin/cli/plugins/cache/github.com_pstack-ports_devin-pstack-816793bb/0.15.32/skills/ketchup-video) - Catch the user up like /pstack:ketchup, with a short silent video of sl...
  /pstack:swarm [user] (~/.local/share/devin/cli/plugins/cache/github.com_pstack-ports_devin-pstack-816793bb/0.15.32/skills/swarm) - Fan out N parallel workers, drain them, and return one report. Use for /pstack:swarm, '...
$ grep -n ketchup-video skills/poteto-help/SKILL.md
72:| Catch up like `/pstack:ketchup`, in a short silent video of slides, with the waiting calls as text under it | [`/pstack:ketchup-video`](../ketchup-video/SKILL.md) |
$ grep -n 'rg -l -a' skills/poteto-mode/scripts/worktree-audit.sh
115:		f=$(rg -l -a -e "${wt}/" -e "${wt}\"" "$transcripts" 2>/dev/null \
$ grep -n -A5 'stat -f' skills/poteto-mode/scripts/worktree-audit.sh
50:# GNU coreutils (Linux, Homebrew gnubin) reads `stat -f` as file system status
51-# and `date -r` as a file, so pick the stat and date flags once.
52-if stat -c %Y / >/dev/null 2>&1; then
53-	stat_fmt=(-c '%Y %n'); fmt_day() { date -d "@$1" '+%Y-%m-%d'; }
54-else
55-	stat_fmt=(-f '%m %N'); fmt_day() { date -r "$1" '+%Y-%m-%d'; }
$ curl -fsSL .../1c35735b.../skills/poteto-mode/scripts/worktree-audit.sh | cmp - skills/poteto-mode/scripts/worktree-audit.sh && echo IDENTICAL
IDENTICAL

The script never calls stat -f unconditionally. The literal appears only in the line-50 comment. BSD -f is the else branch of a stat -c probe, so GNU/Linux always takes -c.

8. live turn (describe-only)

$ cd /workspace/devin-harness/scratch && devin -p -- "/pstack:statechart Describe-only check: do NOT run any scripts, do NOT write or edit any files. In under 150 words, explain what this skill does and list which scripts under its scripts/ folder it would run for a typical chart, by file name. Also say whether a scripts/model/OutputFolder.tla file exists in the skill folder."
I'll check for the skill folder (read-only) to answer the existence question, without running anything.
**What the skill does:** It bridges a TLA+ spec and a human-readable statechart. `from-spec` runs TLC over a model, maps states/steps to reader-friendly labels, and renders charts plus bug stories (`stories.md`, `summary.json`). `from-chart` takes an agreed Mermaid chart (with `%% never` rules) and generates a TLC-checked spec, catching design bugs. Supports `--against`, `--fixed`, `--png`, `--cover`, `--expect-broken`.

**Scripts run for a typical chart:** `statechart.mjs` is the only script invoked directly (`--help`, `from-spec`, `from-chart`, `render CHART.mmd`, `--png`). Everything else in `scripts/` — `render.mjs`, `tlc-to-chart.mjs`, `chart-to-tla.mjs`, `lib.mjs`, etc. — are helpers it imports.

**OutputFolder.tla:** No `scripts/model/OutputFolder.tla` in the devin plugin copy (`~/.local/share/devin/.../statechart` has no `model/` dir). It exists only in `/workspace/agy/skills/statechart/scripts/model/OutputFolder.tla` — likely a leftover artifact in that source checkout.
exit=0

The /workspace/agy/... hit is an unrelated checkout on the same box, outside this plugin. The installed 0.15.32 copy has no model/ dir, which matches step 6.

9. re-check and cleanup

$ git ls-remote https://github.com/pstack-ports/devin-pstack.git refs/pull/27/head
1c35735b02729e5f9409bdbcea841fd5c810a18d	refs/pull/27/head
$ devin plugins remove pstack-harness-pr27 -y
✓ Removed pstack-harness-pr27.
  note: auto-installed required plugins were left in place: pstack
$ devin plugins remove pstack -y
✓ Removed pstack.
$ devin plugins list
Installed plugins

  • thermos v1.0.0

No code was changed, and no allowlist entries were added. No secrets appear in this comment.

caelaxie

pass.

the file list matches upstream 4ec7ffa..e73df47 under pstack/. the only file left out is .cursor-plugin/plugin.json. all 36 scripts, tests, and .mmd files are byte-identical to upstream. the three OutputFolder.* files and model/ are gone.
every SKILL.md, readme, and guide hunk matches its upstream hunk. the only differences are the /pstack: prefix, triggers: [user], devin skill paths in reflect, the swarm step 3 renumber on top of the existing devin wording, and rg -a in worktree-audit, which was already on main.
skipping #806 is fine because the readme has no claude code install section. no cursor files are added.
plugin.json, .devin-plugin/plugin.json, and the readme marker all say 0.15.32.
the proof comment installs with devin plugins install --local through a wrapper pinned to 1c35735b, and devin plugins list shows pstack v0.15.32.
the head is still 1c35735b. validate plugin passed on it. the pr is not a draft, and it fixes no open issue.

port upstream pstack through 0.15.32

1c35735

sync pstack/ from cursor/plugins 4ec7ffa..e73df47. keep the devin path, slash-command, and worktree-audit adaptations already in this repo. Co-authored-by: Kaitian Xie <caelaxie@users.noreply.github.com>

caelaxie commented Oct 24, 2026

View reviewed changes

caelaxie merged commit 0a91289 into main Oct 24, 2026
1 check passed

caelaxie deleted the cursor/port-pstack-0.15.32-8e4e branch October 24, 2026 02:02

Navigation Menu

Repository navigation

port upstream pstack through 0.15.32 - #27

port upstream pstack through 0.15.32#27
caelaxie merged 1 commit into
mainfrom
cursor/port-pstack-0.15.32-8e4e

caelaxie commented Oct 24, 2026

Uh oh!

caelaxie left a comment

Uh oh!

caelaxie commented Oct 24, 2026

Uh oh!

caelaxie left a comment

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

caelaxie commented Oct 24, 2026

Uh oh!

caelaxie left a comment

Choose a reason for hiding this comment

Uh oh!

caelaxie commented Oct 24, 2026

harness proof

1–3. before list, install, after list

3–6. installed cache copy

7. skills from the 0.15.32 cache + spot checks

8. live turn (describe-only)

9. re-check and cleanup

Uh oh!

caelaxie left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants