Reviewer Tools - sagemath/sage GitHub Wiki

Bash scripts useful to review PRs locally.

Dependencies:

• GitHub CLI: https://cli.github.com
• jq: https://jqlang.github.io/jq

gh-review

Create a local branch named p/12345/description from a GitHub PR #12345.

Usage:gh-review 12345

#!/bin/bash
#set -ex
PR_NUMBER="$1"
BRANCH_NAME=p/$PR_NUMBER/$(gh pr view "$PR_NUMBER" --json headRefName | jq -r '.headRefName')

# Check if the branch already exists
if git show-ref --verify --quiet "refs/heads/$BRANCH_NAME"; then
  echo "Branch '$BRANCH_NAME' already exists."
  read -p "Do you want to delete the existing branch and re-checkout? [y/N]: " -r
  if [ $REPLY =~ ^[Yy]$ ](/sagemath/sage/wiki/-$REPLY-=~-^[Yy]$-); then
    # Delete the existing branch
    git branch -D "$BRANCH_NAME"
  else
    echo "Aborting the checkout process."
    exit 1
  fi
fi

gh pr checkout $PR_NUMBER -b "$BRANCH_NAME"

gh-close-merged:

Delete all local branches (created by gh-review) whose connected PR was merged in GitHub.

Usage: gh-close-merged

#!/bin/bash

# Iterate over all local branches
for branch in $(git branch | cut -c 3-); do
    # Check if the branch name matches the format
    if [ $branch =~ ^p/([0-9]+)/ ](/sagemath/sage/wiki/-$branch-=~-^p/([0-9]+)/-); then
        # Extract the PR number from the branch name
        branch_pr_number=${BASH_REMATCH[1]}

        # Get the state of the pull request
        pr_state=$(gh pr view $branch_pr_number --json state | jq -r '.state')

        # Check if the pull request is merged
        if [ $pr_state == "MERGED" ](/sagemath/sage/wiki/-$pr_state-==-"MERGED"-); then
            # Delete the local branch
            if git branch -D $branch; then
                echo "Branch $branch was deleted since pull request #$branch_pr_number was merged."
            else
                echo "Failed to delete branch $branch."
            fi
            echo "---"
        fi
    fi
done

gh-rename

Rename the current local branch to p/12345/description for the PR #12345 created from the branch. This is a utility for the author of the PR.

Usage:gh-rename 12345

#!/bin/bash
set -ex
PR_number=$(gh pr view --json number | jq -r '.number')
branch_name_github=$(gh pr view "$PR_number" --json headRefName | jq -r '.headRefName')

# Remove "p/" prefix if it exists
if [ "$branch_name_github" == p/* ](/sagemath/sage/wiki/-"$branch_name_github"-==-p/*-); then
  branch_name_github="${branch_name_github#p/}"
fi

# Reconstruct the string with the number inserted
new_branch_name="p/${PR_number}/$branch_name_github"

git branch -m $new_branch_name

Acknowledgment: Thanks, ChatGPT!