mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
8fe068ef68
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.
16 lines
864 B
Bash
Executable File
16 lines
864 B
Bash
Executable File
#! /bin/env bash
|
|
# Open a Mathlib4 PR for benchmarking a given Lean 4 PR
|
|
|
|
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-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-nightly-testing/pull/$PR_NUMBER"
|
|
gh api repos/leanprover-community/mathlib4-nightly-testing/issues/$PR_NUMBER/comments -X POST -f body="!bench" > /dev/null
|