#! /usr/bin/env bash

# ASSUMPTIONS:
# - the OPAM packages, specified by the user, are topologically sorted wrt. to the dependency relationship.
# - all the variables below are set.

set -e

BENCH_DEBUG=

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='```'

# Check that the required arguments are provided

check_variable () {
  if [ ! -v "$1" ]
  then
      echo "Variable $1 should be set"
      exit 1
  fi
}

#check_variable "BUILD_ID"
#check_variable "BUILD_URL"
#check_variable "JOB_NAME"
#check_variable "JENKINS_URL"
#check_variable "CI_JOB_URL"
#check_variable "CI_REPOSITORY_URL"

: "${coq_pr_number:=}"
: "${coq_pr_comment_id:=}"
: "${new_ocaml_version:=5.4.1}"
: "${old_ocaml_version:=5.4.1}"
: "${new_ocaml_flambda:=1}"
: "${old_ocaml_flambda:=1}"
: "${new_coq_repository:=${CI_REPOSITORY_URL:-.}}"
: "${old_coq_repository:=${CI_REPOSITORY_URL:-.}}"
: "${new_coq_opam_archive_git_uri:=https://github.com/coq/opam-coq-archive.git}"
: "${old_coq_opam_archive_git_uri:=https://github.com/coq/opam-coq-archive.git}"
: "${new_coq_opam_archive_git_branch:=master}"
: "${old_coq_opam_archive_git_branch:=master}"
: "${num_of_iterations:=1}"
: "${timeout:=3h}"
: "${coq_opam_packages:=rocq-stdlib rocq-bignums coq-hott coq-performance-tests-lite coq-engine-bench-lite rocq-elpi rocq-mathcomp-boot rocq-mathcomp-order rocq-mathcomp-ssreflect rocq-mathcomp-finite-group rocq-mathcomp-algebra rocq-mathcomp-solvable rocq-mathcomp-field rocq-mathcomp-group-representation coq-mathcomp-odd-order rocq-mathcomp-analysis coq-math-classes coq-corn coq-compcert rocq-equations rocq-metarocq-utils rocq-metarocq-common rocq-metarocq-template rocq-metarocq-pcuic rocq-metarocq-safechecker rocq-metarocq-erasure rocq-metarocq-translations coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto-with-bedrock coq-unimath coq-coquelicot coq-iris-examples coq-fourcolor coq-rewriter-perf-SuperFast coq-vst coq-category-theory coq-neural-net-interp-computed-lite}"
: "${coq_native:=}"
: "${auto_overlays:=1}"

# example: coq-hott.dev git+https://github.com/some-user/coq-hott#some-branch
# (make sure to include the version for the opam package, note that just https won't work)
: "${new_opam_override_urls:=}"
: "${old_opam_override_urls:=}"

if [ "$CI" ]; then
  : "${new_coq_commit:=$(git rev-parse HEAD^2)}"
  : "${old_coq_commit:=$(git merge-base HEAD^1 $new_coq_commit)}"
else
  echo New coq commit:
  read -r new_coq_commit
  new_coq_commit=$(git rev-parse "$new_coq_commit")
  echo "new_coq_commit=$new_coq_commit"

  echo Old coq commit:
  read -r old_coq_commit
  old_coq_commit=$(git rev-parse "$old_coq_commit")
  echo "old_coq_commit=$old_coq_commit"
fi

new_ocaml_switch=ocaml-base-compiler.$new_ocaml_version
old_ocaml_switch=ocaml-base-compiler.$old_ocaml_version

if echo "$num_of_iterations" | grep '^[1-9][0-9]*$' 2> /dev/null > /dev/null; then
    :
else
    echo
    echo "ERROR: num_of_iterations \"$num_of_iterations\" is not a positive integer." > /dev/stderr
    print_man_page_hint
    exit 1
fi

bench_dirname="_bench"
mkdir -p "${bench_dirname}"
working_dir="$PWD/${bench_dirname}"

log_dir=$working_dir/logs
mkdir "$log_dir"
export COQ_LOG_DIR=$log_dir

