From 3fab804cb9a07a8ccd936205e301413bfdfd37fb Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 25 Aug 2020 14:45:23 -0400
Subject: Remove useless commit guessing logic

On GitLab, we don't need to base the job info on the PR number, since
it ought to be available from the git repo.  Removing the logic will
make the bench infrastructure more uniform.
---
 dev/bench/gitlab.sh | 42 ------------------------------------------
 1 file changed, 42 deletions(-)

(limited to 'dev/bench/gitlab.sh')

diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh
index 15f5c01ac6..38b4e25bde 100755
--- a/dev/bench/gitlab.sh
+++ b/dev/bench/gitlab.sh
@@ -52,15 +52,6 @@ check_variable "coq_opam_packages"
 new_coq_commit=$(git rev-parse HEAD^2)
 old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit)
 
-if which jq > /dev/null; then
-    :
-else
-    echo > /dev/stderr
-    echo "ERROR: \"jq\" program is not available." > /dev/stderr
-    echo > /dev/stderr
-    exit 1
-fi
-
 if echo "$num_of_iterations" | grep '^[1-9][0-9]*$' 2> /dev/null > /dev/null; then
     :
 else
@@ -76,39 +67,6 @@ working_dir="$PWD/_bench"
 log_dir=$working_dir/logs
 mkdir "$log_dir"
 
-if [ ! -z "${coq_pr_number}" ]; then
-    github_response="$(curl "https://api.github.com/repos/coq/coq/pulls/${coq_pr_number}")"
-    new_coq_repository="$(echo "${github_response}" | jq -r '.head.repo.clone_url')"
-    new_coq_commit="$(echo "${github_response}" | jq -r '.head.sha')"
-    old_coq_repository="$(echo "${github_response}" | jq -r '.base.repo.clone_url')"
-    old_coq_commit="$(echo "${github_response}" | jq -r '.base.sha')"
-    coq_pr_title="$(echo "${github_response}" | jq -r '.title')"
-    # for coqbot parsing purposes, coq_pr_number and coq_pr_comment_id must not have newlines
-    coq_pr_number="$(echo "${coq_pr_number}" | tr -d '\n' | tr -d '\r')"
-    coq_pr_comment_id="$(echo "${coq_pr_comment_id}" | tr -d '\n' | tr -d '\r')"
-
-    for val in "${new_coq_repository}" "${new_coq_commit}" "${old_coq_repository}" "${old_coq_commit}" "${coq_pr_title}"; do
-        if [ -z "$val" ] || [ "val" == "null" ]; then
-            echo 'ERROR: Invalid Response:' > /dev/stderr
-            echo "${github_response}" > /dev/stderr
-            echo "Info:" > /dev/stderr
-            curl -i "https://api.github.com/repos/coq/coq/pulls/${coq_pr_number}" > /dev/stderr
-            exit 1
-        fi
-    done
-
-    if [ -z "$BENCH_DEBUG" ]; then # if it's non-empty, this'll get
-                                   # printed later anyway.  But we
-                                   # want to see it always if we're
-                                   # automatically computing values
-        echo "DEBUG: new_coq_repository = $new_coq_repository"
-        echo "DEBUG: new_coq_commit = $new_coq_commit"
-        echo "DEBUG: old_coq_repository = $old_coq_repository"
-        echo "DEBUG: old_coq_commit = $old_coq_commit"
-    fi
-
-fi
-
 if [ ! -z "$BENCH_DEBUG" ]
 then
    echo "DEBUG: ocaml -version = `ocaml -version`"
-- 
cgit v1.2.3