From 5cc9f6f9cbcb2bae03f3860ffd4be30f2b050e72 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 22 Jan 2024 14:06:59 +1100 Subject: [PATCH] chore: CI creates lean-pr-testing-NNNN branches at Std too (#3200) Currently we create `lean-pr-testing-NNNN` branches at Mathlib automatically for each Lean PR. We don't automatically create one at Std; mostly simply because Std fails less often, so it has been okay to do this manually as needed. It is conceptually simpler, however, if this is done uniformly. This PR: * does not proceed with Std/Mathlib CI unless the appropriate `nightly-testing-YYYY-MM-DD` tag exists at Std (like it already doesn't proceed if that tag is missing at Mathlib) * creates `lean-pr-testing-NNNN` branches at Std * when it creates `lean-pr-testing-NNNN` branches at Mathlib, updates the Std dependency to use the `lean-pr-testing-NNNN` branch at Std - [x] depends on #3199 Note that because most users do not have write access at Std, in order to make updates to `lean-pr-testing-NNNN` branches there they will need to make PRs. These will be merged with a very low bar, and feel free to ping me for assistance on this. If this is annoying we will automate. Also, frequent contributors to Lean may ask @digama0 or @joehendrix for write access in order to easily work on these branches. This PR requires that we have a secret here with write access at Std. I'm arranging that [on zulip](https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/bot.20access/near/416686090). I will update the documentation at https://leanprover-community.github.io/contribute/tags_and_branches.html to reflect these changes when they are merged. --------- Co-authored-by: Joachim Breitner --- .github/workflows/pr-release.yml | 84 ++++++++++++++++++++++++++++---- 1 file changed, 75 insertions(+), 9 deletions(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index a000ed52f665..5477d34fdf31 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -126,9 +126,9 @@ jobs: if [ "$NIGHTLY_SHA" = "$MERGE_BASE_SHA" ]; then echo "The merge base of this PR coincides with the nightly release" - REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")" + MATHLIB_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/mathlib4.git nightly-testing-"$MOST_RECENT_NIGHTLY")" - if [[ -n "$REMOTE_TAGS" ]]; then + if [[ -n "$MATHLIB_REMOTE_TAGS" ]]; then echo "... and Mathlib has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag." MESSAGE="" else @@ -136,12 +136,22 @@ jobs: 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 + STD_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover/std4.git nightly-testing-"$MOST_RECENT_NIGHTLY")" + + if [[ -n "$STD_REMOTE_TAGS" ]]; then + echo "... and Std has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag." + MESSAGE="" + else + echo "... but Std does not yet have a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag." + MESSAGE="- ❗ Std 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\`, Std CI should run now." + fi + else echo "The most recently nightly tag on this branch has SHA: $NIGHTLY_SHA" echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA" git -C lean4.git log -10 origin/master - MESSAGE="- ❗ Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch." + MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch." fi if [[ -n "$MESSAGE" ]]; then @@ -213,6 +223,62 @@ jobs: description: description, }); + # We next automatically create a Std branch using this toolchain. + # Std doesn't itself have a mechanism to report results of CI from this branch back to Lean + # Instead this is taken care of by Mathlib CI, which will fail if Std fails. + - name: Cleanup workspace + if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' + run: | + sudo rm -rf ./* + + # Checkout the Std repository with all branches + - name: Checkout Std repository + if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' + uses: actions/checkout@v3 + with: + repository: leanprover/std4 + token: ${{ secrets.MATHLIB4_BOT }} + ref: nightly-testing + fetch-depth: 0 # This ensures we check out all tags and branches. + + - name: Check if tag exists + if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' + id: check_std_tag + run: | + git config user.name "leanprover-community-mathlib4-bot" + git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com" + + 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}' tag at Std. Falling back to 'nightly-testing'." + BASE=nightly-testing + fi + + echo "Using base branch: $BASE" + + EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)" + echo "Branch exists: $EXISTS" + if [ "$EXISTS" = "0" ]; then + echo "Branch does not exist, creating it." + git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE" + echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain + git add lean-toolchain + git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" + else + echo "Branch already exists, pushing an empty commit." + git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} + # The Std `nightly-testing` or `nightly-testing-YYYY-MM-DD` branch 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 + + - name: Push changes + if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' + run: | + git push origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} + # We next automatically create a Mathlib branch using this toolchain. # Mathlib CI will be responsible for reporting back success or failure @@ -234,7 +300,7 @@ jobs: - name: Check if tag exists if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true' - id: check_tag + id: check_mathlib_tag run: | git config user.name "leanprover-community-mathlib4-bot" git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com" @@ -248,20 +314,20 @@ jobs: echo "Using base tag: $BASE" - git checkout "$BASE" - EXISTS="$(git ls-remote --heads origin lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} | wc -l)" echo "Branch exists: $EXISTS" if [ "$EXISTS" = "0" ]; then echo "Branch does not exist, creating it." - git checkout -b lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} + git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE" echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain git add lean-toolchain + sed -i "s/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \".\+\"/require std from git \"https:\/\/github.com\/leanprover\/std4\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean + git add lakefile.lean git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" 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` tag may have moved since this branch was created, so merge their changes. + git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} + # The Mathlib `nightly-testing` branch 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 }}"