# maps CI project (first arg of "overlay")
# to space separated list of opam packages which use the project's url
declare -A auto_overlay_map
auto_overlay_map[stdlib]="rocq-stdlib"
auto_overlay_map[elpi]="rocq-elpi"
auto_overlay_map[equations]="rocq-equations"
auto_overlay_map[metarocq]="rocq-metarocq-utils rocq-metarocq-common rocq-metarocq-template rocq-metarocq-pcuic rocq-metarocq-safechecker rocq-metarocq-erasure rocq-metarocq-translations"

if [ "$auto_overlays" ]; then
  CI_PULL_REQUEST="${CI_COMMIT_REF_NAME#pr-}"
  overlay() {
    local project=$1
    local ov_url=$2
    local ov_ref=$3
    local ov_prnumber=$4
    local ov_prbranch=$5
    : "${ov_prbranch:=$ov_ref}"

    if [ "$CI_PULL_REQUEST" = "$ov_prnumber" ]; then
      for package in ${auto_overlay_map[$project]}; do
        new_opam_override_urls="$package.dev git+$ov_url#$ov_ref $new_opam_override_urls"
      done
    fi
  }
  for overlay in dev/ci/user-overlays/*.sh; do
    # the directory can be empty
    if [ -e "$overlay" ]; then
      . "$overlay"
    fi
  done
fi

echo "DEBUG: ocaml -version = $(ocaml -version)"
echo "DEBUG: working_dir = $working_dir"
echo "DEBUG: new_ocaml_switch = $new_ocaml_switch"
echo "DEBUG: new_coq_repository = $new_coq_repository"
echo "DEBUG: new_coq_commit = $new_coq_commit"
echo "DEBUG: new_coq_opam_archive_git_uri = $new_coq_opam_archive_git_uri"
echo "DEBUG: new_coq_opam_archive_git_branch = $new_coq_opam_archive_git_branch"
echo "DEBUG: old_ocaml_switch = $old_ocaml_switch"
echo "DEBUG: old_coq_repository = $old_coq_repository"
echo "DEBUG: old_coq_commit = $old_coq_commit"
echo "DEBUG: old_coq_opam_archive_git_uri = $old_coq_opam_archive_git_uri"
echo "DEBUG: old_coq_opam_archive_git_branch = $old_coq_opam_archive_git_branch"
echo "DEBUG: num_of_iterations = $num_of_iterations"
echo "DEBUG: coq_opam_packages = $coq_opam_packages"
echo "DEBUG: new_opam_override_urls = $new_opam_override_urls"
echo "DEBUG: old_opam_override_urls = $old_opam_override_urls"
echo "DEBUG: coq_pr_number = $coq_pr_number"
echo "DEBUG: coq_pr_comment_id = $coq_pr_comment_id"
echo "DEBUG: coq_native = $coq_native"
echo "DEBUG: auto_overlays = $auto_overlays"

# We put local binaries such as opam in .bin and extend PATH
BIN=$(pwd)/.bin
mkdir "$BIN"
wget https://github.com/ocaml/opam/releases/download/2.3.0/opam-2.3.0-x86_64-linux -O "$BIN"/opam
chmod +x "$BIN"/opam

export OPAMSKIPUPDATE=1 # stop opam from messing with our pin edits

# generate per file info in test suite and coq_makefile devs
export TIMED=1

export PATH="$BIN":$PATH

echo "Global env info:"
echo "----------------"
echo "pwd: $PWD"
echo "path: $PATH"
echo "opam version: `opam --version`"

number_of_processors=$(cat /proc/cpuinfo | grep '^processor *' | wc -l)

program_name="$0"
program_path=$(readlink -f "${program_name%/*}")

coqbot_url_prefix="https://coqbot.herokuapp.com/pendulum/"

# --------------------------------------------------------------------------------

# Some sanity checks of command-line arguments provided by the user that can be done right now.

if which perf > /dev/null; then
    echo -n
else
    echo > /dev/stderr
    echo "ERROR: \"perf\" program is not available." > /dev/stderr
    echo > /dev/stderr
    exit 1
fi

if which curl > /dev/null; then
    :
else
    echo > /dev/stderr
    echo "ERROR: \"curl\" program is not available." > /dev/stderr
    echo > /dev/stderr
    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
    echo > /dev/stderr
    exit 1
fi

if [ ! -d "$working_dir" ]; then
    echo > /dev/stderr
    echo "ERROR: \"$working_dir\" is not a directory." > /dev/stderr
    echo > /dev/stderr
    exit 1
fi

if [ ! -w "$working_dir" ]; then
    echo > /dev/stderr
    echo "ERROR: \"$working_dir\" is not writable." > /dev/stderr
    echo > /dev/stderr
    exit 1
fi

# --------------------------------------------------------------------------------

# Tell coqbot to update the initial comment, if we know which one to update
function coqbot_update_comment() {
    is_done="$1"
    comment_body="$2"
    uninstallable_packages="$3"

    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](${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}${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 Rocq 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 Rocq 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/rocq-prover/rocq/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
        if [ ! -z "${coq_pr_comment_id}" ]; then
            # Tell coqbot to update the in-progress comment
            curl -X POST --data-binary "${coq_pr_number}${nl}${coq_pr_comment_id}${nl}${comment_text}" "${coqbot_url_prefix}/update-comment"
        elif [ ! -z "${is_done}" ]; then
            # Tell coqbot to post a new comment that we're done benchmarking
            curl -X POST --data-binary "${coq_pr_number}${nl}${comment_text}" "${coqbot_url_prefix}/new-comment"
        fi
        if [ ! -z "${is_done}" ]; then
            # Tell coqbot to remove the `needs: benchmarking` label
            curl -X POST --data-binary "${coq_pr_number}" "${coqbot_url_prefix}/benchmarking-done"
        fi
    fi
}

# initial update to the comment, to say that we're in progress
coqbot_update_comment "" "" ""

# --------------------------------------------------------------------------------

zulip_post=""
if [[ $ZULIP_BENCH_BOT ]]; then
    pr_full=$(git log -n 1 --pretty=%s)
    pr_full=${pr_full#"[CI merge] PR #"}
    pr_num=${pr_full%%:*}
    pr_msg=${pr_full#*:}
    zulip_header="Bench at $CI_JOB_URL
Testing [$pr_msg](https://github.com/rocq-prover/rocq/pull/$pr_num)
On packages $coq_opam_packages
"

    # 24008 is the "github notifications" stream
    resp=$(curl -sSX POST https://rocq-prover.zulipchat.com/api/v1/messages \
    -u "$ZULIP_BENCH_BOT" \
    --data-urlencode type=stream \
    --data-urlencode to='240008' \
    --data-urlencode subject='Bench Notifications' \
    --data-urlencode content="$zulip_header")

    zulip_post=$(echo "$resp" | jq .id)
    case "$zulip_post" in
        ''|*[!0-9]*) # not an int
            echo "Failed to post to zulip: $resp"
            zulip_post=""
            ;;
    esac
fi

zulip_edit() {
    if ! [[ $zulip_post ]]; then return; fi
    ending=$1
    if [[ $rendered_results ]]; then
        msg="$zulip_header

~~~
$rendered_results
~~~

$ending
"
    else
        msg="$zulip_header

$ending
"
    fi
    curl -sSX PATCH https://rocq-prover.zulipchat.com/api/v1/messages/"$zulip_post" \
         -u "$ZULIP_BENCH_BOT" \
         --data-urlencode content="$msg" >/dev/null || echo "Failed to edit zulip post" >&2
}
zulip_autofail() {
    code=$?
    com=$BASH_COMMAND
    zulip_edit "Failed '$com' with exit code $code."
}
if [[ $zulip_post ]]; then trap zulip_autofail ERR; fi

# see https://github.com/rocq-prover/rocq/pull/15807
if [ "$(ulimit -s)" != "unlimited" ]; then
  ulimit -S -s $((2 * $(ulimit -s)))
fi

# Clone the indicated git-repository.

coq_dir="$working_dir/coq"
git clone -q "$new_coq_repository" "$coq_dir"
cd "$coq_dir"
git remote rename origin new_coq_repository
git remote add old_coq_repository "$old_coq_repository"
git fetch -q "$old_coq_repository"
git checkout -q $new_coq_commit

coq_opam_version=dev

# --------------------------------------------------------------------------------

new_opam_root="$working_dir/opam.NEW"
old_opam_root="$working_dir/opam.OLD"

# --------------------------------------------------------------------------------

old_coq_opam_archive_dir="$working_dir/old_coq_opam_archive"
git clone -q --depth 1 -b "$old_coq_opam_archive_git_branch" "$old_coq_opam_archive_git_uri" "$old_coq_opam_archive_dir"
new_coq_opam_archive_dir="$working_dir/new_coq_opam_archive"
git clone -q --depth 1 -b "$new_coq_opam_archive_git_branch" "$new_coq_opam_archive_git_uri" "$new_coq_opam_archive_dir"

initial_opam_packages="num zarith ocamlfind dune yojson camlzip"

# Create an opam root and install Rocq
# $1 = root_name {ex: NEW / OLD}
# $2 = compiler version
# $3 = directory of coq opam archive
# $4 = override urls
# $5 = use flambda if = "1"
create_opam() {

    local RUNNER="$1"
    local OPAM_DIR="$working_dir/opam.$RUNNER"
    local OCAML_VER="$2"
    local OPAM_COQ_DIR="$3"
    local OPAM_OVERRIDE_URLS="$4"
    local USE_FLAMBDA="$5"

    export OPAMROOT="$OPAM_DIR"
    export COQ_RUNNER="$RUNNER"

    opam init --disable-sandboxing -qn -j "$number_of_processors" --bare
    # Allow beta compiler switches
    opam repo add -q --set-default beta https://github.com/ocaml/ocaml-beta-repository.git
    # Allow experimental compiler switches
    opam repo add -q --set-default ocaml-pr https://github.com/ejgallego/ocaml-pr-repository.git
    # Rest of default switches
    opam repo add -q --set-default iris-dev "https://github.com/rocq-iris/opam.git"

    local comp_packages
    if [[ $USE_FLAMBDA = 1 ]];
    then comp_packages=--packages=ocaml-variants.${OCAML_VER}+options,ocaml-option-flambda
    else comp_packages=ocaml-base-compiler.$OCAML_VER
    fi

    opam switch create -qy -j "$number_of_processors" "ocaml-$RUNNER" $comp_packages
    eval $(opam env)

    if [ ! -z "$BENCH_DEBUG" ]; then opam config list; fi

    opam repo add -q --this-switch coq-core-dev "$OPAM_COQ_DIR/core-dev"  # For rocq-stdlib
    opam repo add -q --this-switch coq-extra-dev "$OPAM_COQ_DIR/extra-dev"
    opam repo add -q --this-switch coq-released "$OPAM_COQ_DIR/released"

    local override_package
    local url_or_package
    for url_or_package in $OPAM_OVERRIDE_URLS; do
      if [ "$override_package" ]; then
        echo "Setting source url for $override_package to $url_or_package in $RUNNER"
        # NB opam editor start seems to ignore -y but works with </dev/null
        OPAMEDITOR="echo 'url { src: \"$url_or_package\" }' >> " opam pin add -nye "$override_package" - </dev/null
        opam show "$override_package" --raw
        override_package=
      else
        override_package=$url_or_package
      fi
    done
    if [ "$override_package" ]; then
      >&2 echo "malformed opam_override_urls for $RUNNER (odd length)"
      zulip_edit "Bench failed: malformed opam_override_urls for $RUNNER (odd length)"
      exit 1
    fi

    opam pin add -y dune 3.23.1 # 3.24 not compatible with many packages

    opam install -qy -j "$number_of_processors" $initial_opam_packages
    if [ ! -z "$BENCH_DEBUG" ]; then opam repo list; fi

    echo "wrap-build-commands: [\"$program_path/wrapper.sh\"]" >> "$OPAM_DIR/config"

    if [ ! -z "$coq_native" ]; then opam install coq-native rocq-native; fi

}

# Create an OPAM-root to which we will install the NEW version of Rocq.
create_opam "NEW" "$new_ocaml_version" \
            "$new_coq_opam_archive_dir" "$new_opam_override_urls" "$new_ocaml_flambda"
cd "$coq_dir"
git checkout -q "$new_coq_commit"
new_coq_commit_long=$(git log --pretty=%H | head -n 1)
echo "new_coq_commit = $new_coq_commit"
echo "new_coq_commit_long = $new_coq_commit_long"

# pre build needed helpers (needs an opam switch)
dune build --root "$program_path/../.." -- dev/bench/render_results.exe dev/bench/render_line_results.exe rocq-devtools.install

render_results=$(readlink -f "$program_path/../../_build/default/dev/bench/render_results.exe")
render_line_results=$(readlink -f "$program_path/../../_build/default/dev/bench//render_line_results.exe")
timelog2html=$(readlink -f "$program_path/../../_build/default/dev/bench/rocqtimelog2html.exe")

# Create an OPAM-root to which we will install the OLD version of Rocq.
create_opam "OLD" "$old_ocaml_version" \
            "$old_coq_opam_archive_dir" "$old_opam_override_urls" "$old_ocaml_flambda"
git checkout -q "$old_coq_commit"
old_coq_commit_long=$(git log --pretty=%H | head -n 1)
echo "old_coq_commit = $old_coq_commit"
echo "old_coq_commit_long = $old_coq_commit_long"

installable_coq_opam_packages=""

zulip_edit "Opam setup, benching continues..."

format_vosize() {
  old=$(stat -c%s $2)
  new=$(stat -c%s $3)
  diff=$((new - old))
  diffpercent=$(((diff * 100) / $old))
  echo "$1 $old $new $diff $diffpercent%"
}

# --------------------------------------------------------------------------------
# Measure the compilation times of the specified OPAM packages in both switches

failed_packages=
skipped_packages=

# Generate per line timing info in devs that use coq_makefile
export TIMING=1
export PROFILING=1
export ROCQ_PROFILE_COMPONENTS=command,parse_command,partac.perform

# packages tied to the coq commit need to be pinned accordingly
core_packages='rocq-runtime coq-core rocq-core rocqide-server'

for coq_opam_package in $core_packages $coq_opam_packages; do

    export COQ_OPAM_PACKAGE=$coq_opam_package
    is_core=
    for core in $core_packages; do
      if [ "$coq_opam_package" = "$core" ]; then is_core=1; fi
    done
    if [[ $is_core ]]; then
      : not getting info from opam repo
    else
    if [ ! -z "$BENCH_DEBUG" ]; then
        opam list
        opam show $coq_opam_package || {
            failed_packages="$failed_packages
$coq_opam_package (unknown package)"
            continue
            }
    else
        # cause to skip with error if unknown package
        opam show $coq_opam_package >/dev/null || {
            failed_packages="$failed_packages
$coq_opam_package (unknown package)"
            continue
            }
    fi
    fi
    echo "coq_opam_package = $coq_opam_package"

    for RUNNER in NEW OLD; do

        export COQ_RUNNER=$RUNNER

        # perform measurements for the NEW/OLD commit (provided by the user)
        if [ $RUNNER = "NEW" ]; then
          export OPAMROOT="$new_opam_root"
          COQ_HASH=$new_coq_commit_long
        else
            export OPAMROOT="$old_opam_root"
            COQ_HASH=$old_coq_commit_long
        fi
        echo "Testing $RUNNER commit: $(date)"

        git checkout -q $COQ_HASH

        if { [ "$coq_opam_package" = rocq-core ] || [ "$coq_opam_package" = rocq-runtime ]; } \
             && ! [ -e $coq_opam_package.opam ]; then
          echo "Skipping $coq_opam_package for $RUNNER"
          continue 2
        fi

        if [ -e "$coq_opam_package.opam" ]; then
          local_opam_dir=.
        elif [ -e "stdlib/$coq_opam_package.opam" ]; then
          local_opam_dir=stdlib
        else
          local_opam_dir=
        fi
        if [[ $local_opam_dir ]]; then
          opam pin add -ny "$coq_opam_package.dev" -k path $local_opam_dir
        fi

        eval $(opam env)

        # If a given OPAM-package was already installed (as a
        # dependency of some OPAM-package that we have benchmarked
        # before), remove it.
        opam uninstall -q $coq_opam_package >/dev/null 2>&1

        # '∗' is a unicode star used by opam for packags to be installed
        for dep in $(opam install --show-actions "$coq_opam_package" | grep -o '∗\s*[^ ]*' | sed 's/∗\s*//g'); do
            # show-actions will print transitive deps
            # so we don't need to look at the skipped_packages
            if echo "$failed_packages" | grep -q "^$dep "; then
                skipped_packages="$skipped_packages
