diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json index 4c9f4e8e..9f37ce02 100644 --- a/.claude-plugin/marketplace.json +++ b/.claude-plugin/marketplace.json @@ -9,7 +9,7 @@ "name": "pstack", "source": "./plugins/pstack", "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence.", - "version": "1.15.0", + "version": "1.16.0", "author": { "name": "Lauren Tan (original)" }, diff --git a/.claude/skills/verify-open-pstack/features/registry.json b/.claude/skills/verify-open-pstack/features/registry.json index 21ad3caf..88ad664d 100644 --- a/.claude/skills/verify-open-pstack/features/registry.json +++ b/.claude/skills/verify-open-pstack/features/registry.json @@ -1,8 +1,9 @@ { "skills": [ "architect", "arena", "automate-me", "babysit", "benchmark-checklist", "blast-radius", "bro", "correct", - "create-verification-skill", "deslop", "figure-it-out", "fix-ci", "fix-merge-conflicts", - "get-pr-comments", "how", "in-your-own-words", "interrogate", "ketchup", "maintain-verification-skill", + "create-formal-verification-skill", "create-verification-skill", "deslop", "figure-it-out", + "fix-ci", "fix-merge-conflicts", "get-pr-comments", "how", "in-your-own-words", "interrogate", + "ketchup", "maintain-formal-verification-skill", "maintain-verification-skill", "make-pr-easy-to-review", "no-comments", "poteto-help", "poteto-mode", "principle-attack-the-premise", "principle-boundary-discipline", "principle-build-the-lever", "principle-encode-lessons-in-structure", "principle-exhaust-the-design-space", diff --git a/CHANGES.md b/CHANGES.md index 33ce1a5f..c9d9a4da 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -3,12 +3,30 @@ Mergify auto-queue is live: ready PRs to main require passing verify, Unfret and exact-head live-gate, and no unresolved review thread; workflow changes require operator queueing. This port applies the Cursor → Claude Code substitutions in skill bodies. Earlier drafts left them flagged; this revision resolves them. A later pass added a Codex build that shares the same skills; see [Codex port](#codex-port) below. -## Unreleased +## 1.16.0 syncs to Cursor pstack 0.15.29 + +Open Pstack 1.16.0 tracks Cursor pstack 0.15.29 at `88d47514b82e7c44f00f2b2a72ff6dd12158038c`. Sixteen upstream commits since 0.15.25 touch pstack. Nine change skill content, and all nine are applied with the port adaptations below. `a968159` names two skills after their folders: the port's `poteto-mode` already complies, and `make-bot-ui` stays out. Three add upstream's own Claude Code install and a docs check, which stay out apart from their README text. Three bump only the Cursor manifests and guide, which stay out. The release also fixes #46 and #235, and ships Claude Haiku 5.5 lanes (#223), foreground waits on Claude Code (#232, #233) and the comment sweep (#218), all merged after 1.15.0. Default roles and panels are unchanged. **Claude Haiku 5.5 lanes.** The model catalog registers `claude:claude-haiku-5-5` as an exact pin, with five native agents, `pstack-haiku-5-5-low` to `pstack-haiku-5-5-max`, and efforts `low` to `max`. On a Claude Code parent an unregistered Claude model is a dropout, so this is the first way to run Haiku lanes there. The pin is optional; no role default changes. The catalog registers no `haiku` alias, because Claude Code resolves that alias to Haiku 4.5, which has no effort setting, on Bedrock, Vertex and Foundry (#223, by @jwerby). **Claude Code subagents wait in the foreground.** The generated `pstack--` agents no longer set `background: true`, which Claude Code honored over a caller's `run_in_background: false` (#233). `references/codex-tools.md` has a Waits on Claude Code section: the main session runs long commands and fan-outs in the background, and a subagent dispatches the lanes it needs in the foreground, runs `watch-pr` in the foreground with `--timeout 240` instead of `/loop`, and waits on a background task in one bounded foreground call (#232). Provider dispatch, poteto-mode, babysit step 6 and `docs/reference.md` point to that section. +**`/recall` in worktree sessions (#235).** `recall`, `automate-me` and the session-pickup playbook now encode each `/` and each `.` of the workspace path as `-`, as Claude Code does. Before this, every session under `.claude/worktrees/` looked for a transcript folder that does not exist. + +**New skills.** `/create-formal-verification-skill` generates a project-local skill that formally verifies the code where a bug costs the most and tests reach the least, with TLA+ as the default tool and a fallback when no verifier fits. `/maintain-formal-verification-skill` finds the commits that touched verified code, brings the model and properties back in line, reruns them, and says whether each failure is drift or a bug. It runs only when typed. + +**Setup offers.** After its smoke test, setup offers once each to generate a verification skill and a formal verification skill, unless the project already has one. + +**Quiet setup reruns (#46).** On a rerun whose sheet loads with one valid setting line, with no change named and no inconsistency or kept-predecessor choice, setup no longer asks to keep the roles, asks no effort per family, and writes without a confirmation when every probe passes. It prints the kept roles, efforts and table, and mentions each verification offer in one line. Validation, permission checks, snapshots, readback and the smoke test still run, and a failed probe still stops without writing. A first run, an invalid sheet, a kept-predecessor proposal or a named change still asks. + +**Changed behavior.** `/sharpen` now returns a rewritten prompt and does not do the task: it says what a top professional would add, their raw material, methods and an outside check, then rewrites the prompt to ask for that. `/ketchup` lists every item waiting on the user, so each call is decidable from the reply, and never cuts items to stay under a word count. `typescript-best-practices` makes a brand with a type guard instead of `as`. `poteto-help` routes to the two formal verification skills and adds recipes for them and `/ketchup`. + +**Comments sweep (#218).** Code this repository owns drops comments outside the keep-list in `AGENTS.md`, across the runner, the Codex transcript resolver, the startup hook, the verifier, tests and repository config. A test keeps every model pair released by 1.15.0 in place. + +**Port adaptations.** `create-formal-verification-skill` drops `disable-model-invocation: true`, because setup's offer invokes it. The port's setup never had upstream's step 7 verification offer, so this sync restores it as step 10 and adds the formal offer as step 11, after the port's step 9. `poteto-help` keeps the port's install lines and harness paragraph. The verifier registers both new skills. + +**Not applied.** See `UPSTREAM.md`: upstream's generated Claude Code tree, its adapter, generator, plugin validator and root marketplace entry, the docs-vs-tree check, the two `poteto-help` harness paragraphs, `make-bot-ui`, and the 0.15.26 to 0.15.29 manifests and guide. Cursor's pstack now installs in Claude Code as `pstack@cursor-plugins`, with Claude models only and no Codex. Install one of the two, because both use the `pstack:` prefix. `README-UPSTREAM.md` is the verbatim upstream README. + ## 1.15.0 runs Devin, agy and dsh lanes in any repository Open Pstack 1.15.0 keeps the Cursor pstack 0.15.25 sync. It ships PR #215, merged after 1.14.0. Default roles and panels are unchanged. diff --git a/NOTICE.md b/NOTICE.md index c40ec501..7ceac4a1 100644 --- a/NOTICE.md +++ b/NOTICE.md @@ -24,6 +24,7 @@ This plugin is a port of upstream MIT-licensed work. All upstream copyright noti | `plugins/pstack/skills/` (0.15.6 to 0.15.17 changes: `benchmark-checklist`, `correct`, `ketchup`, `poteto-help`, `principle-explain-the-number`, architect red flags, fresh subagents, hourly audit tick, PR headings, performance mantras, prompt distillation), `plugins/pstack/agents/poteto-agent.md`, `README-UPSTREAM.md` | [cursor/plugins/pstack @ 978ca6e](https://github.com/cursor/plugins/tree/978ca6e9c0e012047cd5058b8e829240336e704e/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | | `plugins/pstack/skills/` (0.15.18 to 0.15.20 changes: `ketchup` before-and-after visuals, prompt cuts in `how`, `why`, poteto-mode playbooks, and four principles, the `/poteto-mode` chat as the playbook runner, `create-verification-skill` usable readiness, plan-checker fences, `watch-pr` review-thread pagination, `worktree-audit.sh -b`), `plugins/pstack/agents/poteto-agent.md`, `README-UPSTREAM.md` | [cursor/plugins/pstack @ 1b6d44f](https://github.com/cursor/plugins/tree/1b6d44ff26d4e242f4e8f68c391e6d2f7ca16def/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | | `plugins/pstack/skills/` (0.15.21 to 0.15.25 changes: the `in-your-own-words` and `sharpen` skills, per-spawn effort in poteto-mode and the routed skills, one full swarm per PR in the autopilots and the multi-phase plan, the Graphite-free `orch` frontier, the `watch-pr` owner-approval gate, Origin PRs in `worktree-audit.sh`, `ketchup` visuals and length, restated principles, and prompt cuts), `plugins/pstack/agents/poteto-agent.md`, `README-UPSTREAM.md` | [cursor/plugins/pstack @ 99743e9](https://github.com/cursor/plugins/tree/99743e9c151c8537cbbf1f98bb38f34ef3368453/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | +| `plugins/pstack/skills/` (0.15.26 to 0.15.29 changes: the `create-formal-verification-skill` and `maintain-formal-verification-skill` skills, setup's verification offers, `poteto-help` routing and recipes, the `sharpen` rewrite, `ketchup` waiting items, and the `typescript-best-practices` brand guard), `README-UPSTREAM.md` | [cursor/plugins/pstack @ 88d4751](https://github.com/cursor/plugins/tree/88d47514b82e7c44f00f2b2a72ff6dd12158038c/pstack) | (c) 2026 Lauren Tan | MIT | [LICENSE](LICENSE) | ## What changed in the port diff --git a/README-UPSTREAM.md b/README-UPSTREAM.md index 4e8b8c2a..9fde3a06 100644 --- a/README-UPSTREAM.md +++ b/README-UPSTREAM.md @@ -4,7 +4,7 @@ i'm [poteto](https://x.com/poteto). i'm not a president or ceo, but i've worked there's a growing sense that ai writes too much slop code. i agree. i don't want to ship like a team of twenty slop artists. throughput without quality is not a goal i aspire to. if you want to go fast, go deep first. -**pstack is my answer.** these are the same skills i use everyday to ship high quality code at Cursor. this turns cursor into a real engineering team. the goal is not to maximize loc, in fact it's the opposite. pstack helps you write less, but higher quality code. +**pstack is my answer.** these are the same skills i use every day to ship high quality code at Cursor. this turns cursor into a real engineering team. the goal is not to maximize loc, in fact it's the opposite. pstack helps you write less, but higher quality code. **pstack gives you fearless parallelism.** when you can go deep on one agent and trust it to write good, verifiable code, you can truly parallelize with confidence. start multiple agents up with `poteto-mode` and trust that they'll apply rigorous engineering principles to their work. @@ -18,6 +18,17 @@ fork it. improve it. make it yours. PRs are welcome! /add-plugin pstack ``` +in claude code: + +```bash +/plugin marketplace add cursor/plugins +/plugin install pstack@cursor-plugins +``` + +claude code prefixes plugin commands and agents, so `/poteto-mode` is `/pstack:poteto-mode`. the [claude code adapter](./docs/harness/claude-code.md) maps every other cursor name. in claude code, `/pstack:setup-pstack` writes your model choices to `~/.claude/rules/pstack-models.md`, and a step that needs a cursor-only feature, such as bugbot or automations, is skipped with a one-line note. + +claude code installs a generated copy of pstack, including this readme and the guide, from [`harness/pstack/`](https://github.com/cursor/plugins/tree/main/harness/pstack) at the repository root. after you change pstack, run `node scripts/generate-pstack-harness-trees.mjs` from the repository root and commit the result. ci fails while the generated copy is out of date. + ## get started two steps: @@ -27,7 +38,7 @@ two steps: new here? the [pstack guide](./docs/guide/README.md) walks you through a first real task, from setup and prompting through verification and overnight runs. stuck, or unsure which skill fits? ask [`/poteto-help`](./skills/poteto-help/SKILL.md). -that's it. the other skills are situational; the mode skill uses them for you as needed. out of the box the mode splits work by model strength: code delegates (feature, refactoring, bug fix, perf, hillclimb) go to grok, while the hardest changes, prose, and judgment go to opus 5.5. the default panel is opus 5.5 / grok. [`/setup-pstack`](./skills/setup-pstack/SKILL.md) changes any of it. +that's it. the other skills are situational, and the mode skill uses them for you as needed. out of the box the mode splits work by model strength: code delegates (feature, refactoring, bug fix, perf, hillclimb) go to grok, while the hardest changes, prose, and judgment go to opus 5.5. the default panel is opus 5.5 / grok. [`/setup-pstack`](./skills/setup-pstack/SKILL.md) changes any of it. ## usage @@ -70,7 +81,7 @@ morning. | [shipping](./skills/poteto-mode/playbooks/shipping.md) | independently verify a green stack, then land the contiguous verified run bottom-up through github by default or origin when available. | | [autonomous run](./skills/poteto-mode/playbooks/autonomous-run.md) | drive a long task to completion without stopping. | | [orchestrate](./skills/poteto-mode/playbooks/orchestrate.md) | a standing project handed to one coordinator chat: multi-day, many stacked prs, fleets of subagents. | -| [autopilot-full](./skills/poteto-mode/playbooks/autopilot-full.md) | run independent prs to merged with one owner per pr and a root swarm verdict on each round, from the code-ready head on. | +| [autopilot-full](./skills/poteto-mode/playbooks/autopilot-full.md) | run independent prs to merged with one owner per pr. a swarm verifies each code-ready head, and every later change to the patch gets a fresh check. | | [autopilot-stack](./skills/poteto-mode/playbooks/autopilot-stack.md) | build and verify one linear base-branch stack for the operator to review and land. | | [session pickup](./skills/poteto-mode/playbooks/session-pickup.md) | resume or take over a prior agent's in-flight work. | | [pause safely](./skills/poteto-mode/playbooks/pause-safely.md) | suspend in-flight work cleanly so it can be resumed later. | @@ -90,7 +101,7 @@ when invoked it: the full rules and playbooks live in [`skills/poteto-mode/SKILL.md`](./skills/poteto-mode/SKILL.md). -to keep [`/poteto-mode`](./skills/poteto-mode/SKILL.md) on across turns, pick it from the `/` menu and press option+enter (mac) or alt+enter (windows) instead of enter. that makes it a [custom mode](https://cursor.com/docs/skills), which cursor offers in the agents window and the cli. it stays in context every turn, applies itself when a playbook matches or the task needs rigor, and stays out of the way otherwise. plain enter attaches it to one message only. say so to opt out, or exit the mode to turn it off. +to keep [`/poteto-mode`](./skills/poteto-mode/SKILL.md) on across turns, pick it from the `/` menu and press option+enter (mac) or alt+enter (windows) instead of enter. that makes it a [custom mode](https://cursor.com/docs/skills#using-a-skill-as-a-custom-mode), which cursor offers in the agents window and the cli. it stays in context every turn until you exit the mode. plain enter attaches it to one message only. [`/poteto-mode`](./skills/poteto-mode/SKILL.md) works extremely well with cursor's `/loop` command. you can make cursor work for many hours without sacrificing rigor. @@ -114,11 +125,11 @@ to keep [`/poteto-mode`](./skills/poteto-mode/SKILL.md) on across turns, pick it | [`/poteto-mode`](./skills/poteto-mode/SKILL.md) | default entry point for any non-trivial task. | | [`/poteto-help`](./skills/poteto-help/SKILL.md) | you're new to pstack, or unsure which skill, playbook, or principle fits. finds out what you're trying to do, answers that part, and hands you a prompt to type. runs only when you type `/poteto-help`. | | [`/in-your-own-words`](./skills/in-your-own-words/SKILL.md) | you want the agent to play back your goal and the problem before it starts. runs only when you type `/in-your-own-words`. | -| [`/sharpen`](./skills/sharpen/SKILL.md) | you want a task approached the way a top expert would, aimed at what you're really after, without overspecifying it or deciding your choices for you. | +| [`/sharpen`](./skills/sharpen/SKILL.md) | you want a prompt made deeper, not bigger, before you send it: what a top professional would do that you didn't ask for, the raw material they'd start from, their methods and tools, and an outside check that the result is right. hands back the rewritten prompt and leaves your choices open. doesn't do the task. runs only when you type `/sharpen`. | | [`/how`](./skills/how/SKILL.md) | you want a walkthrough of how a subsystem works. | | [`/why`](./skills/why/SKILL.md) | you want to know why something was built this way. discovers available MCPs at run time and queries each evidence category in parallel (source control, issue tracker, long-form docs, real-time chat, infra observability, error tracking, analytics warehouse). | | [`/recall`](./skills/recall/SKILL.md) | you're starting or resuming work and want your recent context on a topic rebuilt from your own chat history and the shared record, handed back as a tight current-state brief. | -| [`/ketchup`](./skills/ketchup/SKILL.md) | you want what changed in this chat since your last message, in a few plain sentences and small visuals, with just enough context on each action item to make the call. | +| [`/ketchup`](./skills/ketchup/SKILL.md) | you want what changed in this chat since your last message, in plain words and small visuals, with every item waiting on you listed and decidable from the reply alone, even when that makes the reply long. | | [`/blast-radius`](./skills/blast-radius/SKILL.md) | you have a small-looking change and want to know what else it could break, with the one fact it's safe because of proven by running code, not asserted. | | [`/architect`](./skills/architect/SKILL.md) | you're about to write code that crosses a function boundary and want the caller's usage, types, and module shape settled first. | | [`/arena`](./skills/arena/SKILL.md) | you want N parallel attempts at the same thing, then to grab the best parts of each. | @@ -138,6 +149,8 @@ to keep [`/poteto-mode`](./skills/poteto-mode/SKILL.md) on across turns, pick it | [`/show-me-your-work`](./skills/show-me-your-work/SKILL.md) | you want a reviewable decision trail. logs decisions to a tsv you can commit. | | [`/create-verification-skill`](./skills/create-verification-skill/SKILL.md) | your project has no scripted way to prove app behavior. generates a project-local verify skill with a feature map, for any language or platform. | | [`/maintain-verification-skill`](./skills/maintain-verification-skill/SKILL.md) | your verify skill's feature map has drifted from the app. source wave + one live pass, at most one PR of proven corrections. | +| [`/create-formal-verification-skill`](./skills/create-formal-verification-skill/SKILL.md) | tests can't reach the case that breaks a race, retry, state machine, parser, or unsafe code. verifies one property with the tool that fits and generates a project-local skill to recheck it on every change. | +| [`/maintain-formal-verification-skill`](./skills/maintain-formal-verification-skill/SKILL.md) | code your formal verification covers has changed since it was last checked. updates the model, harness, or properties to match the code, reruns, and says whether each failure is drift in the verification or a bug in the code. | | [`/unslop`](./skills/unslop/SKILL.md) | you're cleaning up writing. removes AI tells. | | [`/bro`](./skills/bro/SKILL.md) | you want the last message restated in plain human language, no jargon. | | [`/technical-writing`](./skills/technical-writing/SKILL.md) | layered doc standard (Diátaxis + Google developer style + STE + Global English) for docs, RFCs, readmes, PR descriptions, commit messages. | @@ -245,7 +258,7 @@ a few things `poteto-mode` references but doesn't bundle: - `/deslop` and the `deslop` skill ship in the `cursor-team-kit` plugin. - `control-cli` (for CLIs and TUIs) and `control-ui` (for browser, Electron, web) ship in `cursor-team-kit` too. -- `/create-skill` is a cursor built-in. cursor also ships a built-in `/babysit`; inside `poteto-mode`, the [babysit playbook](./skills/poteto-mode/playbooks/babysit.md) supersedes it for pr-status requests. +- `/create-skill` is a cursor built-in. cursor also ships a built-in `/autopilot` that watches a pr. inside `poteto-mode`, pr-status requests go to the [babysit playbook](./skills/poteto-mode/playbooks/babysit.md) instead. install `cursor-team-kit` alongside pstack if you want the full set. @@ -267,7 +280,7 @@ when a default changes, a rule written before the change still pins the old defa pstack also ships a dormant [benny automation pack](./automations/benny/). benny triages slack issue reports, then reproduces and fixes confirmed bugs with real ui evidence. its files are not registered as slash skills. -to set it up, point cursor at [`FOR_AGENTS.md`](./automations/benny/FOR_AGENTS.md). setup copies the pack into the target repository at `.cursor/automations/benny/`, enables pstack there for shared skills, and keeps user configuration outside the copied pack. +to set it up, point cursor at [`FOR_AGENTS.md`](./automations/benny/FOR_AGENTS.md). setup copies the pack into the target repository at `.cursor/automations/benny/`, enables pstack there for shared skills, and keeps user configuration outside the copied pack. benny runs on cursor automations, so it is cursor-only. ## license diff --git a/README.md b/README.md index c144e9e9..0c02a8d4 100644 --- a/README.md +++ b/README.md @@ -128,12 +128,14 @@ That is the main workflow. The other skills are there when poteto-mode needs the | `interrogate` | You want different models to try to break a design or diff. | | `create-verification-skill` | Your project has no repeatable way for an agent to prove real behavior. | | `maintain-verification-skill` | The project's verification instructions no longer match the product. | +| `create-formal-verification-skill` | A race, an invariant, or another property needs a proof that tests rarely reach. | +| `maintain-formal-verification-skill` | The code a formal verification covers has changed, and you need to know whether a failure is drift or a bug. | | `babysit` | A pull request needs CI failures and review comments handled until it is ready. | | `reflect` | A hard task is finished and its lessons should improve the next run. | | `correct` | Agents keep making the same mistake in a repository and you want a check that stops it. | | `poteto-help` | You want to know which skill, playbook, or principle fits a question. | | `in-your-own-words` | You want the agent to restate your goal and the problem before it starts. | -| `sharpen` | You want a task approached the way a top expert would, aimed at what you are really after, without overspecifying it. | +| `sharpen` | You want a prompt rewritten deeper, not bigger, before you send it. It returns the rewritten prompt and does not do the task. | Plugin skills include `pstack:` in their name. In Claude Code, invoke a native skill such as `/pstack:architect`. In Codex, ask for the skill, such as `Use pstack:architect for this design.` See the [technical reference](docs/reference.md) for the full list. @@ -170,12 +172,14 @@ This repository also keeps: ## Staying close to Lauren's pstack -Open Pstack 1.15.0 tracks pstack 0.15.25 at Cursor commit [`99743e9c151c8537cbbf1f98bb38f34ef3368453`](https://github.com/cursor/plugins/commit/99743e9c151c8537cbbf1f98bb38f34ef3368453). +Open Pstack 1.16.0 tracks pstack 0.15.29 at Cursor commit [`88d47514b82e7c44f00f2b2a72ff6dd12158038c`](https://github.com/cursor/plugins/commit/88d47514b82e7c44f00f2b2a72ff6dd12158038c). The two projects have separate version numbers. The pstack version identifies Lauren's upstream content. The Open Pstack version identifies the Claude Code and Codex package built from it. In this repository, “upstream” means Lauren's original pstack. Open Pstack does not promise instant updates. It records the exact version it follows, reviews new changes in order, and changes only what Claude Code and Codex require. New pstack behavior belongs in Lauren's project first whenever possible. +Cursor's pstack now installs in Claude Code as `pstack@cursor-plugins`, with Claude models only and no Codex. Install only one of the two, because both use the `pstack:` prefix. + ## Contributing Fixes for Claude Code or Codex and help bringing over new pstack releases are welcome. Search [GitHub Issues](https://github.com/ericlitman/open-pstack/issues) before opening a new issue. For larger behavior changes, explain why the change belongs in Open Pstack instead of Lauren's original project. diff --git a/UPSTREAM.md b/UPSTREAM.md index 768abcf7..30e5de1f 100644 --- a/UPSTREAM.md +++ b/UPSTREAM.md @@ -8,15 +8,15 @@ open-pstack tracks [Cursor's pstack](https://github.com/cursor/plugins/tree/main | --- | --- | | Repository | `https://github.com/cursor/plugins.git` | | Path | `pstack/` | -| Commit | `99743e9c151c8537cbbf1f98bb38f34ef3368453` | -| Upstream version | `0.15.25` | -| open-pstack version | `1.15.0` | +| Commit | `88d47514b82e7c44f00f2b2a72ff6dd12158038c` | +| Upstream version | `0.15.29` | +| open-pstack version | `1.16.0` | -The table above is the current Cursor sync point. Open Pstack 1.10.0 imported this 0.15.25 sync, and 1.11.0 through 1.15.0 keep it. `README-UPSTREAM.md` preserves the upstream pstack README verbatim. `CHANGES.md` and `NOTICE.md` describe the adaptations and provenance. +The table above is the current Cursor sync point. Open Pstack 1.16.0 imported this 0.15.29 sync. `README-UPSTREAM.md` preserves the upstream pstack README verbatim. `CHANGES.md` and `NOTICE.md` describe the adaptations and provenance. ## Upstream-only exclusions -- Commits `799151d` and `6fecddb` add and relocate `make-bot-ui`. It depends on Cursor routines, webhook events, and UI primitives that Claude Code and Codex do not share. +- Commits `799151d` and `6fecddb` add and relocate `make-bot-ui`, and `a968159` renames it after its folder. It depends on Cursor routines, webhook events, and UI primitives that Claude Code and Codex do not share. `a968159`'s other hunk names `poteto-mode` after its folder, which the port's `poteto-mode/SKILL.md` already does. - Four `disable-model-invocation: true` lines from `73f8be4` are not applied to `how`, `why`, `unslop`, or `typescript-best-practices`. Poteto-mode invokes those skills by name, and the flag blocks that route on Claude Code. - The default-model hunks for `bug-fix`, `perf-issue`, and `hillclimb` from `23a56e2`, `889ec4b`, and `70b2dc8` are not applied. Those frequent code-writing roles stay on `codex:gpt-6.1-sol@max`. - `5bf2b15`'s setup budget question, its `# budget` line, and its step down to a lower detected effort are not applied. Setup already asks one requested effort per assigned family, and the step-down would silently lower a requested effort. @@ -33,15 +33,24 @@ The table above is the current Cursor sync point. Open Pstack 1.10.0 imported th - The root Agent Plugins v1 `pstack/plugin.json` from `e5a02f8` and its version bumps through 0.15.25 are not applied. The port keeps its current Claude manifest at `plugins/pstack/.claude-plugin/plugin.json` and Codex manifest at `plugins/pstack/.codex-plugin/plugin.json`. Agent Plugins v1 is revisited with #13. - `unslop` takes `bc697d0`'s description without its `disable-model-invocation: true` line, as for `73f8be4` above. - `pstack/.cursor-plugin/plugin.json` and `pstack/docs/guide/` are not imported. The Cursor manifest has no Claude Code or Codex consumer, and the guide shows Cursor's interface; `poteto-help` links to the guide upstream. That covers the 0.15.21 to 0.15.25 version bumps and `e5136d8`'s guide edit. +- Upstream's own Claude Code install is not applied. That covers `182f2ce`'s and `1b80080`'s generated tree under `harness/pstack/claude-code/`, `scripts/generate-pstack-harness-trees.mjs`, `scripts/validate-plugins.mjs`, the root `.claude-plugin/marketplace.json` entry, the adapter at `pstack/docs/harness/claude-code.md`, and `a968159`'s generator change. That install runs `grok-*` and `gpt-*` roles on the session's Claude model, has no Codex, and maps Cursor names at runtime from the adapter, which would be a second mapping layer on top of the port's own. `README-UPSTREAM.md` takes the README text from `182f2ce`, `1b80080` and `019a6a2` verbatim. +- `019a6a2`'s guide refresh and `scripts/check-pstack-docs.mjs` are not applied. The port does not import `pstack/docs/guide/`, so that check has nothing to compare. The same covers the guide edits in `7b353f7`, `f9be7aa` and `d457567`. +- The two harness paragraphs that `f9be7aa` puts in `poteto-help/SKILL.md`, which install upstream's Claude Code tree and describe other tools, are not applied. The port keeps its own paragraph on Claude Code and Codex. +- The 0.15.26 to 0.15.29 manifest bumps in `pstack/plugin.json` and `pstack/.cursor-plugin/plugin.json` from `0b8e952`, `0148b78` and `d457567` are not applied, as for the earlier bumps above. +- `create-formal-verification-skill` takes `4382e68` without its `disable-model-invocation: true` line, because setup's formal verification offer invokes it and the flag blocks that route on Claude Code. `tests/skill-collision-repro.sh` lists it in `routed_model_skills`. `maintain-formal-verification-skill` keeps the flag and runs only when typed. +- Setup's verification offers are steps 10 and 11 in the port, after its step 9 smoke test. The port never took upstream's step 7, "Offer a verification skill", which upstream has carried since 0.11.3. This sync restores it as step 10, and `f9be7aa`'s formal verification offer becomes step 11. Each keeps upstream's check for a project that already has one. - `poteto-agent.md` does not take `b93e811`'s search of `~/.cursor/plugins/` for poteto-mode, its highest-version rule, or its note that the skill catalog hides poteto-mode. The Claude agent preloads `pstack:poteto-mode`, the port's poteto-mode is not hidden, and Codex has no `poteto-agent` type. The agent keeps upstream's "Use the absolute path your parent gave you." ## Local port-patch ledger +- **#235 — Claude transcript folder encoding**: the port wrote Claude Code's per-project transcript path into `recall`, `automate-me` and the `session-pickup` playbook. Claude Code encodes each `/` and each `.` in the workspace path as `-`, so a `.claude/worktrees/` session's folder holds `--claude-worktrees-`. Keep both characters in those three lines during syncs. - **#140 — Reflect transcript resolution**: Cursor's Reflect step 1 reads the `agent-transcripts/` directory its system prompt names; the port had substituted Claude Code's per-project directory, which left Codex without a lookup. The port replaces that step's body with one line that points to `plugins/pstack/skills/poteto-mode/references/codex-tools.md#active-transcripts`, and leaves the rest of `reflect/SKILL.md` unchanged. That mapping section holds the harness specifics: the Claude per-project scope, layouts, candidate and scan limits, opening-message verification, the Codex resolver call, and the 2,000-word digest fallback. The port-authored Bun resolver `plugins/pstack/skills/poteto-mode/scripts/resolve-codex-transcript.ts`, started through the `sh` launcher `resolve-codex-transcript` next to it so project Bun config and `.env` files cannot affect it, looks up the parent's known chat ID in Codex's read-only `threads` index, checks rollout scope and ownership, and prints opening-message metadata without transcript text. Preserve this divergence during upstream syncs: keep step 1 as the one-line pointer and keep the mapping section and resolver. - **#120 — harness config homes** (tracked for #105): Cursor's setup destination is `~/.cursor/rules/`. The shared port resolves nonempty `CLAUDE_CONFIG_DIR` / `CODEX_HOME`, otherwise `$HOME/.claude` / `$HOME/.codex`, once at `plugins/pstack/skills/poteto-mode/references/codex-tools.md#harness-config-homes`. `setup-pstack/SKILL.md` reuses that home for reads, sheet/integration writes, snapshots, restoration, and readback; Claude preserves the literal legacy import at the default home and renders exactly `@./pstack-models.md` for redirected homes, keeping spaces and `#` in the config-directory name out of the import line; reruns replace the one import whose target basename is `pstack-models.md`, append if absent, and stop if duplicated. Preserve this intentional divergence during upstream syncs. The named config-home invariant in `tests/skill-collision-repro.sh` rejects literal default destinations outside the legacy import, requires the literal default-home rendering and zero/one/many import rules, and verifies unset/empty/space-containing resolution without daily writes. See `CHANGES.md` for the port correction and `tests/setup-config-home-repro.sh` for redirected live-evidence preparation. The Cursor sync point is unchanged. - **#157 — role pointers**: Cursor names model descriptors in the Arena, Architect, How, Interrogate, and Swarm skills, the bug-fix, feature, hillclimb, perf-issue, and refactoring playbooks, poteto-mode's delegation defaults, and setup's probe table and first-run sheet. The port replaces each with a role pointer: the role's backticked sheet label and a link to `plugins/pstack/skills/poteto-mode/references/model-catalog.md#role-defaults`, which `registry/render.ts` generates from `plugins/pstack/skills/poteto-mode/scripts/runner/registry/models.ts`. Interrogate's reviewer table and setup's probe table and example sheet are deleted. When an upstream sync changes a model slug on one of these lines, keep the port's line and put the model change in `registry/models.ts`. `runner/registry.test.ts` enforces the rule: `ROLE_POINTERS` names each file's roles, and its text scan rejects any descriptor or versioned model name in `plugins/pstack/**/*.md`, `README.md`, and `docs/reference.md` outside the generated catalog and agents. +- **#46 — quiet setup reruns**: Upstream's setup has no keep-roles, per-family effort, or write-confirmation questions, so this is a port patch. `setup-pstack/SKILL.md` states one qualifying-rerun exception before step 2's keep-roles question. On a rerun whose sheet loaded with one valid setting line, with no change named and no inconsistency or kept-predecessor proposal that needs a choice, setup validates in step 3, keeps and prints the roles and efforts instead of asking steps 2 and 4, and writes without step 7's confirmation when every step 5 probe passes. Steps 4, 7 and 8 and the offers in steps 10 and 11 each name the exception. It skips no validation, permission check, snapshot, readback, or the step 9 smoke test, and a failed probe still stops without writing. `poteto-help` says the same for reruns. The verifier's `keep-setting` case gives no answers and requires the sheet and Codex mirror to keep their bytes with no `AskUserQuestion` call. Preserve this divergence during upstream syncs. + - **#191 — landing playbooks and per-spawn effort**: `ce649c0` cuts Shipping to six steps and both autopilots to principles. The port takes the cut's rules and reasons but keeps the landing procedure from 1.3.0: Shipping keeps steps 1 to 9, Autopilot-full step 2 holds the guarded rebase and push, and Autopilot-stack step 2 holds the fork and topology rules. Those steps disarm auto-merge and merge-queue entries before verification and before any rewrite, keep the verdict head and base apart from the landing head and base, resolve the base fetch remote apart from the head push URL, bind each push to a captured SHA, and merge only through a server-enforced expected head. The named landing invariants in `tests/skill-collision-repro.sh` check those rules by step and phrase, so a sync that moves them updates the invariants in the same change. `ce649c0`'s Match the model to the job rule is taken with port adaptations: the starting level is the role's configured effort, an unlisted effort moves to the nearest effort the catalog row lists, a configured `ultra` stays, and the fast and standard speed sentences are dropped because the port's descriptors carry no speed selector. - **#232 — subagent waits in babysit**: Cursor's babysit step 6 runs `drive` and `background` under `/loop`. Claude Code subagents have no `ScheduleWakeup`, so `/loop` cannot run in them. The port adds one sentence after the `/loop` sentence that limits `/loop` to the main session and points a Claude Code subagent to `plugins/pstack/skills/poteto-mode/references/codex-tools.md#waits-on-claude-code`, which holds the wait rules. Preserve this sentence during upstream syncs. @@ -58,19 +67,29 @@ Fetch and inspect only commits that touched pstack after the recorded sync point ```shell git fetch cursor main -git log --oneline 99743e9c151c8537cbbf1f98bb38f34ef3368453..cursor/main -- pstack -git diff --stat 99743e9c151c8537cbbf1f98bb38f34ef3368453..cursor/main -- pstack +git log --oneline 88d47514b82e7c44f00f2b2a72ff6dd12158038c..cursor/main -- pstack +git diff --stat 88d47514b82e7c44f00f2b2a72ff6dd12158038c..cursor/main -- pstack ``` No output means the tracked pstack tree has not changed. This comparison does not need a polling service or generated mirror branch. ## Incorporate a change -1. Create or update a GitHub issue in `ericlitman/open-pstack` and branch from current `main`. -2. Read each upstream pstack commit in order. Bring over its intent and content, then apply only the Claude Code and Codex substitutions documented in `CHANGES.md`. -3. Keep one shared `plugins/pstack/skills/` tree. Put harness translation in the existing `codex-tools.md` and provider routing in `provider-dispatch.md`; do not fork a skill per harness. -4. Update the commit and version in this file, the affected provenance rows in `NOTICE.md`, and `README-UPSTREAM.md` when upstream changes it. -5. Run CI-equivalent checks locally, then run the installed Claude Code and Codex behavioral lanes required by the changed surface. Unit tests alone are not a release gate. -6. Merge the reviewed PR before tagging the next open-pstack release. Publish the release with `python3 scripts/release.py publish` from a clean checkout of `main`. +1. Create or update a GitHub issue in `ericlitman/open-pstack` and branch from current `main`. Pin the upstream target commit in the issue. +2. Read each upstream pstack commit in order, and record a decision for each one in the issue as a table: adopt, adapt (name the adaptation), or exclude (give the reason). Bring over each adopted commit's intent and content, then apply only the Claude Code and Codex substitutions documented in `CHANGES.md` and the adaptations in this file. +3. Run the audit and the mechanical merge from a clean checkout: + + ```shell + python3 scripts/upstream-audit.py --port HEAD --upstream > audit.json + python3 scripts/upstream-merge.py audit.json + ``` + + The merge checks out files the port never changed, merges the rest three ways, and prints counts of verbatim, clean, review and unmapped paths. It exits 1 when any path needs review. +4. Resolve each review row by hand. A conflict hunk keeps the port's adaptation and takes upstream's new intent beside it. A change to an excluded path stays out and extends that exclusion's line in this file. Each unmapped path, such as a Cursor manifest or the guide, is excluded or mapped by a decision in step 2. Record every hand resolution and every new adaptation or exclusion in this file. +5. Keep one shared `plugins/pstack/skills/` tree. Put harness translation in the existing `codex-tools.md` and provider routing in `provider-dispatch.md`; do not fork a skill per harness. +6. Add every new skill to the `skills` list in `.claude/skills/verify-open-pstack/features/registry.json`. When the sync changes what a skill with its own recipe does, such as `setup-pstack`, update that recipe in `features/recipes.ts`, its unit tests under `scripts/`, and its feature page. +7. Update the commit and version in this file, add a provenance row to `NOTICE.md`, and take `README-UPSTREAM.md` when upstream changes its README. +8. Run CI-equivalent checks locally, then run the installed Claude Code and Codex behavioral lanes required by the changed surface with `verify-open-pstack`. A sync that edits the verifier runs from the candidate head with `--self-test`. A run above the session limit needs `--wide ""`. Unit tests alone are not a release gate. +9. Merge the reviewed PR before tagging the next open-pstack release. Publish the release with `python3 scripts/release.py publish` from a clean checkout of `main`. Cursor's version and open-pstack's version are independent. Cursor's version identifies the imported content; open-pstack's version identifies the cross-harness distribution. diff --git a/docs/reference.md b/docs/reference.md index 762a0beb..94bf510a 100644 --- a/docs/reference.md +++ b/docs/reference.md @@ -2,7 +2,7 @@ This page contains the full skill, dependency, runtime, and porting reference. For the plain-English introduction and quick start, see the [main README](../README.md). -[Poteto](https://x.com/poteto)'s [pstack](https://github.com/cursor/plugins/tree/main/pstack), adapted to run in Claude Code and Codex without Cursor. One shared skill tree serves both harnesses; Grok remains available as a model-provider lane. Version 1.15.0 is synced to Cursor pstack v0.15.25 at `99743e9c151c8537cbbf1f98bb38f34ef3368453`. See [UPSTREAM.md](../UPSTREAM.md) for the exact sync contract. +[Poteto](https://x.com/poteto)'s [pstack](https://github.com/cursor/plugins/tree/main/pstack), adapted to run in Claude Code and Codex without Cursor. One shared skill tree serves both harnesses; Grok remains available as a model-provider lane. Version 1.16.0 is synced to Cursor pstack v0.15.29 at `88d47514b82e7c44f00f2b2a72ff6dd12158038c`. See [UPSTREAM.md](../UPSTREAM.md) for the exact sync contract. Original by Lauren Tan. This distribution builds on Michael Denyer's [pstack-claude](https://github.com/michael-denyer/pstack-claude) port and retains its history and MIT attribution. It imports seven MIT-licensed skills from [cursor-team-kit](https://github.com/cursor/plugins/tree/main/cursor-team-kit): `deslop`, `thermo-nuclear-code-quality-review`, `make-pr-easy-to-review`, `fix-ci`, `fix-merge-conflicts`, `get-pr-comments`, `what-did-i-get-done`. @@ -59,7 +59,7 @@ The marketplace install is the normal user path. Direct links are only for testi ├── plugins/pstack/ # the plugin itself │ ├── .claude-plugin/plugin.json # Claude Code manifest │ ├── .codex-plugin/plugin.json # Codex manifest (skills: ./skills/) -│ ├── skills/ # 61 skills shared by Claude Code and Codex +│ ├── skills/ # 63 skills shared by Claude Code and Codex │ │ ├── poteto-mode/references/{codex-tools,provider-dispatch}.md # tool + provider routing │ │ └── poteto-mode/scripts/ # bun/bash/node tooling: watch-pr, orch, runner, resolve-codex-transcript, check-plan.mjs, worktree-audit.sh │ ├── hooks/ # SessionStart auto-fire: injects the poteto-mode mandate (Claude Code only) @@ -110,6 +110,7 @@ Not declared as deps, but referenced in skill bodies: - **`bun`** — runs the vendored `skills/poteto-mode/scripts/` tooling (`watch-pr`, `orch`, `runner`) and the port-authored `resolve-codex-transcript` launcher. Install via [`brew install oven-sh/bun/bun`](https://bun.sh). `bootstrap.ts` installs dependencies for `watch-pr` and `orch`; the runner uses only Bun and Node built-ins, so it launches directly without an install/re-exec layer. - **`git` 2.25 or later** — the runner asks `git rev-parse --git-common-dir` for a linked worktree's shared git directory, and `worktree-audit.sh` reads `git worktree list --porcelain`. Ubuntu 20.04 LTS ships 2.25; older git is unsupported. - **Bash on Windows** — the SessionStart hook runs through `hooks/run-hook.cmd`, which looks for Git for Windows' `bash.exe` in its standard system-wide and per-user locations, then for a `bash` on `PATH` (MSYS2, Cygwin). Without one, the hook exits 0 and skips the pstack startup context, as the superpowers wrapper it comes from does. Install [Git for Windows](https://git-scm.com/download/win) to get the context. In Codex, the hook starts `C:\Windows\System32\cmd.exe` by full path, because one command must work in both PowerShell and cmd. A Windows installed outside `C:\Windows` does not run the hook. +- **macOS, Linux or WSL2 for Claude writer lanes** — Claude Code's sandbox does not run on native Windows, so a Claude writer lane needs one of these hosts. - **`node`** — runs `skills/poteto-mode/scripts/check-plan.mjs`. The checker uses only Node built-ins and does not need Bun. - **Provider CLIs** — the external runner uses the assigned subscribed CLI directly, one per provider in the [model catalog's route table](../plugins/pstack/skills/poteto-mode/references/model-catalog.md#routes). Install and authenticate only the providers present in your model sheet. Some providers run read-only lanes only. The catalog notes for OpenCode, Amp, Cursor, Devin, agy and dsh say what repository and host configuration their CLIs load into a lane. Same-provider work stays native; the runner refuses it. - **`jq` and `rg` (ripgrep)** — only for `scripts/worktree-audit.sh` (the Worktree cleanup playbook). Without them the audit still runs but blanks its PR and LAST_CHAT columns, so it warns on stderr rather than returning a table that looks complete. @@ -145,6 +146,8 @@ The table uses the short upstream names. Claude Code exposes each native skill w | `/no-comments` | strip comments before review via the `comment-sicko` subagent, then fix what it finds | | `/create-verification-skill` | generate a project-local verification skill and feature map | | `/maintain-verification-skill` | re-sync a drifted verification skill and its feature map | +| `/create-formal-verification-skill` | generate a project-local skill that formally verifies a race, invariant, or other property tests rarely reach | +| `/maintain-formal-verification-skill` | bring a formal verification back in line after the code it covers changed, and say whether each failure is drift or a bug (typed only) | | `/deslop` | deslop a diff before commit | | `/babysit` | monitor an open PR, fix CI/comments, keep it merge-ready | | `/thermo-nuclear-code-quality-review` | extremely strict maintainability audit | @@ -158,7 +161,7 @@ The table uses the short upstream names. Claude Code exposes each native skill w | `/ketchup` | catch up on everything in this session since your last message (typed only) | | `/poteto-help` | find the skill, playbook, or principle for a question about pstack (typed only) | | `/in-your-own-words` | play back your goal and the problem before work starts (typed only) | -| `/sharpen` | approach a task the way a top expert would, aimed at the real goal, without overspecifying it (typed only) | +| `/sharpen` | rewrite a prompt deeper, not bigger, before you send it; returns the rewritten prompt and does not do the task (typed only) | ## Subagents diff --git a/plugins/pstack/.claude-plugin/plugin.json b/plugins/pstack/.claude-plugin/plugin.json index 7cbd5a18..495877ea 100644 --- a/plugins/pstack/.claude-plugin/plugin.json +++ b/plugins/pstack/.claude-plugin/plugin.json @@ -1,7 +1,7 @@ { "name": "pstack", "displayName": "pstack", - "version": "1.15.0", + "version": "1.16.0", "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence. Ported from cursor/plugins/pstack for Claude Code and Codex.", "author": { "name": "Lauren Tan" diff --git a/plugins/pstack/.codex-plugin/plugin.json b/plugins/pstack/.codex-plugin/plugin.json index 52fb4b5a..f98774aa 100644 --- a/plugins/pstack/.codex-plugin/plugin.json +++ b/plugins/pstack/.codex-plugin/plugin.json @@ -1,6 +1,6 @@ { "name": "pstack", - "version": "1.15.0", + "version": "1.16.0", "description": "if you want to go fast, go deep first. pstack helps you write less, but higher quality code. rigorous agent workflows you can parallelize with confidence. Codex port of the Claude Code plugin; skills are shared, tool names resolve via skills/poteto-mode/references/codex-tools.md.", "author": { "name": "Lauren Tan" diff --git a/plugins/pstack/skills/automate-me/SKILL.md b/plugins/pstack/skills/automate-me/SKILL.md index eb2ae680..005ff102 100644 --- a/plugins/pstack/skills/automate-me/SKILL.md +++ b/plugins/pstack/skills/automate-me/SKILL.md @@ -27,7 +27,7 @@ Update mode changes the rest of the flow: ### 1. Mine their history -Locate the active workspace's transcripts before fanning out. Claude Code stores them at `~/.claude/projects//*.jsonl`, where `` is the workspace's working directory with `/` → `-`. Use only that path. Don't glob across `~/.claude/projects/`. That crosses workspace boundaries and reads private chats from unrelated projects. +Locate the active workspace's transcripts before fanning out. Claude Code stores them at `~/.claude/projects//*.jsonl`, where `` is the workspace's working directory with each `/` and each `.` → `-`. Use only that path. Don't glob across `~/.claude/projects/`. That crosses workspace boundaries and reads private chats from unrelated projects. Survey recent agent conversations within that scope for recurring patterns. Run multiple parallel subagents across slices of history (e.g. last 2-4 weeks, split into 3 slices so each has enough material). Pick each subagent's effort for the job, per the Subagents section of the **poteto-mode** skill. Each slice mining subagent reads transcripts from the workspace-scoped path the parent provides, looks for the signals below, and returns a short structured list of patterns it saw with evidence pointers. Default signals worth hunting: diff --git a/plugins/pstack/skills/create-formal-verification-skill/SKILL.md b/plugins/pstack/skills/create-formal-verification-skill/SKILL.md new file mode 100644 index 00000000..a950e12d --- /dev/null +++ b/plugins/pstack/skills/create-formal-verification-skill/SKILL.md @@ -0,0 +1,40 @@ +--- +name: create-formal-verification-skill +description: "Generate a project-local skill that formally verifies the code where a bug costs the most and tests reach the least, in any language, with whichever verification tool fits. Use for /create-formal-verification-skill, \"model-check this race\", \"prove this invariant\", or when concurrency, retries, state machines, parsers, or unsafe code need more than tests." +--- + +# Create a formal verification skill + +A test checks the cases that someone thought to write. Formal verification checks every case in a stated scope: every order of steps in a model, every input up to a bound, or every input. This skill finds the part of the repo where that matters most, verifies one property of it, and leaves a project-local skill that lets the next agent check a change against that property. Write that skill for an agent who reads it cold, mid-change, and has never seen your work. The user must be able to trust the result and act on it without learning the verification language. + +## Choose the target from the code + +Answer from the codebase, and ask the user only what you cannot observe. If the user named an area or a bug, start there. + +A good target is a promise the code makes, where a break harms users and tests rarely reach the case that breaks it. Choose the strongest such target in the repo, not the one that is easiest to verify. + +## Let the question choose the tool + +Pick the tool that answers the question at the lowest cost: a model checker, a proof assistant, an SMT-backed verifier, or another tool. Whether events can happen in a bad order usually suits a model checker over a small model of the design, and TLA+ is the default for that in any language. Whether the code itself behaves for every input, as with memory safety, overflow, or a data-structure invariant, usually suits a verifier that runs on the code. If no verifier runs on this language, say so, and test the real code with generated inputs, not a hand model of the function. A property that must hold at every size, where a bound is not enough, can need a proof. Prefer a tool that the repo's developers can install and run, and tell the user why you chose it. + +## What makes it good + +- **True to the code.** Every part of the model or proof points to code that a reviewer can open. What the verification treats as one indivisible step is one indivisible step in the code. Names come from this repo. +- **Able to fail.** A check that you have never seen fail proves nothing. Show each property failing on a broken variant of the code it guards, such as a removed check or a reordered step. +- **Findings stay findings.** When the current code breaks the property, report it with the counterexample in the code's terms. Do not weaken the property or the model until it passes, and do not change product code unless the user asks. +- **Honest about scope.** Say what is verified, under which bounds and assumptions, and what is left out. A pass covers the model or the bound, not the whole system. +- **Readable without the tool.** State the property and the harm in one plain sentence each. Tell a counterexample as a short sequence of steps in the code's words. +- **Cheap to rerun.** One command, a reproducible tool version, and a run short enough that the next agent will use it on every relevant change. +- **Kept in step with the code.** Record which files and functions each check covers, and the commit at which you last confirmed that the verification describes them. When the covered code changes after that commit, the next agent can see that the verification needs another look. + +## Generate the verify skill + +Write a project-local skill with frontmatter that names the area and says when to use it. Without frontmatter, the skill never registers. From the skill alone, the next agent must be able to tell whether a change touches the verified code, run the check, tell a real bug from a modeling error, and update the verification when a change is intended. Put the coverage record and the sync commit in the skill, and tell the next agent to move the sync commit forward only after it confirms that the verification describes the code at the new commit. Use this repo's real commands, paths, and nouns, and leave no placeholders. + +## Prove it before you hand off + +Follow the generated skill once, as the next agent would, on a scratch change that breaks the property in the real code. It must catch the break. Then drop the scratch change and confirm that the check is back where it started: passing, or failing only on the findings you will report. A verify skill that was never run is a draft. If the skill misses the break or a step does not run, fix the skill or the verification, not the scratch change. + +## Hand off + +Tell the user what you verified, which tool you used and why, the bounds, what the check found in plain words, how to run it, and what it does not cover. Suggest a second target only if you found a close one. Point the user at `/maintain-formal-verification-skill` for bringing the verification back in line after changes that did not recheck it. diff --git a/plugins/pstack/skills/ketchup/SKILL.md b/plugins/pstack/skills/ketchup/SKILL.md index 8cd2bfd6..49e4d94c 100644 --- a/plugins/pstack/skills/ketchup/SKILL.md +++ b/plugins/pstack/skills/ketchup/SKILL.md @@ -1,12 +1,12 @@ --- name: ketchup -description: "Catch the user up on what changed in this chat since their last message, in a few plain sentences and small visuals. Give each action item just enough context to make the call. Use for /ketchup." +description: "Catch the user up on what changed in this chat since their last message, in plain words and small visuals. List every item waiting on them with what they need to decide it from the reply alone. Use for /ketchup." disable-model-invocation: true --- # Ketchup -Catch the user up on what changed in this chat since the last message they wrote before `/ketchup`, and help them understand each change, not only where it stands. Notifications and subagent results are not their messages. Assume the user remembers their last message and nothing after it. +Catch the user up on what changed in this chat since the last message they wrote before `/ketchup`, and help them understand each change, not only where it stands. Then lay out every call waiting on them so they can make it from your reply alone. Notifications and subagent results are not their messages. Assume the user remembers their last message and nothing after it. Use [`/bro`](../bro/SKILL.md)'s voice, not its task: plain words, short sentences, no jargon, like one person catching up another. Say what changed for the user, not how you did it. Say "the tests pass", not "CI is green". Leave out hashes, file paths, commands, build numbers, and test counts unless the user needs one to act. Call each PR, branch, or agent by a name the user would know, not by a label you invented. If a fact needs context to make sense, give the context or leave the fact out. @@ -14,24 +14,30 @@ Use [`/bro`](../bro/SKILL.md)'s voice, not its task: plain words, short sentence Keep this turn read-only. Make visuals only from what you already have: do not change code, start an app or a job, or post anything. Collect your own work since that message, reports from subagents, and messages from anyone else in this chat. Check the current state of each PR, CI run, or agent this chat touched. Check each number you will show against the facts it comes from, and say so when you correct one. -An action item is a decision or step only the user can take, such as a product choice, an approval, an irreversible action, or access you lack. Include any still waiting on the user, even one raised before their last message. Work you can still do yourself is not an action item. Never make up a call to fill the reply. A step the user did not ask for and the work does not need is not an action item, unless it is irreversible and waiting on the user: give it one action line, no visual, and skip what happens if the user does not answer. +An action item is a call or step only the user can take, such as a product choice, an approval, an irreversible action, or access you lack. Include any still waiting on the user, even one raised before their last message. Work you can still do yourself is not an action item. Never make up a call to fill the reply. A step the user did not ask for and the work does not need is not an action item, unless it is irreversible and waiting on the user: give it one line and no visual. + +One call can cover many items, such as each PR in a set awaiting merge. For each item, collect its link, what it changes for users, the evidence behind your pick, its risk, and your pick. Write "unknown" for a fact the call needs that you do not know. Leave out a link you do not have. ## Write the reply -Keep the whole reply well under 150 words, not counting visuals. When something is easier to grasp as a picture than as sentences, draw it: how a design or system works, a PR stack or dependency chain with each PR's state, a before and after of a fix, or options side by side. Never draw a status list or boxes with nothing connecting them. Never give a fact twice, in text or across visuals. Leave out work that changed nothing for the user. When words run short, cut from what happened before you cut from the action items. +Spend words on the calls, not on the story. Keep what happened under 100 words, not counting pictures, and shorter when less happened. Leave out work that changed nothing for the user. Give each item about 30 words. The reply grows with the number of items: two items need well under 150 words in all, not counting pictures, and thirty need far more. Never cut items or shrink them to stay under a word count: no count in place of a list, and no link in place of an item. A link can add depth, but the reply alone must be enough to decide. -Open with one sentence that says how many things need the user, or that nothing does. If nothing happened and nothing waits on the user, say so and stop. +Open with one short sentence that names what waits on the user, or says nothing does. The action items give the detail. If nothing happened and nothing waits on the user, say so and stop. Then show what happened, pictures first. Embed inline the screenshots and videos the work produced, then any diagram that explains a change. Then sum up in one short bullet per thing the user asked for: what came of it, and whether it is done, still running, failed, or not checked. Write each line the way you would say it out loud: "Search was slow from a missing index", not "Search review: done" or "Slow search: missing index". Name any bug found and fixed on the way. Each line must stay true when read alone. Never mark something done that still waits on the user, and leave out anything the action items say. Under the summary, give at most three short lines that change what the user knows or must do. Then name in one line any work left that you can do yourself. -Then list the action items as plain bullets, never as a diagram or box. Give each two lines, or one for an unasked irreversible step: the decision with your recommendation and why, then what happens if the user does not answer. Ask the call the user owns, such as merge, approve, or pick. A step you would take first goes in your recommendation. So does anything that must happen first, and anything that cannot be undone. Write "unknown" for a part you do not know. Link to the detail. +Then list the action items. Ask the call the user owns, such as merge, approve, or pick, and give your pick. A step you would take first goes in your pick. So does anything that must happen first, and anything that cannot be undone. Give the number or link of each PR, issue, or agent a call is about, also in a call between options. + +Fit the shape to the call. A call about one item is one bullet: the call, your pick, what it changes for users, the evidence behind your pick, and its risk, with the item named once. When items share a call, write the call and your pick once, then give each item its own bullet, riskiest first: its link and name, what it changes for users, the evidence behind your pick, and its risk. Name an item's pick only where it differs from the call's. Give each item's risk even when it is low, such as "Low risk: only the colors change." Say what waiting costs only when it is more than a delay, such as a deadline or lost data. -Show a choice after the list. If the screenshots above already show its options, write each option's gain and cost under its screenshot instead of drawing a new visual; otherwise, compare the options side by side, with the current state when there is one. Give every option the work weighed, each with what it gets the user and what it costs. Keep them out of the rest of the text. +For a call between options, give every option the work weighed, each with what it gets the user and what it costs, and the current state when there is one. Those costs are the call's risk, so add no separate risk line. When the screenshots above show the options, write each option's gain and cost under its screenshot. ## Visuals A visual is a picture: a screenshot, a video, a Mermaid diagram, a chart or diagram that the harness renders, or a generated image. A Markdown table is not a visual, even with before and after columns. +When something is easier to grasp as a picture than as sentences, draw it: how a design or system works, a PR stack or dependency chain with each PR's state, a before and after of a fix, or options side by side. Never draw a status list, a list of action items, or boxes with nothing connecting them. Never give a fact twice, in text or across visuals. + Keep each visual small enough to read at a glance: at most six boxes, with at most eight words in each. Write labels as plain words a person would say, not tags like "Tests: pass". A fact that needs a sentence belongs in the text, or nowhere. Embed screenshots and videos inline when the change is visible, not only as links. If a visible change has none, mark its summary line "No screenshot yet," and say there what changed on screen. Draw diagrams and charts from facts you have: a Mermaid diagram for how things connect and a rendered chart for numbers. Never invent a number, and never draw or generate a picture of a screen you did not capture. Link only artifacts that exist. diff --git a/plugins/pstack/skills/maintain-formal-verification-skill/SKILL.md b/plugins/pstack/skills/maintain-formal-verification-skill/SKILL.md new file mode 100644 index 00000000..5d2f7f22 --- /dev/null +++ b/plugins/pstack/skills/maintain-formal-verification-skill/SKILL.md @@ -0,0 +1,58 @@ +--- +name: maintain-formal-verification-skill +description: "Bring a project's formal verification back in line with the code after the code changes: find the commits that touched verified code, update the model, harness, or properties to describe the code as it is now, rerun, and say whether each failure is drift in the verification or a bug in the code. Use for /maintain-formal-verification-skill, \"is the model still true to the code\", or after merges and refactors that touched verified code without rechecking it." +disable-model-invocation: true +--- + +# Maintain a formal verification skill + +A formal check proves a property of what it describes. When the code changes and the verification does not, the check can keep passing while it describes code that no longer exists. That pass is the dangerous case, because it looks like a proof. This skill is the upkeep loop for a verify skill that `/create-formal-verification-skill` generated, or for any project-local skill that runs a model checker, prover, or code-level verifier against named code. The project-local skill handles a change that an agent makes while it uses that skill. This skill handles the changes that skipped it: merges, edits made without the skill, and drift that builds up across many commits. + +## Outcomes + +Give each check one outcome, and say which: + +- **in sync**: no change since the last sync alters what the check describes, and the check passes. +- **updated**: the code changed, the verification now describes the new code, and the check passes. +- **bug**: the verification describes the current code, and the code breaks the property. This is a finding about the code. It is not drift. +- **blocked**: the check could not be brought back in line or could not run. Say exactly why. + +A check can be both updated and bug: the update makes the verification describe the code again, and then the property fails on it. + +## Edit scope + +Edit only the verification: models, harnesses, property files, and the verify skill itself. Never edit product code during a run, unless the user asks you to. When a property fails on the current code, do not weaken the property or the model to make it pass. Report the failure. + +## Pass + +1. **Find the checks.** A verify skill has no fixed name, so find it by what it does: a project skill that runs a model checker, a prover, or another verifier against named code. Read each one you find, or the one the user named. For each check, collect the property, the code it covers, the bounds and assumptions, the command that runs it, and the commit where it was last confirmed to describe the code. If no verify skill exists, stop and point at `/create-formal-verification-skill`. If the skill does not record a sync commit, use the last commit that changed the verification files, and say that you did. + +2. **Run it as it is.** Run each check once before you change anything, and record the result. A pass here does not tell you that the code is correct. It tells you that the old description still holds. A failure here can be drift or a bug. Do not decide which until step 5. + +3. **Read every change to covered code.** Diff the covered files from the sync commit to the current commit, and read each commit message. Also look for code that moved: a covered function that is renamed, split, or moved to another file is still covered code. Also look for new code that touches the state that a check guards, such as a new function that writes the same fields. For each change, decide which of these it is: + - **No effect.** The change does not alter anything the verification describes, such as formatting, comments, or code paths that the verification does not cover. Check this against the model or harness, not against the commit message. + - **The verification no longer describes the code.** A step that was one indivisible action is now two, a branch was added or removed, a check moved, a new path reaches the guarded state, or a value now has a different range. The model or harness must change. + - **The promise changed on purpose.** The change alters what the code promises, and evidence in the change says that this is intended: the doc comment, the tests, the changelog, or the commit message. The property must change, and you must cite that evidence. + - **The promise may be broken.** The code changed, and no evidence says that the promise changed. Treat a failure that follows as a bug candidate. + +4. **Update from the code, not from the result.** Change the model or harness so that each changed part again points to code that a reviewer can open, and keep one indivisible step in the code as one step in the verification. Write the update from the code before you rerun, and do not shape it by what makes the check pass. Change a property only for a promise that changed on purpose. Write down the old wording, the new wording, and the evidence. Keep the bounds unless the change makes them wrong. If you must reduce a bound, say so in the report. + +5. **Rerun and judge each result.** + - **Pass:** the check can now pass on a description that has lost the ability to fail. Break the new code the way the property guards against, such as removing a new check or reordering a new step, and confirm that the check catches it. Then drop the break. + - **Fail:** replay the counterexample against the real code, step by step. If a step cannot happen in the code, the verification is wrong. Fix the verification, and say what was wrong. If every step can happen, it is a bug. Name the commit that introduced it, tell the counterexample as a sequence of steps in the code's own words, and state the harm in one sentence. If a cheap test or reproduction against the real code shows the bug, add it to the report as evidence. Do not commit it to the product code. + +6. **Update the verify skill.** Update the code that each check covers, the commands, the bounds, the assumptions, and the sync commit. Set the sync commit to the commit that you checked. Do not move the sync commit for a blocked check, and say so in the report. Then follow the verify skill once as the next agent would, so that you know its steps still run. + +## Report + +Tell the user, for each check: + +- the outcome, and the commits that you read; +- what changed in the verification and why, with a short reason for each change: the code changed shape, or the promise changed on purpose (with the evidence); +- the rerun result, and the break that you used to show the updated check can still fail; +- each bug, in plain words: the counterexample as steps in the code's words, the harm, and the commit that introduced it; +- what the verification still does not cover, including new code that it should cover and does not. + +Say outright which failures were drift in the verification and which were bugs in the code. For a check that passed before you updated it and fails after, say that the old pass was on a stale description. + +Put the verification updates in a change of their own, separate from any product fix. diff --git a/plugins/pstack/skills/poteto-help/SKILL.md b/plugins/pstack/skills/poteto-help/SKILL.md index 09ba3dbf..63610b96 100644 --- a/plugins/pstack/skills/poteto-help/SKILL.md +++ b/plugins/pstack/skills/poteto-help/SKILL.md @@ -26,6 +26,7 @@ Check the state that changes the answer, and mention it only when it does: - No `pstack-models.md` in the active harness's config home means `/setup-pstack` hasn't run for this user, so every role uses its default model. Resolve the config home per [`codex-tools.md`](../poteto-mode/references/codex-tools.md#harness-config-homes). - No `verify-*` skill or other app harness in the project means agents have no scripted way to drive the app. Mention `/create-verification-skill` when the question is about proving a change works. +- No formal verification skill in the project means no property is checked past what tests reach. Mention `/create-formal-verification-skill` when the question is about a race, an invariant, or another case tests rarely hit. When one exists and the code it covers changed after the commit it records as last in sync, mention `/maintain-formal-verification-skill` if the question touches that code. When the model rule is missing and it matters, ask whether the user wants to pick a model for each role and a requested effort now. It matters when the user is new, the question is about setup or cost, or the answer depends on which models run. Ask at most once per chat. If the need is also unclear, ask both questions together. Offer two choices: @@ -35,7 +36,7 @@ When the model rule is missing and it matters, ask whether the user wants to pic ## Get set up 1. Install. In Claude Code, run `/plugin marketplace add ericlitman/open-pstack`, then `/plugin install pstack@open-pstack`, then `/reload-plugins`. In Codex, run `codex plugin marketplace add ericlitman/open-pstack --ref main`, then `codex plugin add pstack@open-pstack`, and turn on `multi_agent` per [`codex-tools.md`](../poteto-mode/references/codex-tools.md). -2. Run [`/setup-pstack`](../setup-pstack/SKILL.md). It maps a model to each role, asks one requested effort for each model family it assigns, probes those models, and writes a model sheet. The sheet applies to new sessions. +2. Run [`/setup-pstack`](../setup-pstack/SKILL.md). It maps a model to each role, asks one requested effort for each model family it assigns, probes those models, and writes a model sheet. A rerun that keeps a valid sheet and names no change asks none of these questions: it keeps the sheet's roles and efforts, probes them, and writes when every probe passes. The sheet applies to new sessions. Then it offers once each to generate a verification skill and a formal verification skill for the project, unless the project already has one. On a rerun that keeps the sheet, it mentions each offer in one line instead of asking. 3. Start a real task with `/poteto-mode`, a goal, and a check that can pass or fail. In Claude Code, a typed skill carries the plugin prefix, as in `/pstack:poteto-mode`. In Codex, ask for a skill by name, as in "use pstack:poteto-mode". The [README](https://github.com/ericlitman/open-pstack#readme) and [guide page 1](https://github.com/cursor/plugins/blob/main/pstack/docs/guide/01-setup.md) have the details. Offer to word their first prompt with them, per [`references/prompting.md`](references/prompting.md). @@ -64,12 +65,12 @@ The default answer is `/poteto-mode`, which runs most of the others when its ste |---|---| | Do any non-trivial task with rigor | [`/poteto-mode`](../poteto-mode/SKILL.md) | | Check that the agent understood their goal and the problem before it starts | [`/in-your-own-words`](../in-your-own-words/SKILL.md) | -| Aim a task higher before starting: more expert, more outcome-focused, not overspecified | [`/sharpen`](../sharpen/SKILL.md) | +| Get a prompt rewritten deeper, not bigger, before sending it: what a top professional would add, their raw material and methods, and an outside check. It returns the prompt and doesn't do the task | [`/sharpen`](../sharpen/SKILL.md) | | Know how code works now, or where new code should live | [`/how`](../how/SKILL.md) | | Know why code is shaped this way, or where a number came from | [`/why`](../why/SKILL.md) | | Understand a change or subsystem, explained plainly | [`/teach`](../teach/SKILL.md) | | Catch up on their own recent work on a topic | [`/recall`](../recall/SKILL.md) | -| Catch up on what changed in this chat since their last message, in a few plain sentences and small visuals, with enough context to decide each action item | [`/ketchup`](../ketchup/SKILL.md) | +| Catch up on what changed in this chat since their last message, in plain words and small visuals, with every item waiting on them listed and decidable from the reply alone | [`/ketchup`](../ketchup/SKILL.md) | | Know what a small diff could break outside itself | [`/blast-radius`](../blast-radius/SKILL.md) | | Settle types and module shape before code that crosses a function boundary | [`/architect`](../architect/SKILL.md) | | Get several attempts at one brief, merged into the best one | [`/arena`](../arena/SKILL.md) | @@ -83,6 +84,8 @@ The default answer is `/poteto-mode`, which runs most of the others when its ste | Hear the last reply again in plain words | [`/bro`](../bro/SKILL.md) | | Give agents a scripted way to drive the app and prove behavior | [`/create-verification-skill`](../create-verification-skill/SKILL.md) | | Bring a verification skill and its feature map back in line with the app | [`/maintain-verification-skill`](../maintain-verification-skill/SKILL.md) | +| Formally verify a race, invariant, or other property that tests rarely reach | [`/create-formal-verification-skill`](../create-formal-verification-skill/SKILL.md) | +| Bring a formal verification back in line after the code it covers changed, and learn whether a failure is drift or a bug | [`/maintain-formal-verification-skill`](../maintain-formal-verification-skill/SKILL.md) | | Vet a performance number before reporting or acting on it | [`/benchmark-checklist`](../benchmark-checklist/SKILL.md) | | Run a large or cross-cutting change, or one to review after stepping away | [`/figure-it-out`](../figure-it-out/SKILL.md) | | Keep a decision log during a run, and review it afterward | [`/show-me-your-work`](../show-me-your-work/SKILL.md) | diff --git a/plugins/pstack/skills/poteto-help/references/recipes.md b/plugins/pstack/skills/poteto-help/references/recipes.md index d13da3a0..048e0750 100644 --- a/plugins/pstack/skills/poteto-help/references/recipes.md +++ b/plugins/pstack/skills/poteto-help/references/recipes.md @@ -6,7 +6,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. - `/poteto-mode read . restate the underlying issue in your own words, in plain english.` - `/in-your-own-words ` -- `/sharpen ` +- `/sharpen ` - `/poteto-mode investigate why . give me what we know, what data you used, and your best hypotheses. don't change any code yet.` - `use /how to understand . then use /why to find out why it broke recently.` - `/recall my work on from last week, then read .` @@ -34,6 +34,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. ## Review and ship - `/interrogate the whole branch, but skeptically. don't change anything yet. no nitpicks unless it's a real bug or regression.` Read the dismissals too. +- `/create-formal-verification-skill prove holds in , even when interleave or retry.` After merges or refactors in that code: `/maintain-formal-verification-skill`. - `/swarm check every package under against its check script. one worker per package. one report.` - `/poteto-mode open the pr. small ordered commits, evidence in the description.` - `/poteto-mode babysit this pr. get it green.` For status only: `/poteto-mode check on pr . anything outstanding?` @@ -43,6 +44,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. - `/poteto-mode im going to bed. in a fresh worktree off . done means . keep a decision log. don't ask me before committing. /loop until done. if you're truly stuck after a few hours, stop and write up why.` - `/show-me-your-work catch me up on what you did last night.` Read its Attention section first. +- `/ketchup` catches you up on this chat since your last message and lists every call that waits on you. - `/poteto-mode full autopilot on this queue. each item is independent.` - `/poteto-mode autopilot these changes but stack them, don't ship. i'll land the stack.` - `/reflect capture what we learned so the next run doesn't repeat it.` Approve only edits that change a future decision. diff --git a/plugins/pstack/skills/poteto-mode/playbooks/session-pickup.md b/plugins/pstack/skills/poteto-mode/playbooks/session-pickup.md index 01b8cea4..60988fb3 100644 --- a/plugins/pstack/skills/poteto-mode/playbooks/session-pickup.md +++ b/plugins/pstack/skills/poteto-mode/playbooks/session-pickup.md @@ -2,7 +2,7 @@ **You own the resume point. Read the prior trail, don't redo it.** -1. Locate the prior trail. A local transcript under Claude Code's per-project transcripts directory at `~/.claude/projects//*.jsonl` (where `` is the workspace cwd with `/` → `-`. Do not glob across other directories under `~/.claude/projects/`, that crosses workspace boundaries and reads private chats from unrelated projects), a cloud-agent URL, or a pushed branch. Read the metadata overview and last messages first, then scan back for the decision points. Parse a long transcript in a subagent and keep the reduced timeline in the main thread (the **principle-guard-the-context-window** skill). Pick each subagent's effort for the job, per the Subagents section. +1. Locate the prior trail. A local transcript under Claude Code's per-project transcripts directory at `~/.claude/projects//*.jsonl` (where `` is the workspace cwd with each `/` and each `.` → `-`. Do not glob across other directories under `~/.claude/projects/`, that crosses workspace boundaries and reads private chats from unrelated projects), a cloud-agent URL, or a pushed branch. Read the metadata overview and last messages first, then scan back for the decision points. Parse a long transcript in a subagent and keep the reduced timeline in the main thread (the **principle-guard-the-context-window** skill). Pick each subagent's effort for the job, per the Subagents section. 2. Reconstruct operational state. The branch and worktree, what already landed (`git log`, `git diff` against the base), the open todos, the decisions made. The prior trail is authoritative input. Resist the bias to re-derive it. 3. Diff done vs pending. Compare what shipped against what was planned, name the resume point, do not re-run the prior repro or redo completed work. A "let me verify from scratch" pass means you're treating the trail as untrustworthy when it's authoritative. 4. Route the remaining work to the matching playbook and pick the verdict: continue the execution, ship a finished recommendation, ratify or override a prior conclusion, or postmortem a failed run. The pickup playbook ends here. The routed playbook owns the rest. diff --git a/plugins/pstack/skills/recall/SKILL.md b/plugins/pstack/skills/recall/SKILL.md index 0baacbf4..48fcecdc 100644 --- a/plugins/pstack/skills/recall/SKILL.md +++ b/plugins/pstack/skills/recall/SKILL.md @@ -11,7 +11,7 @@ Keep it tight and on-topic. Read only what the in-scope threads need, then stop. Your context lives in two records. Your own chat history holds what you did and decided. The shared record holds everything that happened around the same code under other names: the symptoms users keep reporting, the fixes that shipped and got reverted, the errors still firing in prod. That second record is what the **why** skill searches, across source control, the issue tracker, chat and issue channels, long-form docs, and error tracking. A feature with a long bug tail keeps most of its story there, so don't reconstruct it from your transcripts alone. -Transcripts live at `~/.claude/projects//.jsonl`, where `` is the workspace path with the leading slash dropped and each "/" turned into "-" (so `/Users/you/proj` becomes `-Users-you-proj`). Every line is one chat message. +Transcripts live at `~/.claude/projects//.jsonl`, where `` is the workspace path with each "/" and each "." turned into "-" (so `/Users/you/proj` becomes `-Users-you-proj`, and `/Users/you/proj/.claude/worktrees/x` becomes `-Users-you-proj--claude-worktrees-x`). Every line is one chat message. 1. Classify, then route. One specific prior chat to resume is the `session-pickup` playbook, not this. Turning habits into a durable skill is `automate-me`. A human-readable summary of your work is a different task. Recall loads working context across recent chats before you act. If the user already gave you a full state capsule (paths, branch, the change), use it and skip the mining. 2. Lock the scope before searching. Pin the window ("recent" is a real range, default the last 7 days), the topic if named, and the workspace (default the active one. Never read another project's transcripts without being asked). State the scope back. Never quietly turn "all" into "recent N". diff --git a/plugins/pstack/skills/setup-pstack/SKILL.md b/plugins/pstack/skills/setup-pstack/SKILL.md index c1fd8f2a..9da5cb0a 100644 --- a/plugins/pstack/skills/setup-pstack/SKILL.md +++ b/plugins/pstack/skills/setup-pstack/SKILL.md @@ -39,7 +39,9 @@ The line `codex writer sandbox: full-access` or `codex writer sandbox: bounded` Treat the normalized values as current role-to-family assignments. Overlay those rows on the complete first-run role map, the catalog's [role defaults](../poteto-mode/references/model-catalog.md#role-defaults). Materialize any missing documented role row from that map on the next successful write. A duplicate role row is inconsistent state; report it and resolve it before probing. A row whose role is not in the role defaults, such as `how critics`, is from a retired role. Drop it and list it at confirmation. A bare host-native slug from an older sheet is also invalid because it does not say which provider owns it. A versioned Claude model that matches no matrix row, kept predecessor, or rolling alias remains inconsistent state. A value whose `(provider, model)` is a [kept predecessor](../poteto-mode/references/model-catalog.md#kept-predecessors-and-normalization) is not inconsistent state. On a rerun, propose replacing every occurrence with its family's current model at the same effort, and ask. If the operator declines, that family's model stays the kept predecessor for steps 3 to 7: probe it, render it, and write it unchanged. If the sheet is missing, seed from the role defaults, whose descriptors carry the model matrix's Default effort cells. -Then ask whether to keep these role-to-family assignments or change named roles. Keeping them is the default. Apply only role changes the operator names; never offer a reset of a customized sheet to the first-run assignments. A changed role may use any model-matrix family, `inherit-parent`, or `auto`. +A qualifying rerun is a rerun whose sheet loaded, whose loaded state has one valid setting line, on which the operator names no change, and where no inconsistency or kept-predecessor proposal needs a choice. On a qualifying rerun, validate in step 3. If that passes without resolving an inconsistency, keep the role assignments and efforts and print them instead of asking the questions in steps 2 and 4. If every step 5 probe then passes, print the step 7 table and write without step 7's confirmation. The qualifying rerun skips no validation, permission check, snapshot, readback, or the step 9 smoke test. + +Otherwise, ask whether to keep these role-to-family assignments or change named roles. Keeping them is the default. Apply only role changes the operator names; never offer a reset of a customized sheet to the first-run assignments. A changed role may use any model-matrix family, `inherit-parent`, or `auto`. If the loaded state has no setting line, ask once whether Codex writer lanes that the external runner launches should run with Codex's full-access sandbox. Say that full access lets the writer launch a browser and write dot-folders such as `.agents/`, and that it removes every sandbox limit, including filesystem confinement to the worktree. Declining is the default. Record `codex writer sandbox: full-access` on a yes and `codex writer sandbox: bounded` on a decline, so a rerun does not ask again. When the line exists, keep it unless the operator names a change, and do not ask. @@ -55,7 +57,7 @@ One distinct effort per family is the current value. A family with no non-alias ### 4. Collect one requested effort per family -Ask one effort question for each assigned family. Name each model, its current or proposed value, and the Selectable efforts from its matrix row. A family whose only selectable effort is `default` gets no effort question. Empty input keeps that value. On a first run, state the assigned families' matrix defaults before asking. On a rerun, state the parsed values without offering to reset customized role lanes. +Except on the qualifying rerun above, ask one effort question for each assigned family. Name each model, its current or proposed value, and the Selectable efforts from its matrix row. A family whose only selectable effort is `default` gets no effort question. Empty input keeps that value. On a first run, state the assigned families' matrix defaults before asking. On a rerun, state the parsed values without offering to reset customized role lanes. ### 5. Probe the requested pairs @@ -91,13 +93,13 @@ Rewrite every matrix-family descriptor to `provider:model@/pstack-models.md`, the route table for this parent, every rendered role and descriptor, and the setting line. Carry the loaded assignments into the new destination; only explicit role or effort changes and the documented normalization may change them. Ask for confirmation before writing. +Show any rolling-alias migrations as original and normalized descriptors and any retired-role rows dropped in step 2. Then show the source file read in step 2, the new destination `/pstack-models.md`, the route table for this parent, every rendered role and descriptor, and the setting line. Carry the loaded assignments into the new destination; only explicit role or effort changes and the documented normalization may change them. Ask for confirmation before writing, unless the qualifying rerun's probes all passed. Why and Reflect require the parent's live MCP surface. Keep their investigator, reviewer, and synthesizer roles on `inherit-parent` or `auto`; the bounded external runner deliberately omits ambient MCPs. `inherit-parent` and `auto` always validate, but say when they reduce a panel's provider diversity. For panel roles, one lane runs per entry. The list length is the fan-out count. `arena cross-judge pool` is a list from which Arena chooses a provider different from the parent and base candidate when possible. `swarm workers` is the default for every worker unless a race explicitly assigns another descriptor. Every non-alias role value must match `:@` and must have passed step 5. -After the operator confirms, separately check the parent's effective write permission for **both actual destinations** (the sheet and parent integration, resolved through `CODEX_HOME` when set) and any directory creation needed. Render both artifacts in memory and perform this check before the first write or directory creation. Native probes succeeding does not grant configuration-write permission. A restricted parent may still be allowed to write under `CODEX_HOME`; assess each resolved destination rather than rejecting it just because it is outside the workspace. If either destination is denied or its permission remains unknown, stop with the destination-specific explanation: leave every existing artifact byte-identical and create neither artifact on a first run. Do not test permission by overwriting a target, write only the allowed artifact, or automatically request escalation. +After the operator confirms, or the qualifying rerun's probes all pass, separately check the parent's effective write permission for **both actual destinations** (the sheet and parent integration, resolved through `CODEX_HOME` when set) and any directory creation needed. Render both artifacts in memory and perform this check before the first write or directory creation. Native probes succeeding does not grant configuration-write permission. A restricted parent may still be allowed to write under `CODEX_HOME`; assess each resolved destination rather than rejecting it just because it is outside the workspace. If either destination is denied or its permission remains unknown, stop with the destination-specific explanation: leave every existing artifact byte-identical and create neither artifact on a first run. Do not test permission by overwriting a target, write only the allowed artifact, or automatically request escalation. Only after both destinations are permitted, write the in-memory render from step 6 using step 8's snapshot and readback procedure. Never paste the role defaults as the result. They only seed step 2; selected efforts and explicit role changes always replace their values before writing. @@ -109,7 +111,7 @@ On Claude, the integration is the one `@` import line in `/CLAUDE.m On Codex, the integration is the exact sheet bytes between one `` and `` pair in `/AGENTS.md`. Replace that whole bounded block on a rerun. Insert one block at the end on first run. If either marker is missing, duplicated, or reversed, stop and report inconsistent state instead of guessing a boundary. -Snapshot every target's current bytes. Write the sheet and parent integration only after every requested pair passes and the operator confirms. Read both targets back and compare them with the in-memory render. If either write or readback fails, restore every snapshot and report the failure. An unchanged rerun must produce byte-identical sheet and integration content after normalization. +Snapshot every target's current bytes. Write the sheet and parent integration only after every requested pair passes and the operator confirms or the rerun qualifies. Read both targets back and compare them with the in-memory render. If either write or readback fails, restore every snapshot and report the failure. An unchanged rerun must produce byte-identical sheet and integration content after normalization. Do not copy the model sheet between harnesses without rerunning the parent-specific probes; route availability can differ even on the same host. @@ -118,3 +120,11 @@ Do not copy the model sheet between harnesses without rerunning the parent-speci Before declaring setup complete, run one small read-only mixed panel from this parent: every distinct chosen descriptor, distinct output/receipt paths, and an independent cross-judge. Launch Claude-native agents and every external process in the background with retained handles, then drain them. Verify the native transcript entries and every external receipt. A structural config check or unit test is not a substitute. Report the sheet path, parent route table, requested-effort probe results, smoke results, and external elapsed/token/cost receipts. Re-running this skill re-probes and updates the same sheet. Do not claim the provider exposed hidden applied-effort observability. + +### 10. Offer a verification skill (optional) + +Check whether the project has a way to drive the real app for proof (a `verify-*` skill, or an existing harness). If not, offer once: "want a project-local verification skill, so agents can drive the app the way a user does and prove changes work? I can generate one with /create-verification-skill." On yes, invoke `/create-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing. On the qualifying rerun, mention this offer in one line instead of asking, and do not invoke the skill. + +### 11. Offer a formal verification skill (optional) + +Check whether the project already has a formal verification skill (a project skill that runs a model checker, a proof, or another verifier against the code). If not, offer once: "want a formal verification skill, so agents can prove a key property of your code holds in every case in scope, not only the cases tests reach? I can generate one with /create-formal-verification-skill." On yes, invoke `/create-formal-verification-skill` (resolves wherever pstack is installed: workspace, user, or plugin). On no, move on without pushing. On the qualifying rerun, mention this offer in one line instead of asking, and do not invoke the skill. diff --git a/plugins/pstack/skills/sharpen/SKILL.md b/plugins/pstack/skills/sharpen/SKILL.md index 4f9bb4ab..5b4a7b10 100644 --- a/plugins/pstack/skills/sharpen/SKILL.md +++ b/plugins/pstack/skills/sharpen/SKILL.md @@ -1,7 +1,16 @@ --- name: sharpen -description: "Sharpen a task before starting: the expert approach, what the user is really after, and the right level of specification. Use for /sharpen." +description: "Make a task deeper, not bigger, then rewrite the prompt. Use for /sharpen." disable-model-invocation: true --- -Before starting, ask how a top expert would approach this task (their raw sources, their real methods, an outside check that the result is right), what the user is really after, and whether the task is over- or underspecified. Loosen constraints that don't serve the goal as readily as you add ones that do, and leave choices that are the user's to make open instead of deciding them. Fold in only what makes the work better, not bigger, but always keep one outside check that the result is right, without narrating the framing, then do the work. Don't hand back a rewritten prompt. +I want a deeper version of this task, not a bigger one. Before rewriting it, do four things: + +1. Say what a top professional in this field would do here that I'm not asking for. +2. Name the rawest material they would start from instead of what has already been digested for me. +3. Name the specific methods and tools they would use. +4. Say what, other than you or me, would show the result is right. + +Then rewrite my prompt to ask for exactly that. + +Leave choices that are mine to make open instead of deciding them. diff --git a/plugins/pstack/skills/typescript-best-practices/SKILL.md b/plugins/pstack/skills/typescript-best-practices/SKILL.md index 2bf543fb..33ebef76 100644 --- a/plugins/pstack/skills/typescript-best-practices/SKILL.md +++ b/plugins/pstack/skills/typescript-best-practices/SKILL.md @@ -11,7 +11,7 @@ Apply the **type-system-discipline** principle skill first. | Rule | Summary | |------|---------| | Discriminated unions | Model variants with a `kind` literal discriminant so impossible states can't be represented. No optional-field bags. | -| Branded types | Brand primitives with `& { readonly __brand: "X" }` so they can't be mixed up. Validate once at the boundary. | +| Branded types | Brand primitives with `& { readonly __brand: "X" }` so they can't be mixed up. Validate once at the boundary. A brand comes from a verifying type guard (`input is AgentId`), never from `as`. | | Constructive modeling | Build the shape so the illegal value can't be constructed. `[T, ...T[]]` for non-empty, `[T, T][]` for even length, `start` plus `duration` for a range. Not a runtime guard, not a wish for refinement types. | | Simplest total type | Keep `T[]` while every operation on it stays total. Strengthen to `NonEmpty` only where the loose type forces `!`, a cast, or a "should never happen" throw. | | `unknown` over `any` | External data is `unknown`. | diff --git a/plugins/pstack/skills/typescript-best-practices/references/patterns.md b/plugins/pstack/skills/typescript-best-practices/references/patterns.md index c21d876b..f8dd99b6 100644 --- a/plugins/pstack/skills/typescript-best-practices/references/patterns.md +++ b/plugins/pstack/skills/typescript-best-practices/references/patterns.md @@ -9,9 +9,13 @@ Brand primitives so they can't be mixed up. Validate once at the boundary. Downs ```ts type AgentId = string & { readonly __brand: "AgentId" }; +function isAgentId(input: string): input is AgentId { + return isUUID(input); +} + function parseAgentId(input: string): AgentId { - if (!isUUID(input)) throw new Error(`Invalid agent id: ${input}`); - return input as AgentId; + if (!isAgentId(input)) throw new Error(`Invalid agent id: ${input}`); + return input; } function focusAgent(id: AgentId): void { diff --git a/tests/skill-collision-repro.sh b/tests/skill-collision-repro.sh index 9c31aa66..5ba4dfd4 100755 --- a/tests/skill-collision-repro.sh +++ b/tests/skill-collision-repro.sh @@ -333,7 +333,7 @@ else note "ok: excluded upstream skills stay absent" fi -routed_model_skills=(how why unslop typescript-best-practices) +routed_model_skills=(how why unslop typescript-best-practices create-formal-verification-skill) routed_model_bad="" for name in "${routed_model_skills[@]}"; do routed_skill="$plugin/skills/$name/SKILL.md"