From 03d38f50d1864f09cb8334c4030e35a518ad37c5 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Mon, 21 Sep 2026 14:19:30 +0200 Subject: [PATCH 1/4] ci: auto-resolve lakefile.toml when merging main into the bump branch main now pins a Mathlib revision in lakefile.toml, while bump/v4.X.0 branches point at mathlib4-nightly-testing. When main moves its pin, the [[require]] block may conflict and create-adaptation-pr.sh bails out in auto mode, so the bump branch reminder fires every few hours. Resolve conflicting hunks in lakefile.toml in favor of the bump branch with git merge-file --ours, keeping non-conflicting changes from main. --- scripts/create-adaptation-pr.sh | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/scripts/create-adaptation-pr.sh b/scripts/create-adaptation-pr.sh index 47b1ee2a10..aa48c43c71 100755 --- a/scripts/create-adaptation-pr.sh +++ b/scripts/create-adaptation-pr.sh @@ -107,10 +107,22 @@ if git diff --name-only --diff-filter=U | grep -q .; then git checkout bump/"$BUMPVERSION" -- lean-toolchain lake-manifest.json git add lean-toolchain lake-manifest.json + # The Mathlib pins on `main` and the bump branch may conflict. Resolve `lakefile.toml` + # hunk-by-hunk, preferring the bump branch but keeping non-conflicting changes from `main`. + if git diff --name-only --diff-filter=U | grep -qx lakefile.toml; then + echo "### Resolving conflicts in 'lakefile.toml' in favor of 'bump/$BUMPVERSION'" + git show :1:lakefile.toml > lakefile.toml.base + git show :3:lakefile.toml > lakefile.toml.main + git checkout --ours -- lakefile.toml + git merge-file --ours lakefile.toml lakefile.toml.base lakefile.toml.main + rm lakefile.toml.base lakefile.toml.main + git add lakefile.toml + fi + # Check if there are more merge conflicts after auto-resolution if ! git diff --name-only --diff-filter=U | grep -q .; then # Auto-commit the resolved conflicts if no other conflicts remain - git commit -m "Auto-resolved conflicts in lean-toolchain and lake-manifest.json" + git commit -m "Auto-resolved conflicts in lean-toolchain, lake-manifest.json, and lakefile.toml" fi fi From 5b39aa4f1f9865389a55b41933bfd5d020ba06d2 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Mon, 21 Sep 2026 14:19:30 +0200 Subject: [PATCH 2/4] ci: run lake update after merging main into the bump branch Merging main may change lakefile.toml (e.g. add a dependency) while lake-manifest.json is taken whole from the bump branch, leaving the two out of sync. Run lake update after the merge and commit the manifest if it changed. --- scripts/create-adaptation-pr.sh | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/scripts/create-adaptation-pr.sh b/scripts/create-adaptation-pr.sh index aa48c43c71..1feba572d2 100755 --- a/scripts/create-adaptation-pr.sh +++ b/scripts/create-adaptation-pr.sh @@ -126,6 +126,16 @@ if git diff --name-only --diff-filter=U | grep -q .; then fi fi +if ! git diff --name-only --diff-filter=U | grep -q .; then + echo + echo "### [auto] run 'lake update' so that 'lake-manifest.json' matches the merged 'lakefile.toml'" + lake update + if ! git diff --quiet -- lake-manifest.json; then + git add lake-manifest.json + git commit -m "Update lake-manifest.json after merging main" + fi +fi + if git diff --name-only --diff-filter=U | grep -q . || ! git diff-index --quiet HEAD --; then if [ "$AUTO" = "yes" ]; then echo "Auto mode enabled. Bailing out due to unresolved conflicts or uncommitted changes." From 1879c52755531aec452ff32fed00840f46c30384 Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Mon, 21 Sep 2026 14:19:30 +0200 Subject: [PATCH 3/4] ci: install Lean in the reminder workflow before creating adaptation PRs create-adaptation-pr.sh now runs lake update after merging main into the bump branch, so the job that runs it needs a Lean toolchain. Use lean-action@v1 like the other non-nightly workflows. --- .github/workflows/report_failures_nightly-testing.yml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/.github/workflows/report_failures_nightly-testing.yml b/.github/workflows/report_failures_nightly-testing.yml index 3970b5312c..7f2984bf3e 100644 --- a/.github/workflows/report_failures_nightly-testing.yml +++ b/.github/workflows/report_failures_nightly-testing.yml @@ -297,6 +297,15 @@ jobs: fetch-depth: 0 # checkout all branches token: ${{ steps.app-token.outputs.token }} + # create-adaptation-pr.sh runs `lake update` after merging main into the bump branch. + - name: Configure Lean + if: steps.check_branch.outputs.result == 'false' + uses: leanprover/lean-action@v1 + with: + auto-config: false + use-github-cache: false + use-mathlib-cache: false + - name: Attempt automatic PR creation id: auto_pr if: steps.check_branch.outputs.result == 'false' From 33d7a9abbf707409568b085eda097c42ff7dab7b Mon Sep 17 00:00:00 2001 From: Jesse Alama Date: Mon, 21 Sep 2026 14:44:35 +0200 Subject: [PATCH 4/4] ci: drop the lake update step after merging main into the bump branch The resolved lakefile.toml always matches the bump branch's lake-manifest.json, since the only [[require]] block is the Mathlib pin that both branches edit and the bump branch wins. Running lake update was a no-op that required installing Lean in the reminder workflow. --- .github/workflows/report_failures_nightly-testing.yml | 9 --------- scripts/create-adaptation-pr.sh | 10 ---------- 2 files changed, 19 deletions(-) diff --git a/.github/workflows/report_failures_nightly-testing.yml b/.github/workflows/report_failures_nightly-testing.yml index 7f2984bf3e..3970b5312c 100644 --- a/.github/workflows/report_failures_nightly-testing.yml +++ b/.github/workflows/report_failures_nightly-testing.yml @@ -297,15 +297,6 @@ jobs: fetch-depth: 0 # checkout all branches token: ${{ steps.app-token.outputs.token }} - # create-adaptation-pr.sh runs `lake update` after merging main into the bump branch. - - name: Configure Lean - if: steps.check_branch.outputs.result == 'false' - uses: leanprover/lean-action@v1 - with: - auto-config: false - use-github-cache: false - use-mathlib-cache: false - - name: Attempt automatic PR creation id: auto_pr if: steps.check_branch.outputs.result == 'false' diff --git a/scripts/create-adaptation-pr.sh b/scripts/create-adaptation-pr.sh index 1feba572d2..aa48c43c71 100755 --- a/scripts/create-adaptation-pr.sh +++ b/scripts/create-adaptation-pr.sh @@ -126,16 +126,6 @@ if git diff --name-only --diff-filter=U | grep -q .; then fi fi -if ! git diff --name-only --diff-filter=U | grep -q .; then - echo - echo "### [auto] run 'lake update' so that 'lake-manifest.json' matches the merged 'lakefile.toml'" - lake update - if ! git diff --quiet -- lake-manifest.json; then - git add lake-manifest.json - git commit -m "Update lake-manifest.json after merging main" - fi -fi - if git diff --name-only --diff-filter=U | grep -q . || ! git diff-index --quiet HEAD --; then if [ "$AUTO" = "yes" ]; then echo "Auto mode enabled. Bailing out due to unresolved conflicts or uncommitted changes."