| #! /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 |