feat: client-side support for incremental diagnostics (#752) #3187
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: | |
| 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: | |
| package: | |
| if: github.event_name != 'workflow_dispatch' | |
| runs-on: ubuntu-latest | |
| 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') }} | |
| 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') }} | |
| 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') }} | |
| 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') }} | |
| 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 | |
| with: | |
| name: vscode-lean4 | |
| path: 'vscode-lean4/lean4-*.vsix' | |
| build-and-test: | |
| if: github.event_name != 'workflow_dispatch' | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - name: build-and-test-linux | |
| os: ubuntu-latest | |
| artifact: build-Linux release | |
| # - name: build-and-test-macos | |
| # os: macos-latest | |
| # artifact: build-macOS | |
| - name: build-and-test-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: 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-vsce: | |
| needs: package | |
| if: startsWith(github.ref, 'refs/tags/v') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Setup Node.js | |
| uses: actions/setup-node@v4 | |
| with: | |
| node-version: '24' | |
| - name: Download packaged extension | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: vscode-lean4 | |
| path: vscode-lean4 | |
| - name: Publish to VS Code Marketplace | |
| run: | | |
| cd vscode-lean4 | |
| npx @vscode/vsce publish $PRE_RELEASE_FLAG -i lean4-*.vsix | |
| env: | |
| VSCE_PAT: ${{ secrets.VSCE_PAT }} | |
| PRE_RELEASE_FLAG: ${{ endsWith(github.ref, '-pre') && '--pre-release' || '' }} | |
| publish-ovsx: | |
| needs: package | |
| if: startsWith(github.ref, 'refs/tags/v') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Setup Node.js | |
| uses: actions/setup-node@v4 | |
| with: | |
| node-version: '24' | |
| - name: Download packaged extension | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: vscode-lean4 | |
| path: vscode-lean4 | |
| - name: Publish to Open VSX | |
| run: | | |
| cd vscode-lean4 | |
| npx ovsx publish $PRE_RELEASE_FLAG lean4-*.vsix | |
| env: | |
| OVSX_PAT: ${{ secrets.OVSX_PAT }} | |
| PRE_RELEASE_FLAG: ${{ endsWith(github.ref, '-pre') && '--pre-release' || '' }} | |
| github-release: | |
| needs: [package, publish-vsce, publish-ovsx] | |
| # Run even if one of the publish jobs failed, so a GitHub Release with notes | |
| # is always created on a tag build. Tests are intentionally not a dependency: | |
| # releases ship in parallel with the build-and-test matrix, matching the | |
| # previous single-job behavior where publish ran before tests. | |
| if: | | |
| !cancelled() && | |
| needs.package.result == 'success' && | |
| startsWith(github.ref, 'refs/tags/v') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@v2 | |
| with: | |
| fetch-depth: 0 | |
| - name: Download packaged extension | |
| uses: actions/download-artifact@v4 | |
| with: | |
| name: vscode-lean4 | |
| path: vscode-lean4 | |
| - name: Generate release notes | |
| 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)" | |
| { | |
| # If either marketplace publish failed, prepend a prominent warning so | |
| # the partial failure is obvious on the Release page itself (in addition | |
| # to the red CI status). Note: this banner is NOT updated automatically | |
| # after a successful "Re-run failed jobs" — edit the release body by | |
| # hand after a retry if you want the banner gone. | |
| vsce_result="${{ needs.publish-vsce.result }}" | |
| ovsx_result="${{ needs.publish-ovsx.result }}" | |
| failed=() | |
| if [ "$vsce_result" != "success" ]; then failed+=("VS Code Marketplace"); fi | |
| if [ "$ovsx_result" != "success" ]; then failed+=("Open VSX"); fi | |
| if [ ${#failed[@]} -gt 0 ]; then | |
| if [ ${#failed[@]} -eq 2 ]; then | |
| joined="${failed[0]} and ${failed[1]}" | |
| else | |
| joined="${failed[0]}" | |
| fi | |
| echo "> [!WARNING]" | |
| echo "> This release could not be published to **$joined** from CI." | |
| echo "> See [the CI run](${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}) and use *Re-run failed jobs* once the upstream issue is resolved." | |
| echo "" | |
| fi | |
| 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 | |
| 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 }} | |
| 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` and `pre-release` can be dispatched from `master` for regular | |
| # releases, or from a `patch-release/v<release>` branch to cut a patch on top | |
| # of a previous release after master has already advanced. The version bump | |
| # is the global max of all `v*` tags + 1, so patch releases automatically | |
| # take the next patch number and subsequent master releases skip past it. | |
| 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 |