Release #2
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 | |
| shell: bash | |
| run: | | |
| "$HOME/.elan/bin/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 |