$coq_opam_package (dependency $dep failed)"
                continue 3
            fi
        done

        opam install $coq_opam_package -v -b -j "$number_of_processors" --deps-only -y \
             3>$log_dir/$coq_opam_package.$RUNNER.opam_install.deps_only.stdout.log 1>&3 \
             4>$log_dir/$coq_opam_package.$RUNNER.opam_install.deps_only.stderr.log 2>&4 || {
            failed_packages="$failed_packages
$coq_opam_package (dependency install failed in $RUNNER)"
            continue 2
            }

        if [ ! -z "$BENCH_DEBUG" ]; then ls -l $working_dir; fi

        for iteration in $(seq $num_of_iterations); do
            export COQ_ITERATION=$iteration
            _RES=0
            timeout "$timeout" opam install -y -v -b -j 1 $coq_opam_package \
                 3>$log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.stdout.log 1>&3 \
                 4>$log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.stderr.log 2>&4 || \
                _RES=$?
            if [ $_RES = 0 ] && [ -e $log_dir/$coq_opam_package.$RUNNER.$iteration.ncoms ];
            then
                echo $_RES > $log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.exit_status
                # "opam install" was successful.

                # Remove the benchmarked OPAM-package, unless this is the
                # very last iteration (we want to keep this OPAM-package
                # because other OPAM-packages we will benchmark later
                # might depend on it --- it would be a waste of time to
                # remove it now just to install it later)
                if [ $iteration != $num_of_iterations ]; then
                    opam uninstall -q $coq_opam_package
                fi
            elif [ $_RES = 0 ]; then
              # package became a virtual package (no commands were run), act as though it failed
              echo 127 > $log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.exit_status
              failed_packages="$failed_packages
