Automatically populating commit fields?

[JasonGross]

Can we add a parameter that can be filled with the PR number, and if it's non-empty, then the new_coq_repository, new_coq_commit, old_coq_repository, and old_coq_commit get filled automatically according to the following script?

if [ ! -z "${pr_number}" ]; then
  RESPONSE="$(curl "https://api.github.com/repos/coq/coq/pulls/${pr_number}")"
  new_coq_repository="$(echo "${RESPONSE}" | jq -r '.head.repo.clone_url')"
  new_coq_commit="$(echo "${RESPONSE}" | jq -r '.head.sha')"
  old_coq_repository="$(echo "${RESPONSE}" | jq -r '.base.repo.clone_url')"
  old_coq_commit="$(echo "${RESPONSE}" | jq -r '.base.sha')"

  for val in "${new_coq_repository}" "${new_coq_commit}" "${old_coq_repository}" "${old_coq_commit}"; do
    if [ -z "$val" ] || [ "val" == "null" ]; then
      echo 'ERROR: Invalid Response:'
      echo "${RESPONSE}"
      echo "Info:"
      curl -i "https://api.github.com/repos/coq/coq/pulls/${pr_number}"
      exit 1
    fi
  done
fi

consider (-r is for --raw-output):

$ curl https://api.github.com/repos/coq/coq/pulls/12197 | jq -r '.number,.base.sha,.base.repo.clone_url,.head.sha,.head.repo.clone_url'
12197
62105448c40adfff86c9b191e6de2335839a7b37
https://github.com/coq/coq.git
3dbb4e68f853cb0414aaf234ba186ad5e22ad31f
https://github.com/JasonGross/coq.git

I think this would both make benches easier to set up, and would make progress towards coq/bot#8

[JasonGross]

If it's not done already, we could also auto-update the display name (via the set-build-display-name CLI) which we'd obtain via $(echo "${RESPONSE}" | jq -r '.title') (or even "PR #$(echo "${RESPONSE}" | jq -r '.number'): $(echo "${RESPONSE}" | jq -r '.title')")