diff options
Diffstat (limited to 'dev/bench/gitlab.sh')
| -rwxr-xr-x | dev/bench/gitlab.sh | 82 |
1 files changed, 34 insertions, 48 deletions
diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index 15f5c01ac6..7625e4e7f7 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -12,6 +12,9 @@ r='\033[0m' # reset (all attributes off) b='\033[1m' # bold u='\033[4m' # underline nl=$'\n' +bt='`' # backtick +start_code_block='```' +end_code_block='```' number_of_processors=$(cat /proc/cpuinfo | grep '^processor *' | wc -l) @@ -36,6 +39,7 @@ echo $PWD #check_variable "BUILD_URL" #check_variable "JOB_NAME" #check_variable "JENKINS_URL" +check_variable "CI_JOB_URL" check_variable "coq_pr_number" check_variable "coq_pr_comment_id" check_variable "new_ocaml_switch" @@ -52,15 +56,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 @@ -70,45 +65,13 @@ else exit 1 fi -mkdir -p "_bench" -working_dir="$PWD/_bench" +bench_dirname="_bench" +mkdir -p "${bench_dirname}" +working_dir="$PWD/${bench_dirname}" 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`" @@ -151,6 +114,15 @@ else exit 1 fi +if which du > /dev/null; then + : +else + echo > /dev/stderr + echo "ERROR: \"du\" program is not available." > /dev/stderr + echo > /dev/stderr + exit 1 +fi + if [ ! -e "$working_dir" ]; then echo > /dev/stderr echo "ERROR: \"$working_dir\" does not exist." > /dev/stderr @@ -188,22 +160,31 @@ function coqbot_update_comment() { if [ ! -z "${coq_pr_number}" ]; then comment_text="" + artifact_text="" if [ -z "${is_done}" ]; then comment_text="in progress, " + artifact_text="eventually " else comment_text="" + artifact_text="" fi - comment_text="Benchmarking ${comment_text}log available [here](${BUILD_URL}/console), workspace available [here](${JENKINS_URL}/view/benchmarking/job/${JOB_NAME}/ws/${BUILD_ID})" + comment_text="Benchmarking ${comment_text}log available [here](${CI_JOB_URL}) ([raw log here](${CI_JOB_URL}/raw)), artifacts ${artifact_text}available for [download](${CI_JOB_URL}/artifacts/download) and [browsing](${CI_JOB_URL}/artifacts/browse)" if [ ! -z "${comment_body}" ]; then - comment_text="${comment_text}${nl}"'```'"${nl}${comment_body}${nl}"'```' + comment_text="${comment_text}${nl}${start_code_block}${nl}${comment_body}${nl}${end_code_block}" fi if [ ! -z "${uninstallable_packages}" ]; then comment_text="${comment_text}${nl}The following packages failed to install: ${uninstallable_packages}" fi + comment_text="${comment_text}${nl}${nl}<details><summary>Old Coq version ${old_coq_commit}</summary>" + comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${old_coq_commit}")${nl}${end_code_block}${nl}</details>" + comment_text="${comment_text}${nl}${nl}<details><summary>New Coq version ${new_coq_commit}</summary>" + comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${new_coq_commit}")${nl}${end_code_block}${nl}</details>" + comment_text="${comment_text}${nl}${nl}[Diff: ${bt}${old_coq_commit}..${new_coq_commit}${bt}](https://github.com/coq/coq/compare/${old_coq_commit}..${new_coq_commit})" + # if there's a comment id, we update the comment while we're # in progress; otherwise, we wait until the end to post a new # comment @@ -458,6 +439,11 @@ for coq_opam_package in $sorted_coq_opam_packages; do done done +# Since we do not upload all files, store a list of the files +# available so that if we at some point want to tweak which files we +# upload, we'll know which ones are available for upload +du -ha "$working_dir" > "$working_dir/files.listing" + # The following directories in $working_dir are no longer used: # # - coq, opam.OLD, opam.NEW @@ -472,7 +458,7 @@ done # # The next script processes all these files and prints results in a table. -echo "INFO: workspace = https://ci.inria.fr/coq/view/benchmarking/job/$JOB_NAME/ws/$BUILD_ID" +echo "INFO: workspace = ${CI_JOB_URL}/artifacts/browse/${bench_dirname}" # Print the final results. if [ -z "$installable_coq_opam_packages" ]; then @@ -486,7 +472,7 @@ else rendered_results="$($program_path/render_results "$log_dir" $num_of_iterations $new_coq_commit_long $old_coq_commit_long 0 user_time_pdiff $installable_coq_opam_packages)" echo "${rendered_results}" - echo "INFO: per line timing: https://ci.inria.fr/coq/job/$JOB_NAME/ws/$BUILD_ID/html/" + echo "INFO: per line timing: ${CI_JOB_URL}/artifacts/browse/${bench_dirname}/html/" cd "$coq_dir" echo INFO: Old Coq version |