$coq_opam_package (virtual package?) (in $RUNNER)"
              continue 3
            else
                # "opam install" failed.
                echo $_RES > $log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.exit_status
                failed_packages="$failed_packages
$coq_opam_package (in $RUNNER)"
                continue 3
            fi
        done

        # avoid opam downgrading rocq if some package has weird constraints
        # there is no "opam switch add-invariant" so we do this sed instead,
        # cf https://github.com/ocaml/opam/issues/6269
        if [ "$coq_opam_package" = "rocq-runtime" ]; then
          opam switch set-invariant --formula \
               "$(opam switch invariant | sed 's/]/ \"'"$coq_opam_package"'\"]/')"
        fi
    done

    case $coq_opam_package in
      rocqide-server|coq)
        # don't render results for these
        ;;
      *)
        installable_coq_opam_packages="$installable_coq_opam_packages $coq_opam_package"
    esac

    # --------------------------------------------------------------
    cat $log_dir/$coq_opam_package.$RUNNER.1.*.time || true
    cat $log_dir/$coq_opam_package.$RUNNER.1.*.perf || true

    # Print the intermediate results after we finish benchmarking each OPAM package
    if [ "$coq_opam_package" = "$(echo $coq_opam_packages | sed 's/ /\n/g' | tail -n 1)" ]; then

        # It does not make sense to print the intermediate results when
        # we finished bechmarking the very last OPAM package because the
        # next thing will do is that we will print the final results.
        # It would look lame to print the same table twice.
        :
    else

        echo "DEBUG: $render_results "$log_dir" $num_of_iterations 1 user_time_pdiff $installable_coq_opam_packages"
        rendered_results="$($render_results "$log_dir" $num_of_iterations 1 user_time_pdiff $installable_coq_opam_packages)"
        echo "${rendered_results}"
        # update the comment
        coqbot_update_comment "" "${rendered_results}" ""
        msg="Benching continues ($coq_opam_package done)..."
        if [ -n "$failed_packages" ]; then
            msg="$msg
