Finding the PR number during github CI

Stream: lean4

[Scott Morrison]

I'm trying to modify Lean 4 CI, with the intention of making it easier to create releases, and for a bot to give feedback on PRs about whether the changes will break Std / Mathlib.

However I'm failing at a very simple step, and rather than beat my head against it, hopefully someone who knows Github workflow files better can help.

I just want to know the PR number --- and I need to know this for every push to the PR, not just the event that creates the PR.

In Mathlib we do this, and we use the 8BitJonny/gh-get-current-pr@2.2.0 action. However when I try to use this in Lean 4 CI, I don't get any information back.

Here is the diff (most of the changes are just commenting out parts of CI so I can run experiments faster). Here's a sample run where you can see that both of my attempts to determine the PR number are just returning empty strings.

Any advice?

[Mac Malone]

@Scott Morrison If you look at the raw logs, there is this error at the bottom:

could not determine current branch: failed to run git: not on any branch

[Mac Malone]

Comparing the raw logs of your lean PR with the raw logs of my previous mathlib PR, the key difference appears to the be absence or presence of -B in the checkout line:

/usr/bin/git checkout --progress --force -B master refs/remotes/origin/master (my PR)
/usr/bin/git checkout --progress --force refs/remotes/pull/1/merge (your PR)

Your PR is checked out in a detached HEAD state with no branch whereas the mathlib PR is checked out as a branch. Given the above error, it is likely the get PR actions need a branch to properly infer the PR, thus the 'detached HEAD' state makes this impossible.

[Denis Gorbachev]

Just an idea - export the context vars as env vars

      - name: Report pull request number
        env:
          PR_NUMBER_ATTEMPT_1: ${{ steps.pr-number-attempt-1.outputs.number }}
          PR_NUMBER_ATTEMPT_2: ${{ steps.pr-number-attempt-2.outputs.number }}
        run: |
          echo "gh client reported: $PR_NUMBER_ATTEMPT_1"
          echo "gh-get-current-pr reported: $PR_NUMBER_ATTEMPT_2"

[Mac Malone]

@Scott Morrison My suspicious for difference in checkout behavior is that it has to do with one of these being a branch within a repo vs a branch outside of a repo. See this the old actions/checkout#6 issue for some discussion and possible workarounds.

[Mac Malone]

There is also a number of new issues and PRs with similar problems (actions/checkout#1325, actions/checkout#1108, actions/checkout#138).

[Scott Morrison]

In fact, I'm confused why Lean 4 CI even runs on pushes to branches. The top of .github/workflows/build.yml in Mathlib reads:

on:
  push:
    branches-ignore:
      # ignore tmp branches used by bors
      - 'staging.tmp*'
      - 'trying.tmp*'
      - 'staging*.tmp'
      - 'nolints'
      # ignore staging branch used by bors, this is handled by bors.yml
      - 'staging'

and I see that as running on pushes to most branches.

However the .github/workflows/ci.yml has

name: CI
on:
  push:
    branches:
      - 'master'
    tags:
      - '*'
  pull_request:
    branches:
      - master
  schedule:
    - cron: '0 7 * * *'  # 8AM CET/11PM PT

which seems like it should be triggered only by pushes to master or pushes that create/modify a tag, or to new PRs to master.

What in there is triggering when I push something to an existing PR branch?

[Scott Morrison]

Mac Malone said:

Scott Morrison My suspicious for difference in checkout behavior is that it has to do with one of these being a branch within a repo vs a branch outside of a repo. See this the old actions/checkout#6 issue for some discussion and possible workarounds.

I don't understand here. In the example run I linked to above, we're looking at a push to a branch on my fork, which is part of a PR to master also on my fork. There's no cross-repo stuff going on anyway?

[Sebastian Ullrich]

The pull_request ... master event is triggered for any push to a PR targeting master

[Sebastian Ullrich]

According to https://docs.github.com/en/webhooks-and-events/webhooks/webhook-events-and-payloads?actionType=synchronize#pull_request, github.event.number should hold the PR number when triggered by pull_request? Not sure I'm missing any intermediary objects.

[Scott Morrison]

github.event.number indeed has the information I'm after!