Skip to content

refactor: clean up semver handling #3162

refactor: clean up semver handling

refactor: clean up semver handling #3162

Workflow file for this run

name: vscode-lean4 build
on:
workflow_dispatch:
inputs:
action:
description: 'Action to perform'
required: true
type: choice
options:
- publish-packages
- release
- pre-release
pull_request:
branches:
- '*'
push:
branches:
- '*'
tags:
- '*'
permissions:
contents: write
id-token: write
jobs:
build-and-test:
if: github.event_name != 'workflow_dispatch'
strategy:
fail-fast: false
matrix:
include:
- name: Linux
os: ubuntu-latest
artifact: build-Linux release
# - name: macOS
# os: macos-latest
# artifact: build-macOS
- name: Windows
os: windows-latest
artifact: build-Windows
name: ${{ matrix.name }}
runs-on: ${{ matrix.os }}
steps:
- name: Checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
- name: Setup Node.js
uses: actions/setup-node@v4
with:
node-version: '24'
registry-url: 'https://registry.npmjs.org'
- name: Build
run: |
npm ci
npm run build
- name: Try publishing infoview-api
if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
continue-on-error: true
run: |
npm publish --workspace=lean4-infoview-api --access=public
- name: Try publishing infoview
if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
continue-on-error: true
run: |
npm publish --workspace=lean4-infoview --access=public
- name: Try publishing unicode-input
if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
continue-on-error: true
run: |
npm publish --workspace=lean4-unicode-input --access=public
- name: Try publishing unicode-input-component
if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
continue-on-error: true
run: |
npm publish --workspace=lean4-unicode-input-component --access=public
- name: Package
run: npm run package --workspace=lean4
if: ${{ !startsWith(github.ref, 'refs/tags/v') || !endsWith(github.ref, '-pre') }}
- name: Package pre-release
run: npm run packagePreRelease --workspace=lean4
if: ${{ startsWith(github.ref, 'refs/tags/v') && endsWith(github.ref, '-pre') }}
- name: Upload artifact
uses: actions/upload-artifact@v4
if: matrix.os == 'ubuntu-latest'
with:
name: vscode-lean4
path: 'vscode-lean4/lean4-*.vsix'
- name: Publish packaged extension
if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
run: |
cd vscode-lean4
npx @vscode/vsce publish -i lean4-*.vsix
npx ovsx publish lean4-*.vsix
env:
OVSX_PAT: ${{ secrets.OVSX_PAT }}
VSCE_PAT: ${{ secrets.VSCE_PAT }}
- name: Publish packaged pre-release extension
if: ${{ startsWith(github.ref, 'refs/tags/v') && endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
run: |
cd vscode-lean4
npx @vscode/vsce publish --pre-release -i lean4-*.vsix
npx ovsx publish --pre-release lean4-*.vsix
env:
OVSX_PAT: ${{ secrets.OVSX_PAT }}
VSCE_PAT: ${{ secrets.VSCE_PAT }}
- name: Generate release notes
if: startsWith(github.ref, 'refs/tags/v') && matrix.os == 'ubuntu-latest'
run: |
current_tag="${GITHUB_REF#refs/tags/}"
is_pre="${{ endsWith(github.ref, '-pre') }}"
if [ "$is_pre" = "true" ]; then
# Pre-release: commits since last tag of any kind
prev_tag="$(git tag --sort=-v:refname --list 'v*' --no-contains | head -1)"
else
# Full release: commits since last full release (skip pre-release tags)
prev_tag="$(git tag --sort=-v:refname --list 'v*' --no-contains | grep -v -- '-pre$' | head -1)"
fi
echo "Previous tag: $prev_tag"
echo "Current tag: $current_tag"
# Fetch collaborators with write access (once, to avoid per-commit API calls)
write_users="$(gh api "/repos/${{ github.repository }}/collaborators" --paginate --jq '.[] | select(.permissions.push) | .login' 2>/dev/null || true)"
{
git log "$prev_tag".."$current_tag"^ --pretty=tformat:"%H %s" | while read -r hash msg; do
# Skip release commits
case "$msg" in
"Release "* | "chore: bump @leanprover/"*) continue ;;
esac
# Look up the GitHub author
gh_user="$(gh api "/repos/${{ github.repository }}/commits/$hash" --jq '.author.login // empty' 2>/dev/null || true)"
if [ -n "$gh_user" ] && ! echo "$write_users" | grep -qx "$gh_user"; then
# Append "author: user" inside existing trailing parentheses, or add new ones
if echo "$msg" | grep -q ')\s*$'; then
msg="$(echo "$msg" | sed 's/)\s*$/, author: '"$gh_user"')/')"
else
msg="$msg (author: $gh_user)"
fi
fi
echo "- $msg"
done
} > release_notes.md
echo "Release notes:"
cat release_notes.md
env:
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- name: Upload extension as release
if: startsWith(github.ref, 'refs/tags/v') && matrix.os == 'ubuntu-latest'
uses: softprops/action-gh-release@v1
with:
files: 'vscode-lean4/lean4-*.vsix'
fail_on_unmatched_files: true
prerelease: ${{ endsWith(github.ref, '-pre') }}
body_path: release_notes.md
env:
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
- name: Lint
run: npm run lint
- name: Install Brew Packages
run: |
brew install ccache tree zstd coreutils
if: matrix.os == 'macos-latest'
- name: Set path to elan on Linux or macOS
if: matrix.os == 'ubuntu-latest' || matrix.os == 'macos-latest'
run: |
echo "$HOME/.elan/bin" >> $GITHUB_PATH
- name: Set path to elan on Windows
shell: pwsh
if: matrix.os == 'windows-latest'
run: |
echo "$HOME\.elan\bin" >> $env:GITHUB_PATH
- name: Run tests
uses: GabrielBB/xvfb-action@v1.0
with:
run: npm run test
publish-packages:
if: github.event_name == 'workflow_dispatch' && inputs.action == 'publish-packages'
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v2
- name: Setup Node.js
uses: actions/setup-node@v4
with:
node-version: '24'
registry-url: 'https://registry.npmjs.org'
- name: Build
run: |
npm ci
npm run build
- name: Try publishing infoview-api
continue-on-error: true
run: npm publish --workspace=lean4-infoview-api --access=public
- name: Try publishing infoview
continue-on-error: true
run: npm publish --workspace=lean4-infoview --access=public
- name: Try publishing unicode-input
continue-on-error: true
run: npm publish --workspace=lean4-unicode-input --access=public
- name: Try publishing unicode-input-component
continue-on-error: true
run: npm publish --workspace=lean4-unicode-input-component --access=public
release:
if: github.event_name == 'workflow_dispatch' && inputs.action == 'release'
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
token: ${{ secrets.RELEASE_TOKEN }}
- name: Compute next version
id: version
run: |
last_tag="$(git tag --sort=-v:refname --list 'v*' --no-contains | head -1)"
echo "Last tag: $last_tag"
last_version="${last_tag#v}"
last_version="${last_version%-pre}"
new_version="$(echo "$last_version" | awk -F. '{$NF=$NF+1; print}' OFS=.)"
echo "New version: $new_version"
echo "new_version=$new_version" >> "$GITHUB_OUTPUT"
- name: Update version and create tag
run: |
new_version="${{ steps.version.outputs.new_version }}"
sed -i 's/"version": ".*"/"version": "'$new_version'"/' vscode-lean4/package.json
git config user.name "github-actions[bot]"
git config user.email "github-actions[bot]@users.noreply.github.com"
git commit -am "Release $new_version"
git tag -a "v$new_version" -m "vscode-lean4 $new_version"
- name: Push
run: |
git push
git push --tags
pre-release:
if: github.event_name == 'workflow_dispatch' && inputs.action == 'pre-release'
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v2
with:
fetch-depth: 0
token: ${{ secrets.RELEASE_TOKEN }}
- name: Compute next version
id: version
run: |
last_tag="$(git tag --sort=-v:refname --list 'v*' --no-contains | head -1)"
echo "Last tag: $last_tag"
last_version="${last_tag#v}"
last_version="${last_version%-pre}"
new_version="$(echo "$last_version" | awk -F. '{$NF=$NF+1; print}' OFS=.)"
echo "New version: $new_version"
echo "new_version=$new_version" >> "$GITHUB_OUTPUT"
- name: Update version and create tag
run: |
new_version="${{ steps.version.outputs.new_version }}"
sed -i 's/"version": ".*"/"version": "'$new_version'"/' vscode-lean4/package.json
git config user.name "github-actions[bot]"
git config user.email "github-actions[bot]@users.noreply.github.com"
git commit -am "Release $new_version (pre-release)"
git tag -a "v$new_version-pre" -m "vscode-lean4 $new_version (pre-release)"
- name: Push
run: |
git push
git push --tags