Failed: $failed_packages
$skipped_packages"
        fi
        zulip_edit "$msg"
    fi

    # N.B. Not all packages end in .dev, e.g., coq-lambda-rust uses .dev.timestamp.
    # So we use a wildcard to catch such packages.
    coq_opam_package_nover=${coq_opam_package%%.*}
    new_base_path=$(echo "$new_opam_root/ocaml-NEW/.opam-switch/build/$coq_opam_package_nover".*/)
    old_base_path=$(echo "$old_opam_root/ocaml-OLD/.opam-switch/build/$coq_opam_package_nover".*/)

    # Generate per-file comparison
    for iteration in $(seq $num_of_iterations); do
        # opam logs prefix the printing with "- " so remove that
        # remove the base path for nicer printing and so the script can identify common files
        "$program_path"/../../tools/make-both-time-files.py --real \
            <(sed -e 's/^- //' -e "s:$new_base_path::" "$log_dir/$coq_opam_package.NEW.opam_install.$iteration.stdout.log") \
            <(sed -e 's/^- //' -e "s:$old_base_path::" "$log_dir/$coq_opam_package.OLD.opam_install.$iteration.stdout.log") \
            > "$log_dir/$coq_opam_package.BOTH.perfile_timings.$iteration.log"
    done

    # Generate HTML report for LAST run

    for vo in $(cd $new_base_path/; find . -name '*.vo'); do
        if [ -e $old_base_path/$vo ]; then
          format_vosize "$coq_opam_package/$vo" "$old_base_path/$vo" "$new_base_path/$vo" >> "$log_dir/vosize.log"
        fi

        # use profile if it exists, otherwise timing
        # NB: timelog2html sometimes randomly fails
        old_data=
        new_data=
        if [ -e "$old_base_path/$vo.prof.json.gz" ]; then
          old_data="$old_base_path/$vo.prof.json.gz"
        elif [ -e "$old_base_path/${vo%%o}.timing" ]; then
          old_data="$old_base_path/${vo%%o}.timing"
        fi
        if [ -e "$new_base_path/$vo.prof.json.gz" ]; then
          new_data="$new_base_path/$vo.prof.json.gz"
        elif [ -e "$new_base_path/${vo%%o}.timing" ]; then
          new_data="$new_base_path/${vo%%o}.timing"
        fi

        if [ "$old_data" ] && [ "$new_data" ]; then
          mkdir -p "$working_dir/html/$coq_opam_package/$(dirname "$vo")/"
          $timelog2html \
            "-o" "$working_dir/html/$coq_opam_package/${vo%%o}.html" \
            "-raw-o" "$working_dir/html/$coq_opam_package/${vo%%o}.rocq-timediff" \
            "$new_base_path/${vo%%o}" \
            "$old_data" \
            "$new_data" \
            || echo "Failed (code $?): timelog2html for $vo on $old_data $new_data"
        fi
    done
