From c1287a50f0727035e4928b5e4882c5a529c6e029 Mon Sep 17 00:00:00 2001 From: Thomas Gibson-Robinson Date: Sat, 19 Sep 2026 16:22:23 +0100 Subject: [PATCH] Add Agent Plugins 1.0 manifests as well --- .claude-plugin/marketplace.json | 2 +- .github/scripts/github_app_token.py | 7 +- .github/scripts/sync_plugin.py | 36 +++--- .github/scripts/validate.py | 142 ++++++++++++++++++++++++ .github/workflows/sync-plugin.yml | 63 +++++++++-- .github/workflows/validate.yml | 40 +++++++ README.md | 40 +++++++ popili-beta/.claude-plugin/plugin.json | 2 +- popili-beta/.lsp.json | 2 +- popili-beta/.mcp.json | 2 +- popili-beta/com.github.copilot/lsp.json | 11 ++ popili-beta/mcp.json | 10 ++ popili-beta/plugin.json | 18 +++ popili/.claude-plugin/plugin.json | 2 +- popili/.lsp.json | 2 +- popili/.mcp.json | 2 +- popili/com.github.copilot/lsp.json | 11 ++ popili/mcp.json | 10 ++ popili/plugin.json | 18 +++ 19 files changed, 382 insertions(+), 38 deletions(-) create mode 100644 .github/scripts/validate.py create mode 100644 .github/workflows/validate.yml create mode 100644 README.md create mode 100644 popili-beta/com.github.copilot/lsp.json create mode 100644 popili-beta/mcp.json create mode 100644 popili-beta/plugin.json create mode 100644 popili/com.github.copilot/lsp.json create mode 100644 popili/mcp.json create mode 100644 popili/plugin.json diff --git a/.claude-plugin/marketplace.json b/.claude-plugin/marketplace.json index bd0c621..9a61188 100644 --- a/.claude-plugin/marketplace.json +++ b/.claude-plugin/marketplace.json @@ -8,7 +8,7 @@ { "name": "popili", "source": "./popili", - "description": "Allows the Popili formal verification tools to be used on Coco programs within Claude Code" + "description": "Popili formal verification and code intelligence for the Coco language" }, { "name": "popili-beta", diff --git a/.github/scripts/github_app_token.py b/.github/scripts/github_app_token.py index e68658d..49356a4 100755 --- a/.github/scripts/github_app_token.py +++ b/.github/scripts/github_app_token.py @@ -67,7 +67,10 @@ def get_installation_token(jwt: str, installation_id: str) -> str: }, ) with urllib.request.urlopen(req) as resp: - return json.loads(resp.read())['token'] + token = json.loads(resp.read())['token'] + if not isinstance(token, str): + sys.exit(f"Error: GitHub returned a {type(token).__name__} installation token, expected a string") + return token def env(name: str) -> str: @@ -77,7 +80,7 @@ def env(name: str) -> str: return value -def main(): +def main() -> None: jwt = create_jwt( app_id=env('COCOTEC_BOT_APP_ID'), project=env('GCP_KMS_PROJECT'), diff --git a/.github/scripts/sync_plugin.py b/.github/scripts/sync_plugin.py index b0326bd..abf4457 100644 --- a/.github/scripts/sync_plugin.py +++ b/.github/scripts/sync_plugin.py @@ -1,11 +1,7 @@ #!/usr/bin/env python3 -"""Download and extract the Popili Claude Code plugin from dl.cocotec.io. +"""Download a released plugin version and extract it over the right channel directory. -Determines the target plugin directory (popili or popili-beta) based on the -version string, downloads the plugin zip, extracts it, and validates that -the plugin.json version was stamped correctly. - -Prints the plugin directory name to stdout for use by the workflow. +Prints the plugin directory name to stdout for the workflow. """ import argparse @@ -16,6 +12,10 @@ import zipfile from pathlib import Path +from validate import AGENT_MANIFEST, validate_plugin + +ARCHIVE = "popili-agent-plugin.zip" + def determine_channel(version: str) -> str: """Return the plugin directory name based on version string.""" @@ -24,15 +24,15 @@ def determine_channel(version: str) -> str: return "popili" -def main(): +def main() -> None: parser = argparse.ArgumentParser() parser.add_argument("--version", required=True) args = parser.parse_args() - zip_path = Path("claude-code-plugin.zip") + zip_path = Path(ARCHIVE) target = Path(determine_channel(args.version)) - url = f"https://dl.cocotec.io/popili/archive/{args.version}/claude-code-plugin.zip" + url = f"https://dl.cocotec.io/popili/archive/{args.version}/{ARCHIVE}" print(f"Downloading {url}", file=sys.stderr) urllib.request.urlretrieve(url, zip_path) @@ -40,20 +40,16 @@ def main(): shutil.rmtree(target) target.mkdir() - with zipfile.ZipFile(zip_path) as zf: - zf.extractall(target) + with zipfile.ZipFile(zip_path) as archive: + archive.extractall(target) zip_path.unlink() - plugin_json = target / ".claude-plugin" / "plugin.json" - if not plugin_json.exists(): - sys.exit("ERROR: plugin.json not found in extracted zip") - - with open(plugin_json) as f: - version = json.load(f)["version"] - - if version == "{STABLE_BUILD_SEMANTIC_VERSION}": - sys.exit("ERROR: plugin.json still contains template variable") + if problems := validate_plugin(target): + for problem in problems: + print(f"ERROR: {problem}", file=sys.stderr) + sys.exit(f"{ARCHIVE} for {args.version} is not loadable; refusing to open a pull request") + version = json.loads((target / AGENT_MANIFEST).read_text())["version"] print(f"Plugin version: {version}", file=sys.stderr) print(target) diff --git a/.github/scripts/validate.py b/.github/scripts/validate.py new file mode 100644 index 0000000..ebe1f93 --- /dev/null +++ b/.github/scripts/validate.py @@ -0,0 +1,142 @@ +#!/usr/bin/env python3 +"""Check the marketplace catalogue and that each plugin directory is complete. + +Run with no arguments to check every plugin the marketplace lists. Import `validate_plugin` to check +a single directory. + +Deliberately thin: manifest contents are validated before release, so this is a smoke test, not a +second implementation of the Agent Plugins spec. +""" + +import json +from pathlib import Path +import sys +from typing import Any + +Json = dict[str, Any] + +PLUGIN_SCHEMA = "https://agent-plugins.org/schemas/1.0.0/plugin.schema.json" +MCP_SCHEMA = "https://agent-plugins.org/schemas/1.0.0/mcp.schema.json" + +MARKETPLACE = Path(".claude-plugin") / "marketplace.json" + +# Claude Code reads the first, every other client the second. +CLAUDE_MANIFEST = Path(".claude-plugin") / "plugin.json" +AGENT_MANIFEST = Path("plugin.json") + +# Checked for presence only; a partial extraction or a stray deletion is what this catches. +EXPECTED_FILES = ( + Path(".mcp.json"), + Path(".lsp.json"), + Path("com.github.copilot") / "lsp.json", +) + + +def read_json(path: Path, problems: list[str]) -> Json | None: + if not path.exists(): + problems.append(f"{path}: missing") + return None + try: + parsed = json.loads(path.read_text()) + except json.JSONDecodeError as error: + problems.append(f"{path}: invalid JSON: {error}") + return None + if not isinstance(parsed, dict): + problems.append(f"{path}: must contain a JSON object, found {type(parsed).__name__}") + return None + return parsed + + +def validate_plugin(root: Path) -> list[str]: + """Return every problem found in the plugin directory at `root`; empty means it looks installable.""" + problems: list[str] = [] + + for relative in EXPECTED_FILES: + if not (root / relative).is_file(): + problems.append(f"{root / relative}: missing") + + agent_manifest = read_json(root / AGENT_MANIFEST, problems) + claude_manifest = read_json(root / CLAUDE_MANIFEST, problems) + + if agent_manifest is not None and claude_manifest is not None: + version = agent_manifest.get("version") + if not isinstance(version, str): + problems.append(f"{root / AGENT_MANIFEST}: no version string") + elif "{" in version: + problems.append(f"{root / AGENT_MANIFEST}: unsubstituted template variable {version!r}") + if version != claude_manifest.get("version"): + problems.append( + f"{root}: manifests disagree on version: {AGENT_MANIFEST} has {version!r}, " + f"{CLAUDE_MANIFEST} has {claude_manifest.get('version')!r}" + ) + + # The field that decides whether a client outside Claude Code loads this at all. + if agent_manifest is not None and agent_manifest.get("$schema") != PLUGIN_SCHEMA: + problems.append( + f"{root / AGENT_MANIFEST}: $schema is {agent_manifest.get('$schema')!r}, must be exactly " + f"{PLUGIN_SCHEMA!r}" + ) + + portable_mcp = read_json(root / "mcp.json", problems) + if portable_mcp is not None and portable_mcp.get("$schema") != MCP_SCHEMA: + problems.append(f"{root}/mcp.json: $schema is {portable_mcp.get('$schema')!r}, must be exactly {MCP_SCHEMA!r}") + + return problems + + +def validate_marketplace() -> tuple[list[str], list[Path]]: + """A bad entry installs nothing while every plugin directory looks fine.""" + problems: list[str] = [] + marketplace = read_json(MARKETPLACE, problems) + if marketplace is None: + return problems, [] + + entries = marketplace.get("plugins") + if not isinstance(entries, list): + problems.append(f"{MARKETPLACE}: plugins must be a list") + return problems, [] + + roots: list[Path] = [] + seen: set[str] = set() + for entry in entries: + if not isinstance(entry, dict): + problems.append(f"{MARKETPLACE}: every plugins entry must be an object") + continue + name = entry.get("name") + if not isinstance(name, str) or not name: + problems.append(f"{MARKETPLACE}: an entry has no name") + continue + if name in seen: + problems.append(f"{MARKETPLACE}: duplicate plugin name {name!r}") + seen.add(name) + if not entry.get("description"): + problems.append(f"{MARKETPLACE}: {name} has no description") + + source = entry.get("source") + if not isinstance(source, str): + problems.append(f"{MARKETPLACE}: {name} has no source path") + continue + root = Path(source) + if not root.is_dir(): + problems.append(f"{MARKETPLACE}: {name} points at {source}, which is not a directory") + else: + roots.append(root) + + return problems, roots + + +def main() -> None: + problems, roots = validate_marketplace() + for root in roots: + problems += validate_plugin(root) + + if problems: + for problem in problems: + print(f"FAIL: {problem}", file=sys.stderr) + sys.exit(1) + + print(f"{len(roots)} plugin(s) validated: {', '.join(str(root) for root in roots)}") + + +if __name__ == "__main__": + main() diff --git a/.github/workflows/sync-plugin.yml b/.github/workflows/sync-plugin.yml index ca2d091..4542abb 100644 --- a/.github/workflows/sync-plugin.yml +++ b/.github/workflows/sync-plugin.yml @@ -9,9 +9,16 @@ on: permissions: contents: write id-token: write + +# Queue rather than cancel: every release is meant to produce a sync. +concurrency: + group: sync-plugin + cancel-in-progress: false + jobs: sync: runs-on: ubuntu-latest + timeout-minutes: 15 steps: - uses: actions/checkout@v6 @@ -39,24 +46,62 @@ jobs: GCP_KMS_KEY: ${{ secrets.GCP_KMS_KEY }} GCP_KMS_KEY_VERSION: ${{ secrets.GCP_KMS_KEY_VERSION }} + # Via env, not `${{ }}` interpolation, which bash would see as code. - name: Sync plugin id: sync + shell: bash run: | - PLUGIN_DIR=$(python3 .github/scripts/sync_plugin.py --version ${{ inputs.version }}) - echo "plugin_dir=$PLUGIN_DIR" >> $GITHUB_OUTPUT + PLUGIN_DIR=$(python3 .github/scripts/sync_plugin.py --version "$VERSION") + echo "plugin_dir=$PLUGIN_DIR" >> "$GITHUB_OUTPUT" + env: + VERSION: ${{ inputs.version }} - name: Create Pull Request + shell: bash run: | - PLUGIN_DIR="${{ steps.sync.outputs.plugin_dir }}" - VERSION="${{ inputs.version }}" - git checkout -b "sync/${PLUGIN_DIR}-${VERSION}" + set -euo pipefail + BRANCH="sync/${PLUGIN_DIR}-${VERSION}" + git config user.name "cocotec-automation[bot]" git config user.email "244153713+cocotec-automation[bot]@users.noreply.github.com" + git checkout -b "$BRANCH" git add "$PLUGIN_DIR" + + # Re-dispatching an already-synced version is normal. + if git diff --cached --quiet; then + echo "::notice::${PLUGIN_DIR} is already at ${VERSION}; nothing to sync." + echo "\`${PLUGIN_DIR}\` already at \`${VERSION}\` — no changes." >> "$GITHUB_STEP_SUMMARY" + exit 0 + fi + git commit --message "${PLUGIN_DIR}: update plugin to ${VERSION}" - git push --set-upstream origin HEAD - gh pr create --base main \ - --title "${PLUGIN_DIR}: update plugin to ${VERSION}" \ - --body "Automated update of the ${PLUGIN_DIR} plugin to version ${VERSION}." + # Bot-owned branch; a force can only discard a previous attempt at this sync. + git push --force --set-upstream origin "$BRANCH" + + PR=$(gh pr list --head "$BRANCH" --state open --json number --jq '.[0].number // empty') + if [ -n "$PR" ]; then + URL=$(gh pr view "$PR" --json url --jq .url) + else + # printf: a block scalar leaks indentation and a heredoc eats the backticks. + BODY=$(printf '%s\n' \ + "Merging publishes \`${VERSION}\` to everyone installing \`${PLUGIN_DIR}@cocotec\`." \ + "" \ + "Auto-merge is on, so approving this is enough.") + URL=$(gh pr create --base main \ + --title "${PLUGIN_DIR}: update plugin to ${VERSION}" \ + --body "$BODY") + PR="$URL" + fi + + # Non-fatal: the pull request exists either way and can be merged by hand. + if MERGE_ERROR=$(gh pr merge "$PR" --auto --squash 2>&1); then + echo "::notice::Auto-merge enabled; merges once approved." + else + echo "::warning::Could not enable auto-merge on ${URL}: ${MERGE_ERROR}" + fi + + echo "Synced \`${PLUGIN_DIR}\` to \`${VERSION}\`: ${URL}" >> "$GITHUB_STEP_SUMMARY" env: GITHUB_TOKEN: ${{ steps.generate_token.outputs.token }} + PLUGIN_DIR: ${{ steps.sync.outputs.plugin_dir }} + VERSION: ${{ inputs.version }} diff --git a/.github/workflows/validate.yml b/.github/workflows/validate.yml new file mode 100644 index 0000000..5e76077 --- /dev/null +++ b/.github/workflows/validate.yml @@ -0,0 +1,40 @@ +name: Validate +on: + pull_request: + push: + branches: [main] + merge_group: + +permissions: + contents: read + +concurrency: + group: validate-${{ github.ref }} + cancel-in-progress: true + +jobs: + # `build` is the required check in the ruleset. + build: + runs-on: ubuntu-latest + timeout-minutes: 5 + steps: + - uses: actions/checkout@v6 + + - name: Validate plugins + run: python3 .github/scripts/validate.py + + - name: Compile scripts + run: python3 -m compileall -q .github/scripts + + # Not the required check: `build` stays stdlib-only so an outage upstream cannot block a sync. + typecheck: + runs-on: ubuntu-latest + timeout-minutes: 5 + steps: + - uses: actions/checkout@v6 + + - name: Typecheck scripts + # Run from inside the directory so `import validate` resolves. Pinned: --strict gains checks. + run: | + pip install --quiet mypy==2.3.1 + cd .github/scripts && mypy --strict . diff --git a/README.md b/README.md new file mode 100644 index 0000000..14546a4 --- /dev/null +++ b/README.md @@ -0,0 +1,40 @@ +# Cocotec agent plugins + +This is a plugin marketplace containing plugins to integrate the [Popili](https://cocotec.io/popili) language and MCP +servers into coding agents, enabling them to typecheck, navigate and formally verify Coco programs. + +| Plugin | Channel | +| ------------- | --------------------------- | +| `popili` | Stable releases | +| `popili-beta` | Beta and release candidates | + +Install only one as both channels declare the same MCP and language server names. + +## Install + +```bash +# Claude Code +claude plugin marketplace add cocotec/agent-plugins +claude plugin install popili@cocotec + +# Codex CLI +codex plugin marketplace add cocotec/agent-plugins +codex plugin add popili@cocotec + +# GitHub Copilot CLI +copilot plugin marketplace add cocotec/agent-plugins +copilot plugin install popili@cocotec +``` + +The plugin runs `popili`, so it needs the Popili CLI on your `PATH`; get it from +[cocotec.io/downloads](https://cocotec.io/downloads/). Under Claude Code you can point at a specific file with +`POPILI_PATH` instead. + +| Client | MCP | LSP | +| --------------- | --- | ----------------------------------- | +| Claude Code | ✅ | ✅ | +| Codex | ✅ | n/a — Codex has no LSP support | +| GitHub Copilot | ✅ | ✅ | + +Each plugin ships both an [Agent Plugins 1.0](https://agent-plugins.org/specification) manifest and +a Claude Code one. diff --git a/popili-beta/.claude-plugin/plugin.json b/popili-beta/.claude-plugin/plugin.json index 965404c..9237cab 100644 --- a/popili-beta/.claude-plugin/plugin.json +++ b/popili-beta/.claude-plugin/plugin.json @@ -1,6 +1,6 @@ { "name": "popili", - "description": "Coco formal verification tools — language server and MCP integration for Popili", + "description": "Popili formal verification and code intelligence for the Coco language", "version": "0.1.0", "author": { "name": "Cocotec" diff --git a/popili-beta/.lsp.json b/popili-beta/.lsp.json index dd4cf6a..e00c9ea 100644 --- a/popili-beta/.lsp.json +++ b/popili-beta/.lsp.json @@ -1,7 +1,7 @@ { "popili": { "command": "${POPILI_PATH:-popili}", - "args": ["serve-lsp"], + "args": ["serve-lsp", "--shared"], "extensionToLanguage": { ".coco": "coco" } diff --git a/popili-beta/.mcp.json b/popili-beta/.mcp.json index 15d74de..5b55c70 100644 --- a/popili-beta/.mcp.json +++ b/popili-beta/.mcp.json @@ -3,7 +3,7 @@ "popili": { "type": "stdio", "command": "${POPILI_PATH:-popili}", - "args": ["serve-mcp"] + "args": ["serve-mcp", "--shared"] } } } diff --git a/popili-beta/com.github.copilot/lsp.json b/popili-beta/com.github.copilot/lsp.json new file mode 100644 index 0000000..0492950 --- /dev/null +++ b/popili-beta/com.github.copilot/lsp.json @@ -0,0 +1,11 @@ +{ + "lspServers": { + "popili": { + "command": "popili", + "args": ["serve-lsp", "--shared"], + "fileExtensions": { + ".coco": "coco" + } + } + } +} diff --git a/popili-beta/mcp.json b/popili-beta/mcp.json new file mode 100644 index 0000000..42ef8a5 --- /dev/null +++ b/popili-beta/mcp.json @@ -0,0 +1,10 @@ +{ + "$schema": "https://agent-plugins.org/schemas/1.0.0/mcp.schema.json", + "mcpServers": { + "popili": { + "type": "stdio", + "command": "popili", + "args": ["serve-mcp", "--shared"] + } + } +} diff --git a/popili-beta/plugin.json b/popili-beta/plugin.json new file mode 100644 index 0000000..8e39f88 --- /dev/null +++ b/popili-beta/plugin.json @@ -0,0 +1,18 @@ +{ + "$schema": "https://agent-plugins.org/schemas/1.0.0/plugin.schema.json", + "name": "popili", + "description": "Popili formal verification and code intelligence for the Coco language", + "version": "0.1.0", + "author": { + "name": "Cocotec", + "email": "support@cocotec.io", + "url": "https://cocotec.io" + }, + "homepage": "https://cocotec.io/popili", + "keywords": [ + "coco", + "popili", + "formal-verification", + "model-checking" + ] +} diff --git a/popili/.claude-plugin/plugin.json b/popili/.claude-plugin/plugin.json index 965404c..9237cab 100644 --- a/popili/.claude-plugin/plugin.json +++ b/popili/.claude-plugin/plugin.json @@ -1,6 +1,6 @@ { "name": "popili", - "description": "Coco formal verification tools — language server and MCP integration for Popili", + "description": "Popili formal verification and code intelligence for the Coco language", "version": "0.1.0", "author": { "name": "Cocotec" diff --git a/popili/.lsp.json b/popili/.lsp.json index dd4cf6a..e00c9ea 100644 --- a/popili/.lsp.json +++ b/popili/.lsp.json @@ -1,7 +1,7 @@ { "popili": { "command": "${POPILI_PATH:-popili}", - "args": ["serve-lsp"], + "args": ["serve-lsp", "--shared"], "extensionToLanguage": { ".coco": "coco" } diff --git a/popili/.mcp.json b/popili/.mcp.json index 15d74de..5b55c70 100644 --- a/popili/.mcp.json +++ b/popili/.mcp.json @@ -3,7 +3,7 @@ "popili": { "type": "stdio", "command": "${POPILI_PATH:-popili}", - "args": ["serve-mcp"] + "args": ["serve-mcp", "--shared"] } } } diff --git a/popili/com.github.copilot/lsp.json b/popili/com.github.copilot/lsp.json new file mode 100644 index 0000000..0492950 --- /dev/null +++ b/popili/com.github.copilot/lsp.json @@ -0,0 +1,11 @@ +{ + "lspServers": { + "popili": { + "command": "popili", + "args": ["serve-lsp", "--shared"], + "fileExtensions": { + ".coco": "coco" + } + } + } +} diff --git a/popili/mcp.json b/popili/mcp.json new file mode 100644 index 0000000..42ef8a5 --- /dev/null +++ b/popili/mcp.json @@ -0,0 +1,10 @@ +{ + "$schema": "https://agent-plugins.org/schemas/1.0.0/mcp.schema.json", + "mcpServers": { + "popili": { + "type": "stdio", + "command": "popili", + "args": ["serve-mcp", "--shared"] + } + } +} diff --git a/popili/plugin.json b/popili/plugin.json new file mode 100644 index 0000000..8e39f88 --- /dev/null +++ b/popili/plugin.json @@ -0,0 +1,18 @@ +{ + "$schema": "https://agent-plugins.org/schemas/1.0.0/plugin.schema.json", + "name": "popili", + "description": "Popili formal verification and code intelligence for the Coco language", + "version": "0.1.0", + "author": { + "name": "Cocotec", + "email": "support@cocotec.io", + "url": "https://cocotec.io" + }, + "homepage": "https://cocotec.io/popili", + "keywords": [ + "coco", + "popili", + "formal-verification", + "model-checking" + ] +}