From 2a6d24ee27839b142133eb695fda851b2a0185cc Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 17 Mar 2024 10:35:42 +1100 Subject: [PATCH 1/4] chore: fix rebase suggestion for Mathlib CI --- .github/workflows/pr-release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 5c1f8fd6828d..0f7847f2d21e 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -151,7 +151,7 @@ jobs: echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA" git -C lean4.git log -10 origin/master - MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_SHA\`." + MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto nightly-with-mathlib\`." fi if [[ -n "$MESSAGE" ]]; then From 385108f9656fd79e984886d9e099c35085b2a2d4 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 17 Mar 2024 10:36:53 +1100 Subject: [PATCH 2/4] origin --- .github/workflows/pr-release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 0f7847f2d21e..f187d32bd008 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -151,7 +151,7 @@ jobs: echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA" git -C lean4.git log -10 origin/master - MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto nightly-with-mathlib\`." + MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto origin/nightly-with-mathlib\`." fi if [[ -n "$MESSAGE" ]]; then From da57f22c7eaad638c7412aed3238b1b2780af4ad Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 17 Mar 2024 12:26:45 +1100 Subject: [PATCH 3/4] use SHA, but the one for nightly-with-mathlib --- .github/workflows/pr-release.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index f187d32bd008..694ef4ef41ff 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -151,7 +151,8 @@ jobs: echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA" git -C lean4.git log -10 origin/master - MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto origin/nightly-with-mathlib\`." + NIGHTLY_WITH_MATHLIB_SHA=$(git -C lean4.git rev-parse "nightly-with-mathlib") + MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`." fi if [[ -n "$MESSAGE" ]]; then From d23ee90b281332b2e8d46ff462480e89bb4c22c0 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 22 Mar 2024 10:48:41 +1100 Subject: [PATCH 4/4] Update .github/workflows/pr-release.yml Co-authored-by: Joachim Breitner --- .github/workflows/pr-release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 694ef4ef41ff..4edacd974c3a 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -151,7 +151,7 @@ jobs: echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA" git -C lean4.git log -10 origin/master - NIGHTLY_WITH_MATHLIB_SHA=$(git -C lean4.git rev-parse "nightly-with-mathlib") + NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "nightly-with-mathlib")" MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`." fi