ci: automate tagged releases

Author: Qiu233

.github/workflows/release.yml

@@ -0,0 +1,122 @@
+name: Release
+
+on:
+  workflow_dispatch:
+    inputs:
+      tag:
+        description: Release tag matching the package version (for example, v0.1.0)
+        required: true
+        type: string
+
+permissions:
+  contents: read
+
+concurrency:
+  group: release-${{ inputs.tag }}
+  cancel-in-progress: false
+
+jobs:
+  validate:
+    name: Validate release
+    if: github.ref == 'refs/heads/master'
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - uses: leanprover/lean-action@v1
+        with:
+          build-args: Binary Test
+          check-reservoir-eligibility: true
+
+      - name: Verify release tag
+        env:
+          RELEASE_TAG: ${{ inputs.tag }}
+        run: |
+          package_version="$(lake reservoir-config | jq -r '.version')"
+          if [[ "${RELEASE_TAG}" != "v${package_version}" ]]; then
+            echo "release tag ${RELEASE_TAG} does not match package version v${package_version}" >&2
+            exit 1
+          fi
+          if git ls-remote --exit-code --tags origin "refs/tags/${RELEASE_TAG}" >/dev/null 2>&1; then
+            echo "release tag ${RELEASE_TAG} already exists" >&2
+            exit 1
+          fi
+
+  build-archives:
+    name: Build archive (${{ matrix.name }})
+    needs: validate
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - name: Linux x86-64
+            os: ubuntu-latest
+          - name: macOS x86-64
+            os: macos-15-intel
+          - name: macOS ARM64
+            os: macos-15
+          - name: Windows x86-64
+            os: windows-latest
+    runs-on: ${{ matrix.os }}
+
+    steps:
+      - uses: actions/checkout@v4
+
+      - uses: leanprover/lean-action@v1
+        with:
+          build-args: Binary
+          test: false
+          use-github-cache: false
+
+      - name: Pack Lake build archive
+        run: lake pack
+
+      - name: Stage Lake build archive
+        uses: actions/upload-artifact@v4
+        with:
+          name: release-${{ runner.os }}-${{ runner.arch }}
+          path: .lake/binary-*.tar.gz
+          if-no-files-found: error
+          include-hidden-files: true
+
+  publish:
+    name: Publish release
+    needs: build-archives
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+
+      - name: Download Lake build archives
+        uses: actions/download-artifact@v4
+        with:
+          pattern: release-*
+          path: dist
+          merge-multiple: true
+
+      - name: Create tag and GitHub release
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+          RELEASE_TAG: ${{ inputs.tag }}
+        run: |
+          git config user.name "github-actions[bot]"
+          git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
+          git tag -a "${RELEASE_TAG}" "${GITHUB_SHA}" -m "binary ${RELEASE_TAG}"
+          git push origin "${RELEASE_TAG}"
+          gh release create "${RELEASE_TAG}" dist/*.tar.gz \
+            --verify-tag \
+            --generate-notes \
+            --title "${RELEASE_TAG}"
+          for archive in dist/*.tar.gz; do
+            asset="$(basename "${archive}")"
+            url="https://github.com/${GITHUB_REPOSITORY}/releases/download/${RELEASE_TAG}/${asset}"
+            curl --fail --head --location --retry 5 --retry-all-errors "${url}"
+            echo "- ${url}" >> "${GITHUB_STEP_SUMMARY}"
+          done

lakefile.lean

@@ -3,6 +3,8 @@ open Lake DSL
 
 package "binary" where
   version := v!"0.1.0"
+  releaseRepo := "https://github.com/Lean-zh/binary"
+  preferReleaseBuild := true
 
 @[default_target]
 lean_lib Binary where