max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: CI looks for nightly-testing-YYYY-MM-DD at Mathlib as either a branch or tag (#3199)

Browse source 
As discussed during the FRO meeting 2024-01-18, we are changing the
`nightly-testing-YYYY-MM-DD` branches at Std and Mathlib from branches
to tags, in:

* https://github.com/leanprover/std4/pull/545
* https://github.com/leanprover-community/mathlib4/pull/9842

This PR updates the script that creates the `lean-pr-testing-NNNN`
branches at Mathlib so it is agnostic about whether
`nightly-testing-YYYY-MM-DD` will be a branch or a tag.

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This commit is contained in:
Scott Morrison 2024-01-21 10:50:03 +11:00 • committed by GitHub
parent c0f264ffe0
commit 73b87f2558
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 12 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
.github/workflows/pr-release.yml vendored
View file

@ -41,7 +41,7 @@ jobs:
name: build-.*
name_is_regexp: true
- name: Push branch and tag
- name: Push tag
if: ${{ steps.workflow-info.outputs.pullRequestNumber != '' }}
run: |
git init --bare lean4.git
@ -126,14 +126,14 @@ jobs:
if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then
echo "The merge base of this PR coincides with the nightly release"
REMOTE_BRANCHES="$(git ls-remote -h https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
if [[ -n "$REMOTE_BRANCHES" ]]; then
echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' branch."
if [[ -n "$REMOTE_TAGS" ]]; then
echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE=""
else
echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' branch."
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` branch does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
echo "... but Mathlib does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
MESSAGE="- ❗ Mathlib CI can not be attempted yet, as the \`nightly-testing-$MOST_RECENT_NIGHTLY\` tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto \`nightly-with-mathlib\`, Mathlib CI should run now."
fi
else
@ -232,21 +232,21 @@ jobs:
ref: nightly-testing
fetch-depth: 0 # This ensures we check out all tags and branches.
- name: Check if branch exists
- name: Check if tag exists
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
id: check_branch
id: check_tag
run: |
git config user.name "leanprover-community-mathlib4-bot"
git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
if git branch -r | grep -q "nightly-testing-${MOST_RECENT_NIGHTLY}"; then
if git ls-remote --heads --tags --exit-code origin "nightly-testing-${MOST_RECENT_NIGHTLY}" >/dev/null; then
BASE="nightly-testing-${MOST_RECENT_NIGHTLY}"
else
echo "This shouldn't be possible: couldn't find a 'nightly-testing-${MOST_RECENT_NIGHTLY}' branch at Mathlib. Falling back to 'nightly-testing'."
BASE=nightly-testing
fi
echo "Using base branch: $BASE"
echo "Using base tag: $BASE"
git checkout "$BASE"
@ -261,7 +261,8 @@ jobs:
else
echo "Branch already exists, pushing an empty commit."
git checkout lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
# The Mathlib `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch may have moved since this branch was created, so merge their changes.
# The Mathlib `nightly-testing` or `nightly-testing-YYYY-MM-DD` tag may have moved since this branch was created, so merge their changes.
# (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
fi