From 92f58e3ad4a6a7a9ad9049c67d4b04c1ea484814 Mon Sep 17 00:00:00 2001 From: athul-ramesh Date: Mon, 26 Oct 2026 03:10:52 +0530 Subject: [PATCH] feat(pstack): port compatible upstream 0.15.26-0.15.32 changes to e73df47 (0.7.0) --- .devin-plugin/plugin.json | 2 +- README.md | 10 ++-- docs/pstack-0.15.32-port-audit.md | 43 ++++++++++++++ docs/release-notes.md | 4 +- docs/usage-guide.md | 6 +- .../create-formal-verification-skill/SKILL.md | 44 ++++++++++++++ skills/ketchup/SKILL.md | 22 ++++--- .../SKILL.md | 59 +++++++++++++++++++ skills/poteto-help/SKILL.md | 8 ++- skills/poteto-help/references/recipes.md | 8 ++- skills/reflect/SKILL.md | 4 +- skills/sharpen/SKILL.md | 15 ++++- skills/typescript-best-practices/SKILL.md | 2 +- .../references/patterns.md | 8 ++- tests/port-contracts.test.mjs | 36 ++++++++++- 15 files changed, 243 insertions(+), 28 deletions(-) create mode 100644 docs/pstack-0.15.32-port-audit.md create mode 100644 skills/create-formal-verification-skill/SKILL.md create mode 100644 skills/maintain-formal-verification-skill/SKILL.md diff --git a/.devin-plugin/plugin.json b/.devin-plugin/plugin.json index 9492db2..dfe06e8 100644 --- a/.devin-plugin/plugin.json +++ b/.devin-plugin/plugin.json @@ -1,6 +1,6 @@ { "name": "pstack", - "version": "0.6.1", + "version": "0.7.0", "description": "Rigorous agent workflows for Devin CLI. Write less, higher quality code.", "homepage": "https://github.com/athul-ramesh/ptstack-devin", "repository": "https://github.com/athul-ramesh/ptstack-devin", diff --git a/README.md b/README.md index 7502c04..55ed147 100644 --- a/README.md +++ b/README.md @@ -22,19 +22,21 @@ The 0.2.0 release was verified against Devin CLI 3000.11.3 (9c803229faa4), local Avoid installing two copies with the same plugin name. Devin may source-qualify inventory names while loading skills from an older copy; verify the path returned by the skill tool. -## Using 0.5.0 +## Using 0.7.0 Ask `/pstack:poteto-help` with a setup or workflow question. This explicit-user skill answers with one suggested prompt and a source link. It does not start a task for a help question. A request to do work follows poteto-mode instead. -Invoke [`/pstack:ketchup`](skills/ketchup/SKILL.md) to catch up on this chat since your last message. It is explicit-user and read-only. It summarizes changes and decisions well under 150 words in plain sentences, with small available visuals, options, costs, a recommendation, and what happens without an answer. The CLI uses compact text when no renderer is available. +Invoke [`/pstack:ketchup`](skills/ketchup/SKILL.md) to catch up on this chat since your last message. It is explicit-user and read-only. It keeps the story short, then lists every call waiting on you, each with its link, what it changes, the evidence, the risk, and a pick, so you can decide from the reply alone. A large batch makes a long reply rather than a cut list. Small visuals appear only when the host renders them; the CLI uses compact text otherwise. The [usage guide](docs/usage-guide.md) covers prompting, investigation, prototypes before plans, real behavior verification, benchmark evidence, repeated-mistake enforcement, and bounded in-session delivery. The help skill includes [prompting guidance](skills/poteto-help/references/prompting.md) and [copyable recipes](skills/poteto-help/references/recipes.md). -Invoke [`/pstack:sharpen`](skills/sharpen/SKILL.md) before a task to have the agent frame it the way a top expert would, keep one outside check, leave your choices open, and then do the work. It runs only when requested. +Invoke [`/pstack:sharpen`](skills/sharpen/SKILL.md) on a prompt before you send it. The agent says what a top professional would add, the raw material and methods they would use, and an outside check, then hands back the rewritten prompt with your choices left open. It does not do the task. It runs only when requested. + +Invoke [`/pstack:create-formal-verification-skill`](skills/create-formal-verification-skill/SKILL.md) when tests cannot reach the case that breaks a race, retry, state machine, parser, or unsafe code. It verifies one property with a tool that fits and runs on your machine, shows the check failing on a broken variant, and writes a project skill under `.devin/skills/` to recheck it. [`/pstack:maintain-formal-verification-skill`](skills/maintain-formal-verification-skill/SKILL.md) brings that verification back in line after the covered code changes. This plugin bundles no verifier; the agent asks before installing one. Invoke [`/pstack:in-your-own-words`](skills/in-your-own-words/SKILL.md) to hear the goals and problem the agent understood. It runs only when requested and adds no confirmation gate. -Release 0.6.1 selectively ports upstream pstack 0.15.25; see the [0.15.25 port audit](docs/pstack-0.15.25-port-audit.md). Release 0.6.0 selectively ported upstream pstack 0.15.24; see the [0.15.24 port audit](docs/pstack-0.15.24-port-audit.md). The prior release selectively ported upstream pstack 0.15.23. It adds goal playback, shorter ketchup replies, usable-state verification, a cheap observability proposal after deep debugging, robust Markdown fence checks, and configurable worktree merge bases. Devin dispatch, profile pins, and delivery authority are preserved. See the [port audit](docs/pstack-0.15.23-port-audit.md) for source coverage, exclusions, and evidence limits. Earlier audits cover [0.15.17](docs/pstack-0.15.17-port-audit.md) and [0.15.13](docs/pstack-0.15.13-port-audit.md). +Release 0.7.0 selectively ports upstream pstack 0.15.26 through 0.15.32 and follow-ups to `e73df47`; see the [0.15.32 port audit](docs/pstack-0.15.32-port-audit.md). Release 0.6.1 selectively ported upstream pstack 0.15.25; see the [0.15.25 port audit](docs/pstack-0.15.25-port-audit.md). Release 0.6.0 selectively ported upstream pstack 0.15.24; see the [0.15.24 port audit](docs/pstack-0.15.24-port-audit.md). The prior release selectively ported upstream pstack 0.15.23. It adds goal playback, shorter ketchup replies, usable-state verification, a cheap observability proposal after deep debugging, robust Markdown fence checks, and configurable worktree merge bases. Devin dispatch, profile pins, and delivery authority are preserved. See the [port audit](docs/pstack-0.15.23-port-audit.md) for source coverage, exclusions, and evidence limits. Earlier audits cover [0.15.17](docs/pstack-0.15.17-port-audit.md) and [0.15.13](docs/pstack-0.15.13-port-audit.md). ## Features retained from 0.2.0 diff --git a/docs/pstack-0.15.32-port-audit.md b/docs/pstack-0.15.32-port-audit.md new file mode 100644 index 0000000..b507867 --- /dev/null +++ b/docs/pstack-0.15.32-port-audit.md @@ -0,0 +1,43 @@ +# Port pstack 0.15.26 to 0.15.32 to Devin + +Audited on 2026-10-26 on top of `main` at `28917b5` (PRs #8 and #9 merged). Plugin version is 0.7.0, with 39 public skills, 24 internal principle leaves, and 20 playbooks. + +## Source and coverage + +Upstream range: [`99743e9...e73df47`](https://github.com/cursor/plugins/compare/99743e9c151c8537cbbf1f98bb38f34ef3368453...e73df471cd4bd918367e99f3dd9c51bd53ddf5f0) (`pstack/`, 0.15.25 to 0.15.32 and six follow-ups). All 32 commits that touch `pstack/` were read. + +| Upstream change | Devin disposition | +| --- | --- | +| [#700](https://github.com/cursor/plugins/commit/0317eb8) brand with a type guard, not `as` | Ported. The Branded types row and the `AgentId` example use an `isAgentId` guard. | +| [#692](https://github.com/cursor/plugins/commit/16541c6), [#708](https://github.com/cursor/plugins/commit/bc14437) ketchup lists every waiting item | Adapted. The story stays under 100 words, each item gets about 30 words with its link, user change, evidence, risk, and pick, and items are never cut to meet a word count. Rendered pictures stay conditional on the Devin host and the text fallback is kept. | +| [#712](https://github.com/cursor/plugins/commit/75fabac), [#729](https://github.com/cursor/plugins/commit/88d4751) sharpen returns only the rewritten prompt | Ported in its final form, the four numbered asks and a rewrite. One Devin line is added: hand back only the rewrite and do not start the task, because this plugin's always-on rule otherwise routes nontrivial work to poteto-mode. Help, recipes, README, and usage guide follow. | +| [#709](https://github.com/cursor/plugins/commit/4382e68), [#721](https://github.com/cursor/plugins/commit/6b78e9f), [#716](https://github.com/cursor/plugins/commit/7b353f7), [#724](https://github.com/cursor/plugins/commit/d457567) create and maintain formal verification skills | Adapted as explicit-user `/pstack:create-formal-verification-skill` and `/pstack:maintain-formal-verification-skill`. Generated skills go under `.devin/skills/`. The plugin bundles no verifier, so the agent confirms the tool runs with `exec`, asks before installing a toolchain, and reports a check that could not run as blocked. The TLA+ default and the generated-input fallback are kept. Maintenance stops at merge-ready. | +| [#715](https://github.com/cursor/plugins/commit/f9be7aa) formal verification in setup, help, and guide | Help state check, routing rows, and recipes ported. The setup offer is skipped: this port's `/pstack:setup-pstack` only writes the role sheet and has no verification offer step to extend. Cursor guide pages are not shipped; the usage guide gains the equivalent section. | +| [#794](https://github.com/cursor/plugins/commit/00d5dec) generated verify skills read results with `/statechart` | Skipped. `/statechart` is not shipped. Counterexamples are still told as steps in the code's words. | +| [#741](https://github.com/cursor/plugins/commit/eb4db2b), [#776](https://github.com/cursor/plugins/commit/7698375), [#779](https://github.com/cursor/plugins/commit/4ec7ffa), [#791](https://github.com/cursor/plugins/commit/076f4b2) statechart skill and Pele renderer | Skipped as uncertain. About 12,000 lines of Node scripts and tests (about 5,200 without tests) that install TLC and Java with mise (about 305 MB), render PNGs with Pele and resvg, and expect the agent to look at each PNG. Devin documents image attachments as input, not inline image output in the CLI. A separate port needs native testing first. | +| [#797](https://github.com/cursor/plugins/commit/3c0fdb4) ketchup-video | Skipped as uncertain. It needs a video renderer and inline video in the reply. Devin documents neither, and this plugin ships no renderer. | +| [#800](https://github.com/cursor/plugins/commit/7054003) reflect edits leave the plugin cache | Adapted. Reflect never edits a skill inside an installed plugin. A remote plugin is re-fetched by `devin plugins update`; a `--local` plugin is linked to its checkout. Edits go to a copy under `.devin/skills/` or `~/.config/devin/skills/`, shown before approval, with no PR or push. | +| [#702](https://github.com/cursor/plugins/commit/a968159) name every skill after its folder | Already satisfied. A contract test now enforces it, since Devin uses the folder as the skill identifier. | +| [#807](https://github.com/cursor/plugins/commit/e73df47) swarm Phase A numbering and table reference | Already satisfied. This port's swarm is numbered 1 to 4 and Phase C keeps the result table that Phase D reports. | +| [#801](https://github.com/cursor/plugins/commit/96dec8e), [#802](https://github.com/cursor/plugins/commit/fe096ef) watch-pr fork heads and deadline sleeps; [#804](https://github.com/cursor/plugins/commit/3c596e7) orch prefers the active PR | Not applicable. The Bun watch-pr and orch scripts are not shipped in this port. `worktree-audit.sh` already prefers an open PR per branch. | +| [#803](https://github.com/cursor/plugins/commit/86c2448) inline code delimiters in check-plan | Not applicable. This port's `check-plan.mjs` validates structure and has no prose lint that strips inline code. | +| [#805](https://github.com/cursor/plugins/commit/f83fbe6) GNU stat and date in worktree-audit | Not applicable. This port's `worktree-audit.sh` reads no transcript mtimes; it uses `git log --format=%ct`, which is portable. | +| [#637](https://github.com/cursor/plugins/commit/182f2ce), [#705](https://github.com/cursor/plugins/commit/1b80080), [#806](https://github.com/cursor/plugins/commit/a0b0ad9) Claude Code plugin, adapter, and auto-update note | Skipped. Claude Code only. | +| [#704](https://github.com/cursor/plugins/commit/019a6a2) docs refresh and docs-vs-tree check | Skipped. Cursor README and guide wording plus a repo script for the generated Claude Code tree. The existing link and help-table tests cover this port's docs. | +| [#710](https://github.com/cursor/plugins/commit/0b8e952), [#713](https://github.com/cursor/plugins/commit/0148b78), [#792](https://github.com/cursor/plugins/commit/642289e), [#798](https://github.com/cursor/plugins/commit/b1a1298) version bumps | Plugin bumped independently to 0.7.0. | + +## Devin compatibility + +| Capability | Evidence | +| --- | --- | +| Explicit-user skills and folder names | `triggers` and `name` are documented; the directory name is the identifier. [Creating skills](https://docs.devin.ai/cli/extensibility/skills/creating-skills). | +| Project and global skill paths | `.devin/skills/`, `.agents/skills/`, `.windsurf/skills/`, `~/.config/devin/skills/`. [Skills overview](https://docs.devin.ai/cli/extensibility/skills/overview). | +| Plugin update and local links | `devin plugins info`, `devin plugins update` re-fetches, and `--local` installs link to the source folder. [Plugins](https://docs.devin.ai/cli/extensibility/plugins/overview). | +| Inline images, video, Mermaid | Not documented for the CLI terminal. [CLI changelog](https://docs.devin.ai/cli/changelog/stable). Ketchup keeps its text fallback; statechart and ketchup-video are not shipped. | +| Verifier toolchains | Not provided by Devin or this plugin. The agent runs them with `exec` only after confirming they exist, and asks before installing. | + +The other changes are prose and touch no Devin tool, profile, hook, or helper. + +## Verification and limits + +`node --test tests/*.test.mjs` passes, including new contract tests for skill folder names and this port's Devin paths, tool limits, and reflect destinations. These are static checks. Native 0.7.0 skill registration, a real TLA+ or other verifier run through the new skills, and inline rendering in Devin are untested. diff --git a/docs/release-notes.md b/docs/release-notes.md index a20438d..90b5a25 100644 --- a/docs/release-notes.md +++ b/docs/release-notes.md @@ -1,5 +1,7 @@ # Release notes +Plugin `pstack` 0.7.0 selectively ports upstream 0.15.26 through 0.15.32 and follow-ups to `e73df47`. It adds explicit-user `/pstack:create-formal-verification-skill` and `/pstack:maintain-formal-verification-skill`, which write project skills under `.devin/skills/`, bundle no verifier, and ask before installing one. `/pstack:sharpen` now hands back a rewritten prompt and does not do the task. Ketchup lists every waiting item with its link, evidence, risk, and pick, and never cuts items to meet a word count. Reflect never edits a skill inside an installed plugin. The TypeScript brand example uses a type guard. Statechart and ketchup-video are not shipped. Native activation of 0.7.0 remains untested. See the [port audit](pstack-0.15.32-port-audit.md). + Plugin `pstack` 0.6.1 selectively ports upstream 0.15.25. Four principles (attack-the-premise, fix-root-causes, make-operations-idempotent, test-behavior-not-implementation) are restated as reasoning instead of rules, and `/pstack:correct` follows the new test rule. Marginal sections are cut from interrogate's lead judgment, migrate-callers, type-system-discipline, and swarm. Ketchup now explains each change, leads with existing screenshots, videos, and diagrams when the host renders them, sums up in bullets, and lists action items as plain bullets. The Devin text fallback is kept. Native activation of 0.6.1 and inline image rendering remain untested. See the [port audit](pstack-0.15.25-port-audit.md). Plugin `pstack` 0.6.0 selectively ports upstream 0.15.24. It adds explicit-user `/pstack:sharpen`, rewrites ketchup to a reply well under 150 words with small plain-language visuals, states that Devin dispatch has no per-call effort or speed knob, and runs the full plan audit set once at the code-ready SHA with a single fresh-context verifier for rebases and minor fixes. Native activation of 0.6.0 remains untested. See the [port audit](pstack-0.15.24-port-audit.md). @@ -14,7 +16,7 @@ Plugin 0.2.0 was verified on local Devin CLI 3000.11.3 (9c803229faa4). Earlier 3 ## Shipped -37 public skills under `/pstack:`. 24 `principle-*` leaves, model-triggered. 20 poteto-mode playbooks. Profiles `pstack:poteto-agent`, `pstack:poteto-agent-{swe,opus,sonnet,codex}`, `pstack:comment-sicko`, and `pstack:panel-{swe,opus,sonnet,codex}`. +39 public skills under `/pstack:`. 24 `principle-*` leaves, model-triggered. 20 poteto-mode playbooks. Profiles `pstack:poteto-agent`, `pstack:poteto-agent-{swe,opus,sonnet,codex}`, `pstack:comment-sicko`, and `pstack:panel-{swe,opus,sonnet,codex}`. SessionStart injects `PSTACK_ROUTE=/pstack:poteto-mode`. diff --git a/docs/usage-guide.md b/docs/usage-guide.md index 86624bf..2d8a4d2 100644 --- a/docs/usage-guide.md +++ b/docs/usage-guide.md @@ -44,6 +44,8 @@ Keep the verification skill with the project when delivery is authorized. Update [`/pstack:benchmark-checklist`](../skills/benchmark-checklist/SKILL.md) vets a number before reporting or acting on it. Comparisons require five interleaved runs per side, median and range, correct outputs, and proof that timed work happened. A requested ballpark can use one labeled run while retaining error and work checks. Missing evidence means inconclusive. Performance playbooks already apply this checklist. +Some bugs live on paths nobody drives: two retries that overlap, a lock that expires mid-write, a state change that arrives out of order. For code where such a bug is costly, use [`/pstack:create-formal-verification-skill`](../skills/create-formal-verification-skill/SKILL.md). The question picks the tool. TLA+ is the default for whether events can happen in a bad order. A verifier that runs on the code suits whether the code behaves for every input. When no verifier runs on the language, the agent says so and tests the real code with generated inputs. The plugin bundles no verifier, so the agent confirms the tool runs on this machine and asks before installing it. The check must fail on a broken variant, a finding stays a finding, and the generated skill under `.devin/skills/` records the covered code and the commit it last matched. After merges or refactors that skipped that skill, run [`/pstack:maintain-formal-verification-skill`](../skills/maintain-formal-verification-skill/SKILL.md). It updates the verification from the code, reruns it, and says whether each failure is drift or a bug. + ## Deliver in this session Request commits, pushes, or a PR explicitly. Opening a PR does not start babysitting. [`/pstack:babysit`](../skills/babysit/SKILL.md) handles checks and feedback in the current session. Merge remains with the operator. @@ -70,6 +72,8 @@ The help skill's [prompting reference](../skills/poteto-help/references/promptin Use `/pstack:in-your-own-words` to hear the goals and problem the agent understood. This explicit-user skill restates them without starting a workflow or adding a confirmation gate. -Use `/pstack:ketchup` to catch up since your previous message. Replies stay under 250 words and include older unresolved user decisions. Existing captures and available diagrams show status and before/after options. When the Devin host cannot render them, compact text includes the same facts and unknowns. The skill does not start an app, install a renderer, or post anything to produce a visual. +Use `/pstack:sharpen ` when you are unsure a prompt is aimed right. It hands back the prompt rewritten deeper, not bigger, with an outside check and your choices left open. It does not do the task. Send the rewrite yourself. + +Use `/pstack:ketchup` to catch up since your previous message. The story stays under 100 words. Every call waiting on you gets its own bullet with its link, what it changes, the evidence, the risk, and a pick, including older unresolved decisions, so a large batch makes a long reply instead of a cut list. Existing captures and available diagrams show status and before/after options. When the Devin host cannot render them, compact text includes the same facts and unknowns. The skill does not start an app, install a renderer, or post anything to produce a visual. Verification skills must launch a usable app from an empty data directory. Include migrations and seed data. Missing journey preconditions are failed checks, not a reason to weaken the journey. Proof from a stand-in must identify target setup steps it has not exercised. diff --git a/skills/create-formal-verification-skill/SKILL.md b/skills/create-formal-verification-skill/SKILL.md new file mode 100644 index 0000000..70f5620 --- /dev/null +++ b/skills/create-formal-verification-skill/SKILL.md @@ -0,0 +1,44 @@ +--- +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 and runs here. Use for /pstack: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." +triggers: + - user +--- + +# 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 under `.devin/skills/` 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. + +This plugin bundles no verifier. TLA+ needs Java and the TLA+ tools, and other verifiers have their own toolchains. Before you commit to a tool, confirm with `exec` that it runs on this machine, and record its version. Installing a toolchain changes the user's machine, so name the install command and get the user's approval first. If the tool cannot run here and the user does not approve an install, say so and use the generated-input fallback above. Never report a check as run when the tool did not run. + +## 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 `.devin/skills//SKILL.md`, with a `name` equal to its folder and a `description` that names the area and says when to use it. Devin shows the description in completions, and an agent decides from it when to load the skill. 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. Name the tool, its version, and how to install it. 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 `/pstack:maintain-formal-verification-skill` for bringing the verification back in line after changes that did not recheck it. Leave the new skill and its files uncommitted unless the user asked for delivery. diff --git a/skills/ketchup/SKILL.md b/skills/ketchup/SKILL.md index c3a5303..f19127e 100644 --- a/skills/ketchup/SKILL.md +++ b/skills/ketchup/SKILL.md @@ -1,13 +1,13 @@ --- name: ketchup -description: "Catch the user up on what changed in this chat since their last message, in a few plain sentences and small available visuals. Give each action item just enough context to make the call. Use for /pstack:ketchup." +description: "Catch the user up on what changed in this chat since their last message, in plain words and small available visuals. List every item waiting on them with what they need to decide it from the reply alone. Use for /pstack:ketchup." triggers: - user --- # Ketchup -Catch the user up on what changed in this chat since the last message they wrote before `/pstack: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 `/pstack: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 [`/pstack: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. @@ -15,26 +15,32 @@ Use [`/pstack:bro`](../bro/SKILL.md)'s voice, not its task: plain words, short s Keep this turn read-only. Make visuals only from facts and artifacts you already have. Do not change repository code or data, start an app or a job, or post anything to make them. Collect your own work since that message, subagent reports, and other messages in this chat. Check the current state of each PR, CI run, or agent this chat touched. Say which you could not check. Check each number against its source 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 without an 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 rendered screenshots, videos, or diagrams. Tables and text fallbacks count. When something is easier to grasp as a picture than as sentences, draw it if the host renders 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 rendered screenshots, videos, or diagrams, and shorter when less happened. Tables and text fallbacks count. 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 rendered 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 the existing screenshots and videos the work produced, then any diagram that explains a change, when the host renders them. 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". 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 existing detail. +Then list the action items as plain bullets, never as a diagram or box. 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 in a visual when rendering is available, 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. Otherwise compare them side by side in a visual when rendering is available, or as compact plain lines when it is not. ## Visuals +When something is easier to grasp as a picture than as sentences, draw it if the host renders 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 readable 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. A Markdown table is text, not a picture. Embed existing screenshots and video inline for visible changes when the host renders them, not only as links. If a visible change has no capture, mark its summary line "No screenshot yet," and say there what changed on screen. Never draw or generate a screen you did not capture, invent numbers, or link an artifact that does not exist. For other changes, use a diagram only when the current Devin host renders one. Mermaid suits how things connect when the host renders it. This plugin provides no chart or image tool and no visual rendering guarantee in the CLI. -When rendering is unavailable, say so in a few words, link the existing screenshots and videos, and give the same states, options, costs, and unknowns as compact plain lines within the word limit. Do not invoke an unshipped skill, install a tool, or start a service to satisfy the visual preference. +When rendering is unavailable, say so in a few words, link the existing screenshots and videos, and give the same states, options, costs, and unknowns as compact plain lines. Do not invoke an unshipped skill, install a tool, or start a service to satisfy the visual preference. diff --git a/skills/maintain-formal-verification-skill/SKILL.md b/skills/maintain-formal-verification-skill/SKILL.md new file mode 100644 index 0000000..a8609a5 --- /dev/null +++ b/skills/maintain-formal-verification-skill/SKILL.md @@ -0,0 +1,59 @@ +--- +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 /pstack:maintain-formal-verification-skill, \"is the model still true to the code\", or after merges and refactors that touched verified code without rechecking it." +triggers: + - user +--- + +# 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 `/pstack: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 verifier that is not installed on this machine is blocked, not passing. Name the install command and ask before installing it. + +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 under `.devin/skills/`, `.agents/skills/`, or `.windsurf/skills/` 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 `/pstack: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 with `exec` 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. + +Keep the verification updates in a change of their own, separate from any product fix. Stop at merge-ready. Do not commit, push, or open a PR unless the user asks. diff --git a/skills/poteto-help/SKILL.md b/skills/poteto-help/SKILL.md index 1caf6d4..1b6650e 100644 --- a/skills/poteto-help/SKILL.md +++ b/skills/poteto-help/SKILL.md @@ -27,6 +27,7 @@ Check the state that changes the answer, and mention it only when it does: - No `$HOME/.config/devin/pstack-models.md` means each role uses its skill's default profile unless another explicit configuration applies. - No `verify-*` skill or other app harness in the project means agents have no scripted way to drive the app. Mention `/pstack: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 `/pstack: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 `/pstack:maintain-formal-verification-skill` if the question touches that code. ## Get set up @@ -52,11 +53,11 @@ The default answer is `/pstack:poteto-mode`, which runs most of the others when |---|---| | Do any non-trivial task with rigor | [`/pstack:poteto-mode`](../poteto-mode/SKILL.md) | | Check that the agent understood the goals and the problem | [`/pstack:in-your-own-words`](../in-your-own-words/SKILL.md) | -| Aim a task higher before starting: more expert, more outcome-focused, not overspecified | [`/pstack: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 | [`/pstack:sharpen`](../sharpen/SKILL.md) | | Know how code works now, or where new code should live | [`/pstack:how`](../how/SKILL.md) | | Know why code is shaped this way, or where a number came from | [`/pstack:why`](../why/SKILL.md) | | Understand a change or subsystem, explained plainly | [`/pstack:teach`](../teach/SKILL.md) | -| Catch up on changes since their last message, in a few plain sentences and small available visuals | [`/pstack:ketchup`](../ketchup/SKILL.md) | +| Catch up on changes since their last message, in plain words and small available visuals, with every item waiting on them listed and decidable from the reply alone | [`/pstack:ketchup`](../ketchup/SKILL.md) | | Catch up on their own recent work on a topic | [`/pstack:recall`](../recall/SKILL.md) | | Know what a small diff could break outside itself | [`/pstack:blast-radius`](../blast-radius/SKILL.md) | | Settle types and module shape before code that crosses a function boundary | [`/pstack:architect`](../architect/SKILL.md) | @@ -71,6 +72,8 @@ The default answer is `/pstack:poteto-mode`, which runs most of the others when | Hear the last reply again in plain words | [`/pstack:bro`](../bro/SKILL.md) | | Give agents a scripted way to drive the app and prove behavior | [`/pstack:create-verification-skill`](../create-verification-skill/SKILL.md) | | Bring a verification skill and its feature map back in line with the app | [`/pstack:maintain-verification-skill`](../maintain-verification-skill/SKILL.md) | +| Formally verify a race, invariant, or other property that tests rarely reach | [`/pstack: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 | [`/pstack:maintain-formal-verification-skill`](../maintain-formal-verification-skill/SKILL.md) | | Vet a performance number before reporting or acting on it | [`/pstack:benchmark-checklist`](../benchmark-checklist/SKILL.md) | | Run a large or cross-cutting change, or one to review after stepping away | [`/pstack:figure-it-out`](../figure-it-out/SKILL.md) | | Keep a decision log during a run, and review it afterward | [`/pstack:show-me-your-work`](../show-me-your-work/SKILL.md) | @@ -105,6 +108,7 @@ Port boundaries: - `control-cli`, `control-ui`, `/create-skill`, and `/make-bot-ui` are not shipped here. Use the skill-authoring playbook for skill work. Detect an available UI or CLI adapter before promising visual proof. - Devin's `/loop ` is an interactive command that auto-reviews a diff. It is not an agent-callable timer or unattended scheduler. - Orchestrate is a `/pstack:poteto-mode` playbook, not a public `/orchestrate` skill. +- Upstream `/statechart` and `/ketchup-video` are not shipped here. They need a TLA+ toolchain with a chart renderer, or a video renderer, and Devin documents no inline image or video output in the CLI. Formal verification skills bundle no verifier; the agent confirms the tool runs on this machine and asks before installing one. ## Playbooks and principles diff --git a/skills/poteto-help/references/recipes.md b/skills/poteto-help/references/recipes.md index d583b11..ee5c8de 100644 --- a/skills/poteto-help/references/recipes.md +++ b/skills/poteto-help/references/recipes.md @@ -32,6 +32,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. ## Review and ship - `/pstack: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. +- `/pstack:create-formal-verification-skill prove holds in , even when interleave or retry.` After merges or refactors in that code: `/pstack:maintain-formal-verification-skill`. - `/pstack:swarm check every package under against its check script. one worker per package. one report.` - `/pstack:poteto-mode open the pr. small ordered commits, evidence in the description.` - `/pstack:poteto-mode babysit this pr. get it green.` For status only: `/pstack:poteto-mode check on pr . anything outstanding?` @@ -41,6 +42,7 @@ Swap in the real paths, skills, and done checks. Informal wording works. - `/pstack:poteto-mode run in a fresh worktree off . done means . bound this session to iterations. keep a decision log. at the bound, write resume.md with the remaining work.` - `/pstack:show-me-your-work catch me up on the completed run.` Read its Attention section first. +- `/pstack:ketchup` catches you up on this chat since your last message and lists every call that waits on you. - Autopilot-full and Autopilot-stack are cut from this port. Read [Delivery capability](../../poteto-mode/references/delivery-capability.md) for supported in-session alternatives. - `/pstack:reflect capture what we learned so the next run doesn't repeat it.` Approve only edits that change a future decision. - `/pstack:bro` restates the last reply in plain words. @@ -53,10 +55,10 @@ Swap in the real paths, skills, and done checks. Informal wording works. Use this to hear the goals and problem the agent understood. It does not add a confirmation gate to ordinary work. -## Aim the task higher +## Sharpen a prompt before you send it ```text -/pstack:sharpen +/pstack:sharpen ``` -The agent frames the task the way a top expert would, keeps one outside check, leaves your choices open, and then does the work. It does not hand back a rewritten prompt. +The agent names 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. It hands back your prompt rewritten to ask for that, leaves your choices open, and doesn't do the task. Send the rewrite when it reads right, for example with `/pstack:poteto-mode`. diff --git a/skills/reflect/SKILL.md b/skills/reflect/SKILL.md index 562c86d..8dfecf8 100644 --- a/skills/reflect/SKILL.md +++ b/skills/reflect/SKILL.md @@ -57,6 +57,8 @@ Present the full Accepted / Rejected / Backlog list and wait for explicit approv Backlog items go to whatever tracker this team already uses. Only Accepted waits. +Never edit a skill inside an installed plugin. Run `devin plugins info ` and read its Source line. A plugin installed from GitHub or a git URL is re-fetched by `devin plugins update`, which can replace local edits. A plugin installed with `--local` is linked to its source checkout, so an edit there changes that repository. Before approval, show each edit's destination. For a plugin skill, the default is a copy at `.devin/skills//` for this project or `~/.config/devin/skills//` for every project. After approval, copy the skill folder there and edit the copy. The copy is a separate skill invoked as `/`; `/:` keeps the unedited version. Edit a `--local` plugin's checkout only when the user names it as the destination. Never open a PR or push. + For each approved row, follow Routing: - Trivial existing-skill edit. Parent does it. @@ -66,7 +68,7 @@ For each approved row, follow Routing: ## 6. Summarize -- Edits applied. Path and one line. +- Edits applied. Destination path and one line. - New skills created. Path and one line. - Backlog filed. Title. - Dropped. One line per rejection plus the synthesizer reason. diff --git a/skills/sharpen/SKILL.md b/skills/sharpen/SKILL.md index 5c7c571..d4e45ce 100644 --- a/skills/sharpen/SKILL.md +++ b/skills/sharpen/SKILL.md @@ -1,8 +1,19 @@ --- 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 /pstack:sharpen." +description: "Make a task deeper, not bigger, then rewrite the prompt. Returns the rewrite and does not do the task. Use for /pstack:sharpen." triggers: - user --- -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. + +Hand back only the rewritten prompt. Do not start the task, edit files, or dispatch workers. I will send the rewrite myself, for example with `/pstack:poteto-mode`. diff --git a/skills/typescript-best-practices/SKILL.md b/skills/typescript-best-practices/SKILL.md index 40c2aa0..294d090 100644 --- a/skills/typescript-best-practices/SKILL.md +++ b/skills/typescript-best-practices/SKILL.md @@ -10,7 +10,7 @@ Read `skills/principle-type-system-discipline/SKILL.md` first. This skill ground | 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`. `any` disables type checking everywhere it touches. | diff --git a/skills/typescript-best-practices/references/patterns.md b/skills/typescript-best-practices/references/patterns.md index c4bf5c5..8c3226a 100644 --- a/skills/typescript-best-practices/references/patterns.md +++ b/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/port-contracts.test.mjs b/tests/port-contracts.test.mjs index e51ed7b..1b35eba 100644 --- a/tests/port-contracts.test.mjs +++ b/tests/port-contracts.test.mjs @@ -1,5 +1,5 @@ import assert from 'node:assert/strict'; -import { mkdtempSync, readFileSync, writeFileSync, rmSync } from 'node:fs'; +import { mkdtempSync, readFileSync, readdirSync, writeFileSync, rmSync } from 'node:fs'; import { tmpdir } from 'node:os'; import { dirname, join, resolve } from 'node:path'; import { fileURLToPath } from 'node:url'; @@ -61,7 +61,7 @@ test('interleaved run documentation assigns boundaries and supersedes history', }); test('portable skills retain user activation and numeric principle model activation', () => { - for (const name of ['correct', 'benchmark-checklist', 'ketchup', 'in-your-own-words', 'sharpen']) { + for (const name of ['correct', 'benchmark-checklist', 'ketchup', 'in-your-own-words', 'sharpen', 'create-formal-verification-skill', 'maintain-formal-verification-skill']) { const text = read(`skills/${name}/SKILL.md`); assert.match(text, new RegExp(`^name: ${name}$`, 'm')); assert.match(text, /triggers:\n - user/); @@ -130,3 +130,35 @@ test('0.15.25 port keeps ketchup fallback and reasoning-style principles', () => assert.match(read(`skills/${name}/SKILL.md`), /triggers:\n - model/); } }); + +test('every skill is named after its folder', () => { + for (const name of readdirSync(join(root, 'skills'))) { + assert.match(read(`skills/${name}/SKILL.md`), new RegExp(`^---\\n(?:[^\\n]*\\n)*?name: ${name}\\n`), name); + } +}); + +test('e73df47 port keeps Devin paths, honest tool limits, and local-only reflect edits', () => { + const sharpen = read('skills/sharpen/SKILL.md'); + assert.match(sharpen, /rewrite my prompt to ask for exactly that/); + assert.match(sharpen, /Do not start the task/); + assert.doesNotMatch(sharpen, /then do the work/); + const ketchup = read('skills/ketchup/SKILL.md'); + assert.match(ketchup, /Never cut items or shrink them to stay under a word count/); + assert.match(ketchup, /Give each item's risk even when it is low/); + assert.doesNotMatch(ketchup, /well under 150 words, not counting rendered screenshots/); + for (const name of ['create-formal-verification-skill', 'maintain-formal-verification-skill']) { + const text = read(`skills/${name}/SKILL.md`); + assert.match(text, /\.devin\/skills\//); + assert.match(text, /ask(?:s)? before installing|get the user's approval first/); + assert.doesNotMatch(text, /\.cursor|\/statechart|disable-model-invocation/); + } + assert.match(read('skills/create-formal-verification-skill/SKILL.md'), /TLA\+ is the default/); + assert.match(read('skills/create-formal-verification-skill/SKILL.md'), /test the real code with generated inputs/); + const reflect = read('skills/reflect/SKILL.md'); + assert.match(reflect, /Never edit a skill inside an installed plugin/); + assert.match(reflect, /~\/\.config\/devin\/skills\/\//); + assert.match(reflect, /Never open a PR or push/); + assert.doesNotMatch(reflect, /plugins\/cache/); + assert.doesNotMatch(read('skills/typescript-best-practices/references/patterns.md'), /as AgentId/); + for (const cut of ['statechart', 'ketchup-video']) assert.throws(() => read(`skills/${cut}/SKILL.md`)); +});