Release action

.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

.vscode/mcp.json

@@ -0,0 +1,12 @@
+{
+	"inputs": [],
+	"servers": {
+		"lean-lsp": {
+			"type": "stdio",
+			"command": "uvx",
+			"args": [
+				"lean-lsp-mcp"
+			]
+		}
+	}
+}

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
 

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"