From 8ba1a386245d4c562a599dac5993aca18053ca46 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Mon, 16 Dec 2024 11:31:43 -0500 Subject: [PATCH] chore: permit Lake failures in PR release CI --- .github/workflows/pr-release.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 6bdee3056e72..2b9ce49996ad 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -330,7 +330,7 @@ jobs: echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain git add lean-toolchain sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}",' lakefile.lean - lake update batteries + lake update batteries || echo "Failed to update Batteries." git add lakefile.lean lake-manifest.json git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" else @@ -339,7 +339,7 @@ jobs: # 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 - lake update batteries + lake update batteries || echo "Failed to update Batteries." git add lake-manifest.json git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}" fi