mathlib4/.github/workflows/add_label_from_diff.yaml at master · metakunt/mathlib4 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
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@f061402b660e0c34644504b324e830f2991d4865 # v1.6.1
      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: |
        set +e
        "${GITHUB_WORKSPACE}/tools/.lake/build/bin/autolabel" \
          --pr "${PR_NUMBER}" \
          --curl "${GH_TOKEN}"
        code=$?
        if [ "$code" -ne 0 ]; then
          echo "::warning file=scripts/autolabel.lean::autolabel exited with code ${code}. \
          If this PR adds or removes directories, please update \
          \`scripts/autolabel.lean\` in the same PR so \`master\` stays consistent."
        fi
        exit 0
      env:
        GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
        PR_NUMBER: ${{ github.event.pull_request.number }}