done

# postprocess full vosize log (sort by % change then absolute change)
sort -r -n -k 5 -k 4 "$log_dir/vosize.log" > "$log_dir/vosize.sorted.log"
mv "$log_dir/vosize.sorted.log" "$log_dir/vosize.log"

# 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

# Measured data for each `$coq_opam_package`, `$iteration`, `status \in {NEW,OLD}`:
#
#     - $working_dir/$coq_opam_package.$status.$iteration.time
#       => output of /usr/bin/time --format="%U" ...
#
#     - $working_dir/$coq_opam_package.NEW.$iteration.perf
#       => output of perf stat -e instructions:u,cycles:u ...
#
# The next script processes all these files and prints results in a table.

# Generate per-file comparison for everything at once
new_base_path=$new_opam_root/ocaml-NEW/.opam-switch/build/
old_base_path=$old_opam_root/ocaml-OLD/.opam-switch/build/
for iteration in $(seq $num_of_iterations); do
    "$program_path"/../../tools/make-both-time-files.py --real \
        <(sed -e 's/^- //' -e "s:$new_base_path::" "$log_dir/"*".NEW.opam_install.$iteration.stdout.log") \
        <(sed -e 's/^- //' -e "s:$old_base_path::" "$log_dir/"*".OLD.opam_install.$iteration.stdout.log") \
        > "$log_dir/ALL.BOTH.perfile_timings.$iteration.log"
