Skip to content

Commit

Permalink
fix: rewrite update_dependencies_zulip action (#14630)
Browse files Browse the repository at this point in the history
  • Loading branch information
Ruben-VandeVelde committed Jul 10, 2024
1 parent 3162e25 commit fdc4c84
Showing 1 changed file with 32 additions and 27 deletions.
59 changes: 32 additions & 27 deletions .github/workflows/update_dependencies_zulip.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,39 +7,44 @@ on:
workflows: ["continuous integration"]
types:
- completed
branches:
- 'update-dependencies-**'

jobs:
monitor-failures:
runs-on: ubuntu-latest
if: ${{ github.event.workflow_run.conclusion == 'failure' && startsWith(github.event.workflow_run.head_branch, 'update-dependencies-') }}
if: ${{ github.event.workflow_run.conclusion == 'failure' }}

steps:
- name: Checkout repository
uses: actions/checkout@v4
- name: Construct message
uses: actions/github-script@v7
id: construct_message
with:
fetch-depth: 0
token: ${{ secrets.NIGHTLY_TESTING }}

- name: Set GH_TOKEN
run: echo "GH_TOKEN=${{ secrets.NIGHTLY_TESTING }}" >> "$GITHUB_ENV"

- name: Get PR number
id: get_pr
run: |
pr_number=$(gh pr list --state open --head "leanprover-community/mathlib4:${{ github.event.workflow_run.head_branch }}" --json number -q '.[0].number')
echo "pr_number=$pr_number" >> "$GITHUB_ENV"
- name: Update PR labels
if: env.pr_number
run: |
gh pr edit "${{ env.pr_number }}" --remove-label "auto-merge-after-CI" --add-label "awaiting-CI,awaiting-review"
- name: Get CI URL
id: ci_url
run: |
url="https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}"
curl -s "$url" |
awk -v url="$url" -F'/' '/^ *href/ {gsub(/"/, "", $NF); printf("summary<<EOF\n%s/job/%s\nEOF", url, $NF)}' >> "$GITHUB_OUTPUT"
github-token: ${{ secrets.NIGHTLY_TESTING }}
result-encoding: string
script: |
const owner = context.repo.owner, repo = context.repo.repo;
let output = "❌ `lake update` [failed](" + context.payload.workflow_run.html_url + "). "
let prs = context.payload.workflow_run.pull_requests
if (prs.length) {
for (let pr of prs) {
const { data: pullRequest } = await github.rest.pulls.get({
owner,
repo,
pull_number: pr.number,
});
output += "Found [PR " + pr.number + "](" + pullRequest.html_url + "). "
await github.rest.issues.removeLabel({
owner,
repo,
issue_number: pr.number,
name: "auto-merge-after-CI",
});
}
} else {
output += "No PR found for this run!";
}
return output;
- name: Send Zulip message
uses: zulip/github-actions-zulip/send-message@v1
Expand All @@ -51,4 +56,4 @@ jobs:
type: 'stream'
topic: 'Mathlib `lake update` failure'
content: |
❌ `lake update` [failed](${{ steps.ci_url.outputs.summary }}) on ${{ github.sha }}
${{ steps.construct_message.outputs.result }}

0 comments on commit fdc4c84

Please sign in to comment.