From 87028619453334bc1b2b3dbb3c64463cd119a7c4 Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Fri, 20 Feb 2026 23:35:32 +1100
Subject: [PATCH] chore: enable leanprover/skills plugin for Claude Code
 (#12609)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR registers the
[leanprover/skills](https://github.com/leanprover/skills) plugin
marketplace in `.claude/settings.json` so that Claude Code users working
on lean4 are automatically prompted to install it.

Also un-ignores `.claude/settings.json` in `.gitignore` — the blanket
`settings.json` rule was blocking it from being tracked.

🤖 Prepared with Claude Code
---
 .claude/settings.json | 13 +++++++++++++
 .gitignore            |  1 +
 2 files changed, 14 insertions(+)
 create mode 100644 .claude/settings.json

diff --git a/.claude/settings.json b/.claude/settings.json
new file mode 100644
index 0000000000..eddea20b83
--- /dev/null
+++ b/.claude/settings.json
@@ -0,0 +1,13 @@
+{
+  "extraKnownMarketplaces": {
+    "leanprover": {
+      "source": {
+        "source": "github",
+        "repo": "leanprover/skills"
+      }
+    }
+  },
+  "enabledPlugins": {
+    "lean@leanprover": true
+  }
+}
diff --git a/.gitignore b/.gitignore
index f4625868ad..447cc92071 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,6 +18,7 @@ compile_commands.json
 *.idea
 tasks.json
 settings.json
+!.claude/settings.json
 .gdb_history
 .vscode/*
 script/__pycache__