Skip to content

[Merged by Bors] - chore: rename IrreducibleCloseds fields to match naming convention #15930

[Merged by Bors] - chore: rename IrreducibleCloseds fields to match naming convention

[Merged by Bors] - chore: rename IrreducibleCloseds fields to match naming convention #15930

name: Autolabel PRs
on:
pull_request_target:
types: [opened]
push:
paths:
- scripts/autolabel.lean
- .github/workflows/add_label_from_diff.yaml
# 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 code
uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
with:
ref: ${{ github.event.pull_request.head.sha }}
fetch-depth: 0
- name: Configure Lean
uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
with:
auto-config: false
use-github-cache: false
use-mathlib-cache: false
- name: lake exe autolabel
run: |
# the checkout dance, to avoid a detached head
git checkout master
git checkout -
labels="$(lake exe autolabel)"
printf '%s\n' "${labels}"
# extract
label="$(printf '%s' "${labels}" | sed -n 's=.*#\[\([^,]*\)\].*=\1=p')"
printf 'label: "%s"\n' "${label}"
if [ -n "${label}" ]
then
printf 'Applying label %s\n' "${label}"
# we use curl rather than octokit/request-action so that the job won't fail
# (and send an annoying email) if the labels don't exist
url="https://api.github.com/repos/${{ github.repository }}/issues/${{ github.event.pull_request.number }}/labels"
printf 'url: %s\n' "${url}"
jsonLabel="$(printf '{"labels":["%s"]}' "${label}")"
printf 'jsonLabel: %s\n' "${jsonLabel}"
curl --request POST \
--header 'Accept: application/vnd.github+json' \
--header 'authorization: Bearer ${{ secrets.GITHUB_TOKEN }}' \
--header 'X-GitHub-Api-Version: 2022-11-28' \
--url "${url}" \
--data "${jsonLabel}"
else
echo "There is no single label that we could apply, so we are not applying any label."
fi
env:
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}