[Merged by Bors] - chore: delete deprecated modules from February 2026 #29239
Workflow file for this run
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: Autolabel PRs | |
| on: | |
| pull_request_target: | |
| types: [opened] | |
| # Limit permissions for GITHUB_TOKEN for the entire workflow | |
| permissions: | |
| contents: read | |
| pull-requests: write # Only allow PR comments/labels | |
| # All other permissions are implicitly 'none' | |
| jobs: | |
| add_topic_label: | |
| name: Add topic label | |
| runs-on: ubuntu-latest | |
| # Don't run on forks, where we wouldn't have permissions to add the label anyway. | |
| if: github.repository == 'leanprover-community/mathlib4' | |
| steps: | |
| - name: Checkout master branch to build autolabel from | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| ref: master | |
| path: tools | |
| - name: Configure Lean | |
| uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0 | |
| with: | |
| auto-config: false | |
| use-github-cache: false | |
| use-mathlib-cache: false | |
| lake-package-directory: tools # Building here | |
| - name: Build autolabel from master | |
| working-directory: tools | |
| run: | | |
| lake build autolabel | |
| - name: Checkout branch to label | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| ref: ${{ github.event.pull_request.head.sha || github.sha }} | |
| fetch-depth: 0 | |
| path: pr-branch | |
| # Untrusted (potentially fork) checkout: don't persist the GITHUB_TOKEN into its .git/config. | |
| persist-credentials: false | |
| # autolabel is built from the trusted base checkout and only reads these files, | |
| # so checking out fork PR code under pull_request_target is safe. | |
| allow-unsafe-pr-checkout: true | |
| - name: Run autolabel | |
| working-directory: pr-branch | |
| run: | | |
| "${GITHUB_WORKSPACE}/tools/.lake/build/bin/autolabel" --pr "${{ github.event.pull_request.number }}" --curl "${{ secrets.GITHUB_TOKEN }}" | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| PR_NUMBER: ${{ github.event.pull_request.number }} |