sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

feat: move lean-pr-testing-NNNN branches to a fork (#8933)

Browse Source 
This PR changes the CI setup to generate `lean-pr-testing-NNNN` branches
for Mathlib on the `leanprover-community/mathlib4-nightly-testing` fork,
rather than on the main repo.
This commit is contained in:
Kim Morrison
2025-06-24 13:30:43 +10:00
committed by GitHub
parent 6970d77ae4
commit 8fe068ef68
5 changed files with 12 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
.github/workflows/ci.yml vendored
View File

@@ -421,6 +421,6 @@ jobs:
GITHUB_TOKEN: ${{ secrets.RELEASE_INDEX_TOKEN }}
- name: Update toolchain on mathlib4's nightly-testing branch
run: |
gh workflow -R leanprover-community/mathlib4 run nightly_bump_toolchain.yml
gh workflow -R leanprover-community/mathlib4-nightly-testing run nightly_bump_toolchain.yml
env:
GITHUB_TOKEN: ${{ secrets.MATHLIB4_BOT }}

4
.github/workflows/pr-release.yml vendored
View File

@@ -167,7 +167,7 @@ jobs:
echo "The merge base of this PR coincides with the nightly release"
BATTERIES_REMOTE_TAGS="$(git ls-remote https://github.com/leanprover-community/batteries.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
MATHLIB_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-nightly-testing.git nightly-testing-"$MOST_RECENT_NIGHTLY")"
if [[ -n "$BATTERIES_REMOTE_TAGS" ]]; then
echo "... and Batteries has a 'nightly-testing-$MOST_RECENT_NIGHTLY' tag."
@@ -355,7 +355,7 @@ jobs:
if: steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
uses: actions/checkout@v4
with:
repository: leanprover-community/mathlib4
repository: leanprover-community/mathlib4-nightly-testing
token: ${{ secrets.MATHLIB4_BOT }}
ref: nightly-testing
fetch-depth: 0 # This ensures we check out all tags and branches.

3
doc/dev/index.md
View File

@@ -85,5 +85,6 @@ such that changing files in `Init` doesn't force a full rebuild of `Lean`.
You can test a Lean PR against Mathlib and Batteries by rebasing your PR
on to `nightly-with-mathlib` branch. (It is fine to force push after rebasing.)
CI will generate a branch of Mathlib and Batteries called `lean-pr-testing-NNNN`
that uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
on the `leanprover-community/mathlib4-nightly-testing` fork of Mathlib.
This branch uses the toolchain for your PR, and will report back to the Lean PR with results from Mathlib CI.
See https://leanprover-community.github.io/contribute/tags_and_branches.html for more details.

9
script/mathlib-bench
View File

@@ -5,8 +5,11 @@ set -euo pipefail
[ $# -eq 1 ] || (echo "usage: $0 <lean4 PR #>"; exit 1)
echo "Warning: the speedcenter is probably not listening on mathlib4-nightly-testing yet."
echo "If you're using this script, please contact @kim-em or @Kha to get this set up, and then remove this notice."
LEAN_PR=$1
PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
PR_RESPONSE=$(gh api repos/leanprover-community/mathlib4-nightly-testing/pulls -X POST -f head=lean-pr-testing-$LEAN_PR -f base=nightly-testing -f title="leanprover/lean4#$LEAN_PR benchmarking" -f draft=true -f body="ignore me")
PR_NUMBER=$(echo "$PR_RESPONSE" | jq '.number')
echo "opened https://github.com/leanprover-community/mathlib4/pull/$PR_NUMBER"
gh api repos/leanprover-community/mathlib4/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null
echo "opened https://github.com/leanprover-community/mathlib4-nightly-testing/pull/$PR_NUMBER"
gh api repos/leanprover-community/mathlib4-nightly-testing/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null

2
tests/lean/run/grind_trig.lean
View File

@@ -30,5 +30,5 @@ example (f : R → Nat) : 4 * f ((cos x + sin x)^2) ≠ 2 + f (2 * cos x * sin x
example (f : R → Nat) : max 3 (4 * f ((cos x + sin x)^2)) ≠ 2 + f (2 * cos x * sin x + 1) := by
grind
-- See https://github.com/leanprover-community/mathlib4/blob/nightly-testing/MathlibTest/grind/trig.lean
-- See https://github.com/leanprover-community/mathlib4-nightly-testing/blob/nightly-testing/MathlibTest/grind/trig.lean
-- for the Mathlib version of this test, using the real `ℝ`, `cos`, `sin`, and `cos_sq_and_sin_sq` declarations.