done

# timings data
timings=$working_dir/timings
mkdir -p $timings

# Print line by line slow downs and speed ups
if [ -d "$working_dir/html" ]; then # might not exist if all jobs failed
cd "$working_dir/html"
$render_line_results
# Move line timing files to timings folder (they will become artifacts)
mv fast_table slow_table timings_table $timings

# html tables don't get generated if the bench is run locally ie without CI variables
for f in fast_table.html slow_table.html timings_table.html; do
    if [ -f "$f" ]; then mv "$f" $timings; fi
done
fi

echo "INFO: workspace = ${CI_JOB_URL:-.}/artifacts/browse/${bench_dirname}"

# Print the final results.
if [ -z "$installable_coq_opam_packages" ]; then
    # Tell the user that none of the OPAM-package(s) the user provided
    # /are installable.
    printf "\n\nINFO: failed to install: $coq_opam_packages"
    coqbot_update_comment "done" "" "$coq_opam_packages"
    exit 1
fi

echo "DEBUG: $render_results $log_dir $num_of_iterations 1 user_time_pdiff $installable_coq_opam_packages"
rendered_results="$($render_results "$log_dir" $num_of_iterations 1 user_time_pdiff $installable_coq_opam_packages)"
echo "${rendered_results}"
echo "${rendered_results}" > $timings/bench_summary

