From fb4b7056611e8fa52ab997c15581c311a6dbbaec Mon Sep 17 00:00:00 2001
From: suzuki <casek2703@gmail.com>
Date: Thu, 1 Jan 2026 04:56:25 +0000
Subject: [PATCH 1/3] refactor: bring leanOptions outside lean_lib

---
 lakefile.toml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/lakefile.toml b/lakefile.toml
index 70ece93..23ffae1 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -2,14 +2,16 @@ name = "Project"
 version = "0.1.0"
 defaultTargets = ["Project"]
 
+[leanOptions]
+warningAsError = true
+pp.unicode.fun = true
+autoImplicit = false
+relaxedAutoImplicit = false
+linter.mathlibStandardSet = true
+linter.style.longLine = false
+
 [[lean_lib]]
 name = "Project"
-leanOptions.warningAsError = true
-leanOptions.pp.unicode.fun = true
-leanOptions.autoImplicit = false
-leanOptions.relaxedAutoImplicit = false
-leanOptions.linter.mathlibStandardSet = true
-leanOptions.linter.style.longLine = false
 
 [[require]]
 name = "mathlib"

From 7eb0fc910a3a3a5fa95f3204b87e4b54bbc0c2c6 Mon Sep 17 00:00:00 2001
From: suzuki <casek2703@gmail.com>
Date: Thu, 1 Jan 2026 04:56:43 +0000
Subject: [PATCH 2/3] chore: add mcp.json

---
 .vscode/mcp.json | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 .vscode/mcp.json

diff --git a/.vscode/mcp.json b/.vscode/mcp.json
new file mode 100644
index 0000000..7b31e08
--- /dev/null
+++ b/.vscode/mcp.json
@@ -0,0 +1,12 @@
+{
+	"inputs": [],
+	"servers": {
+		"lean-lsp": {
+			"type": "stdio",
+			"command": "uvx",
+			"args": [
+				"lean-lsp-mcp"
+			]
+		}
+	}
+}

From 2ae36da8e05005afcf2e33de914a3aa115617241 Mon Sep 17 00:00:00 2001
From: suzuki <casek2703@gmail.com>
Date: Thu, 1 Jan 2026 04:57:01 +0000
Subject: [PATCH 3/3] ci:  add release workflow

---
 .github/workflows/release-lean.yml | 54 ++++++++++++++++++++++++++++++
 README.md                          | 13 +++----
 2 files changed, 61 insertions(+), 6 deletions(-)
 create mode 100644 .github/workflows/release-lean.yml

diff --git a/.github/workflows/release-lean.yml b/.github/workflows/release-lean.yml
new file mode 100644
index 0000000..6c3d280
--- /dev/null
+++ b/.github/workflows/release-lean.yml
@@ -0,0 +1,54 @@
+name: Release Lean
+
+on:
+  pull_request:
+    types: [closed]
+    branches:
+      - main
+    paths:
+      - lean-toolchain
+
+jobs:
+  release:
+    if: github.event.pull_request.merged == true
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Determine current Lean tag from lean-toolchain
+        id: current
+        shell: bash
+        run: |
+          set -euo pipefail
+          toolchain="$(cat lean-toolchain)"
+          tag="${toolchain##*:}"
+          if [[ -z "$tag" ]]; then
+            echo "Failed to parse lean-toolchain: $toolchain" >&2
+            exit 1
+          fi
+          echo "tag=$tag" >> "$GITHUB_OUTPUT"
+
+      - name: Check if tag already exists
+        id: tag_exists
+        shell: bash
+        run: |
+          if git tag -l "${{ steps.current.outputs.tag }}" | grep -q .; then
+            echo "exists=true" >> "$GITHUB_OUTPUT"
+            echo "Tag '${{ steps.current.outputs.tag }}' already exists; skipping release."
+          else
+            echo "exists=false" >> "$GITHUB_OUTPUT"
+          fi
+
+      - name: Create GitHub Release
+        if: steps.tag_exists.outputs.exists != 'true'
+        uses: softprops/action-gh-release@v2
+        with:
+          tag_name: ${{ steps.current.outputs.tag }}
+          target_commitish: ${{ github.sha }}
+          prerelease: ${{ contains(steps.current.outputs.tag, '-') }}
+          generate_release_notes: true
diff --git a/README.md b/README.md
index 102f2b8..f88a231 100644
--- a/README.md
+++ b/README.md
@@ -14,12 +14,13 @@ Build completed successfully (498 jobs).
 ## How to use
 
 1. Create a repository from this template.
-2. Confirm lint settings in `package.json`, `.lefthook/`, and `lefthook.yml`.
-3. Remove `Project.lean` and `Project/`.
-4. Make your project files, then update `lakefile.toml`.
-5. Bump lean version in `.devcontainer/Dockerfile`, `lakefile.toml`, and `lean-toolchain`.
-6. Reomve `lake-manifest.json` and `.lake/`.
-7. Execute `lake exe cache get`.
+2. Confirm github workflows in `.github/workflows/`.
+3. Confirm lint settings in `package.json`, `.lefthook/`, and `lefthook.yml`.
+4. Remove `Project.lean` and `Project/`.
+5. Make your project files, then update `lakefile.toml`.
+6. Bump lean version in `.devcontainer/Dockerfile`, `lakefile.toml`, and `lean-toolchain`.
+7. Reomve `lake-manifest.json` and `.lake/`.
+8. Execute `lake exe cache get`.
 
 ## Recommend to use