Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

chore: CI creates lean-pr-testing-NNNN branches at Std too #3200

Merged
merged 9 commits into from
Jan 22, 2024
Merged

chore: CI creates lean-pr-testing-NNNN branches at Std too #3200

Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
bdde13e
chore: CI looks for nightly-testing-YYYY-MM-DD at Mathlib as either a…
kim-em Jan 19, 2024
0fe71e9
add comment
kim-em Jan 19, 2024
cf6d522
chore: create lean-pr-testing-NNNN branches at Std too
kim-em Jan 19, 2024
cb5a0e9
advice from linter
kim-em Jan 19, 2024
f9bd389
more good advice from the linter
kim-em Jan 19, 2024
5694dab
Update .github/workflows/pr-release.yml
kim-em Jan 22, 2024
0cc8496
followup to review suggestion
kim-em Jan 22, 2024
89c7336
merge master
kim-em Jan 22, 2024
a63acb3
more fixes
kim-em Jan 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
84 changes: 75 additions & 9 deletions .github/workflows/pr-release.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,22 +126,32 @@ 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
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

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
Expand Down Expand Up @@ -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 "[email protected]"

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
Expand All @@ -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 "[email protected]"
Expand All @@ -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"
Comment on lines -251 to +321
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm turns out

git switch -c foo base

works if base is a local tag, but not if it is a (remote) branch.

The old code (git checkout base) would work for a (remote) branch, but not for a tag. Kinda annoying.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe we need to parse this output to go onto a common path in both cases

$ git ls-remote --heads --tags --exit-code https://github.com/leanprover-community/mathlib4 nightly-testing-2024-01-22
7d803278d1b5978fccc14f992d9ffb692077ed93	refs/heads/nightly-testing-2024-01-22
$ git ls-remote --heads --tags --exit-code https://github.com/leanprover/std4 nightly-testing-2024-01-22
c15b5a8f04e84bc7aab8b1062a4a80de3046865f	refs/tags/nightly-testing-2024-01-22

Alternatively, we can once manually convert all nightly-testing-YYYY-MM-DD branches to tags on mathlib4. Maybe easier.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Possible fix in #3208

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 }}"
Expand Down