chore: ignore scripts on package bump (#726) #3050
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: vscode-lean4 build | |
| on: | |
| pull_request: | |
| branches: | |
| - '*' | |
| push: | |
| branches: | |
| - '*' | |
| tags: | |
| - '*' | |
| permissions: | |
| contents: write | |
| id-token: write | |
| jobs: | |
| build-and-test: | |
| 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=format:"%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 |