From ad8d6ed5330f48e906ac981a558b6f42fa7ec0c7 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 00:50:16 +0000 Subject: [PATCH 1/3] fix: merge lakefile.toml into nightly-testing structurally The CD pipeline merged lakefile.toml textually with -X ours, which drops main's changes whenever they touch lines next to nightly-testing's dependency revisions. Now take main's lakefile.toml and only carry over nightly-testing's dependency revisions. When the lakefile changes, refresh the manifest with `lake update` on the nightly toolchain. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/cd-pipeline.yml | 58 +++++++++++++++++++++++++++++-- 1 file changed, 56 insertions(+), 2 deletions(-) diff --git a/.github/workflows/cd-pipeline.yml b/.github/workflows/cd-pipeline.yml index fbd99973..b9d79581 100644 --- a/.github/workflows/cd-pipeline.yml +++ b/.github/workflows/cd-pipeline.yml @@ -25,10 +25,64 @@ jobs: token: ${{ secrets.PARSEIT_TOKEN }} - name: Merge main into nightly-testing + id: merge run: | git config user.name "${{ github.actor }}" git config user.email "${{ github.actor_id }}+${{ github.actor }}@users.noreply.github.com" - git merge origin/main --no-commit --strategy-option ours --allow-unrelated-histories - git restore --staged lean-toolchain lake-manifest.json + git merge origin/main --no-commit --no-ff --strategy-option ours --allow-unrelated-histories + # nightly-testing keeps its own toolchain and manifest + git checkout HEAD -- lean-toolchain lake-manifest.json + # take main's lakefile but keep nightly-testing's dependency revisions + git show HEAD:lakefile.toml > "$RUNNER_TEMP/nightly-lakefile.toml" + git show origin/main:lakefile.toml > lakefile.toml + python3 - "$RUNNER_TEMP/nightly-lakefile.toml" lakefile.toml <<'PY' + import re, sys, tomllib + with open(sys.argv[1], "rb") as f: + revs = {r["name"]: r["rev"] for r in tomllib.load(f).get("require", []) if "rev" in r} + with open(sys.argv[2]) as f: + lines = f.read().splitlines(keepends=True) + heads = [i for i, l in enumerate(lines) if re.match(r"\s*\[", l)] + [len(lines)] + out = lines[:heads[0]] + for a, b in zip(heads, heads[1:]): + block = lines[a:b] + if block[0].strip() == "[[require]]": + name = tomllib.loads("".join(block[1:])).get("name") + if name in revs: + rev = 'rev = "%s"\n' % revs[name] + for i, l in enumerate(block): + if re.match(r"\s*rev\s*=", l): + block[i] = rev + break + else: + n = len(block) + while n > 1 and not block[n - 1].strip(): + n -= 1 + block.insert(n, rev) + out += block + with open(sys.argv[2], "w") as f: + f.write("".join(out)) + PY + git add lakefile.toml + if git diff --cached --quiet HEAD -- lakefile.toml; then + echo "lakefile_changed=false" >> "$GITHUB_OUTPUT" + else + echo "lakefile_changed=true" >> "$GITHUB_OUTPUT" + fi + + - name: Install Lean + if: steps.merge.outputs.lakefile_changed == 'true' + uses: leanprover/lean-action@f061402b660e0c34644504b324e830f2991d4865 # v1.6.1 + with: + auto-config: false + use-github-cache: false + + - name: Update manifest + if: steps.merge.outputs.lakefile_changed == 'true' + run: | + lake update --keep-toolchain + git add lake-manifest.json + + - name: Commit and push + run: | git commit --allow-empty -m "chore: merge main into nightly-testing" git push origin nightly-testing From 4f0ede5321b31555dd8c6f3c82080766d149cf75 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 00:50:16 +0000 Subject: [PATCH 2/3] fix: give each branch its own CD concurrency group `github.head_ref` is empty on push events, so every CD run shared the group `cd-`. Use `github.ref` so main and nightly-testing runs no longer queue behind (or cancel pending runs of) each other. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/cd-pipeline.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/cd-pipeline.yml b/.github/workflows/cd-pipeline.yml index b9d79581..d03971d3 100644 --- a/.github/workflows/cd-pipeline.yml +++ b/.github/workflows/cd-pipeline.yml @@ -5,7 +5,7 @@ on: branches: [ "main", "nightly-testing" ] concurrency: - group: cd-${{ github.head_ref }} + group: cd-${{ github.ref }} cancel-in-progress: false jobs: From cf4f917f560463169347688e5d08d5f334448a63 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 00:50:17 +0000 Subject: [PATCH 3/3] fix: reuse one pull request for main toolchain updates The PR branch was named after the toolchain version, so each new release candidate opened a new PR and left the previous one open. Use a fixed branch so the existing PR is updated in place instead. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/update-main-toolchain.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/update-main-toolchain.yml b/.github/workflows/update-main-toolchain.yml index bad927a4..a8df76cb 100644 --- a/.github/workflows/update-main-toolchain.yml +++ b/.github/workflows/update-main-toolchain.yml @@ -72,7 +72,7 @@ jobs: with: token: ${{ secrets.PARSEIT_TOKEN }} commit-message: "chore: update toolchain to ${{ steps.toolchain.outputs.toolchain_rev }}" - branch: update-main-toolchain-${{ steps.toolchain.outputs.toolchain_rev }} + branch: update-main-toolchain base: main delete-branch: true title: "chore: update toolchain to ${{ steps.toolchain.outputs.toolchain_rev }}"