echo "INFO: per line timing: ${CI_JOB_URL:-.}/artifacts/browse/${bench_dirname}/html/"

cd "$coq_dir"
echo INFO: Old Rocq version
git log -n 1 "$old_coq_commit"
echo INFO: New Rocq version
git log -n 1 "$new_coq_commit"

if [ -n "$failed_packages" ]; then
    not_installable_coq_opam_packages=$failed_packages
    if [ -n "$skipped_packages" ]; then
        not_installable_coq_opam_packages="$not_installable_coq_opam_packages
$skipped_packages"
    fi
else # in case the failed package detection is bugged
    not_installable_coq_opam_packages=$(comm -23 <(echo $coq_opam_packages | sed 's/ /\n/g' | sort | uniq) <(echo $installable_coq_opam_packages | sed 's/ /\n/g' | sort | uniq) | sed 's/\t//g')
fi

coqbot_update_comment "done" "${rendered_results}" "${not_installable_coq_opam_packages}"

touch $timings/bench_failures
if [ -n "$not_installable_coq_opam_packages" ]; then
    # Tell the user that some of the provided OPAM-package(s)
    # is/are not installable.
    printf '\n\nINFO: failed to install %s\n' "$not_installable_coq_opam_packages" | tee $timings/bench_failures
    zulip_edit "Bench complete, failed to install packages:
$not_installable_coq_opam_packages"
    exit 1
fi

zulip_edit "Bench complete: all packages successfully installed."