Merge PR #12816: Fixes #12787: anomaly of tactic injection in the presence of artificial dependencies disappearing by reduction

Reviewed-by: ppedrot

1 files changed, 510 insertions, 0 deletions

diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh
new file mode 100755
index 0000000000..5423f30aba
--- /dev/null
+++ b/dev/bench/gitlab.sh
@@ -0,0 +1,510 @@
+#! /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=1
+
+r='\033[0m'          # reset (all attributes off)
+b='\033[1m'          # bold
+u='\033[4m'          # underline
+nl=$'\n'
+
+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/"
+
+# Check that the required arguments are provided
+
+check_variable () {
+  if [ ! -v "$1" ]
+  then
+      echo "Variable $1 should be set"
+      exit 1
+  fi
+}
+
+echo $PWD
+
+#check_variable "BUILD_ID"
+#check_variable "BUILD_URL"
+#check_variable "JOB_NAME"
+#check_variable "JENKINS_URL"
+check_variable "coq_pr_number"
+check_variable "coq_pr_comment_id"
+check_variable "new_ocaml_switch"
+check_variable "new_coq_repository"
+check_variable "new_coq_commit"
+check_variable "new_coq_opam_archive_git_uri"
+check_variable "new_coq_opam_archive_git_branch"
+check_variable "old_ocaml_switch"
+check_variable "old_coq_repository"
+old_coq_commit="609152467f4d717713b7ea700f5155fc9f341cd7"
+check_variable "old_coq_opam_archive_git_uri"
+check_variable "old_coq_opam_archive_git_branch"
+check_variable "num_of_iterations"
+check_variable "coq_opam_packages"
+
+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
+    echo
+    echo "ERROR: num_of_iterations \"$num_of_iterations\" is not a positive integer." > /dev/stderr
+    print_man_page_hint
+    exit 1
+fi
+
+mkdir -p "_bench"
+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`"
+   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: coq_pr_number = $coq_pr_number"
+   echo "DEBUG: coq_pr_comment_id = $coq_pr_comment_id"
+fi
+
+# --------------------------------------------------------------------------------
+
+# 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 [ ! -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
+
+coq_opam_packages_on_separate_lines=$(echo "$coq_opam_packages" | sed 's/ /\n/g')
+if [ $(echo "$coq_opam_packages_on_separate_lines" | wc -l) != $(echo "$coq_opam_packages_on_separate_lines" | sort | uniq | wc -l) ]; then
+    echo "ERROR: The provided set of OPAM packages contains duplicates."
+    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=""
+
+        if [ -z "${is_done}" ]; then
+            comment_text="in progress, "
+        else
+            comment_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})"
+
+        if [ ! -z "${comment_body}" ]; then
+            comment_text="${comment_text}${nl}"'```'"${nl}${comment_body}${nl}"'```'
+        fi
+
+        if [ ! -z "${uninstallable_packages}" ]; then
+            comment_text="${comment_text}${nl}The following packages failed to install: ${uninstallable_packages}"
+        fi
+
+        # 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 "" "" ""
+
+# --------------------------------------------------------------------------------
+
+# 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
+
+official_coq_branch=master
+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 ocamlfind dune"
+
+# Create an opam root and install Coq
+# $1 = root_name {ex: NEW / OLD}
+# $2 = compiler name
+# $3 = git hash of Coq to be installed
+# $4 = directory of coq opam archive
+create_opam() {
+
+    local RUNNER="$1"
+    local OPAM_DIR="$working_dir/opam.$RUNNER"
+    local OPAM_COMP="$2"
+    local COQ_HASH="$3"
+    local OPAM_COQ_DIR="$4"
+
+    export OPAMROOT="$OPAM_DIR"
+
+    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://gitlab.mpi-sws.org/FP/opam-dev.git"
+
+    opam switch create -qy -j$number_of_processors "$OPAM_COMP"
+    eval $(opam env)
+
+    # For some reason opam guesses an incorrect upper bound on the
+    # number of jobs available on Travis, so we set it here manually:
+    opam config set-global jobs $number_of_processors
+    if [ ! -z "$BENCH_DEBUG" ]; then opam config list; fi
+
+    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"
+
+    opam install -qy -j$number_of_processors $initial_opam_packages
+    if [ ! -z "$BENCH_DEBUG" ]; then opam repo list; fi
+
+    cd "$coq_dir"
+    if [ ! -z "$BENCH_DEBUG" ]; then echo "DEBUG: $1_coq_commit = $COQ_HASH"; fi
+
+    git checkout -q $COQ_HASH
+    COQ_HASH_LONG=$(git log --pretty=%H | head -n 1)
+
+    echo "$1_coq_commit_long = $COQ_HASH_LONG"
+
+    _RES=0
+    /usr/bin/time -o "$log_dir/coq.$RUNNER.1.time" --format="%U %M %F" \
+                  perf stat -e instructions:u,cycles:u -o "$log_dir/coq.$RUNNER.1.perf" \
+                  opam pin add -y -b -j "$number_of_processors" --kind=path coq.dev . \
+                  3>$log_dir/coq.$RUNNER.opam_install.1.stdout 1>&3 \
+                  4>$log_dir/coq.$RUNNER.opam_install.1.stderr 2>&4 || \
+        _RES=$?
+    if [ $_RES = 0 ]; then
+        echo "Coq ($RUNNER) installed successfully"
+    else
+        echo "ERROR: \"opam install coq.$coq_opam_version\" has failed (for the $RUNNER commit = $COQ_HASH_LONG)."
+        exit 1
+    fi
+
+    # we don't multi compile coq for now (TODO some other time)
+    # the render needs all the files so copy them around
+    for it in $(seq 2 $num_of_iterations); do
+        cp "$log_dir/coq.$RUNNER.1.time" "$log_dir/coq.$RUNNER.$it.time"
+        cp "$log_dir/coq.$RUNNER.1.perf" "$log_dir/coq.$RUNNER.$it.perf"
+    done
+
+}
+
+# Create an OPAM-root to which we will install the NEW version of Coq.
+create_opam "NEW" "$new_ocaml_switch" "$new_coq_commit" "$new_coq_opam_archive_dir"
+new_coq_commit_long="$COQ_HASH_LONG"
+
+# Create an OPAM-root to which we will install the OLD version of Coq.
+create_opam "OLD" "$old_ocaml_switch" "$old_coq_commit" "$old_coq_opam_archive_dir"
+old_coq_commit_long="$COQ_HASH_LONG"
+# --------------------------------------------------------------------------------
+# Measure the compilation times of the specified OPAM packages in both switches
+
+# Sort the opam packages
+sorted_coq_opam_packages=$("${program_path}/sort-by-deps.sh" ${coq_opam_packages})
+if [ ! -z "$BENCH_DEBUG" ]
+then
+   echo "DEBUG: sorted_coq_opam_packages = ${sorted_coq_opam_packages}"
+fi
+
+# Generate per line timing info in devs that use coq_makefile
+export TIMING=1
+
+# The following variable will be set in the following cycle:
+installable_coq_opam_packages=coq
+
+for coq_opam_package in $sorted_coq_opam_packages; do
+
+    if [ ! -z "$BENCH_DEBUG" ]; then
+        opam list
+        echo "DEBUG: coq_opam_package = $coq_opam_package"
+        opam show $coq_opam_package || continue 2
+    else
+        # cause to skip with error if unknown package
+        opam show $coq_opam_package >/dev/null || continue 2
+    fi
+
+    for RUNNER in NEW OLD; do
+
+        # perform measurements for the NEW/OLD commit (provided by the user)
+        if [ $RUNNER = "NEW" ]; then
+            export OPAMROOT="$new_opam_root"
+            echo "Testing NEW commit: $(date)"
+        else
+            export OPAMROOT="$old_opam_root"
+            echo "Testing OLD commit: $(date)"
+        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
+
+        # OPAM 2.0 likes to ignore the -j when it feels like :S so we
+        # workaround that here.
+        opam config set-global jobs $number_of_processors
+
+        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 1>&3 \
+             4>$log_dir/$coq_opam_package.$RUNNER.opam_install.deps_only.stderr 2>&4 || continue 2
+
+        opam config set-global jobs 1
+
+        if [ ! -z "$BENCH_DEBUG" ]; then ls -l $working_dir; fi
+
+        for iteration in $(seq $num_of_iterations); do
+            _RES=0
+            /usr/bin/time -o "$log_dir/$coq_opam_package.$RUNNER.$iteration.time" --format="%U %M %F" \
+                 perf stat -e instructions:u,cycles:u -o "$log_dir/$coq_opam_package.$RUNNER.$iteration.perf" \
+                    opam install -v -b -j1 $coq_opam_package \
+                     3>$log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.stdout 1>&3 \
+                     4>$log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.stderr 2>&4 || \
+                _RES=$?
+            if [ $_RES = 0 ];
+            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
+            else
+                # "opam install" failed.
+                echo $_RES > $log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.exit_status
+                continue 3
+            fi
+        done
+    done
+
+    installable_coq_opam_packages="$installable_coq_opam_packages $coq_opam_package"
+
+    # --------------------------------------------------------------
+
+    # Print the intermediate results after we finish benchmarking each OPAM package
+    if [ "$coq_opam_package" = "$(echo $sorted_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: $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"
+        if [ ! -z "$BENCH_DEBUG" ]; then
+            cat $log_dir/$coq_opam_package.$RUNNER.1.time || true
+            cat $log_dir/$coq_opam_package.$RUNNER.1.perf || true
+        fi
+        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}"
+        # update the comment
+        coqbot_update_comment "" "${rendered_results}" ""
+    fi
+
+    # Generate HTML report for LAST run
+
+    # 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.  This will have to be updated if
+    # ever there is a package that uses some different naming scheme.
+    new_base_path=$new_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/
+    old_base_path=$old_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/
+    for vo in `cd $new_opam_root/$new_base_path/; find -name '*.vo'`; do
+        if [ -e $old_opam_root/$old_base_path/${vo%%o}.timing -a \
+                -e $new_opam_root/$new_base_path/${vo%%o}.timing ]; then
+            mkdir -p $working_dir/html/$coq_opam_package/`dirname $vo`/
+            $program_path/timelog2html $new_opam_root/$new_base_path/${vo%%o} \
+                                       $old_opam_root/$old_base_path/${vo%%o}.timing \
+                                       $new_opam_root/$new_base_path/${vo%%o}.timing > \
+                                       $working_dir/html/$coq_opam_package/${vo%%o}.html
+        fi
+    done
+done
+
+# 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.
+
+echo "INFO: workspace = https://ci.inria.fr/coq/view/benchmarking/job/$JOB_NAME/ws/$BUILD_ID"
+
+# 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: $sorted_coq_opam_packages"
+    coqbot_update_comment "done" "" "$sorted_coq_opam_packages"
+    exit 1
+else
+    echo "DEBUG: $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"
+    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/"
+
+    cd "$coq_dir"
+    echo INFO: Old Coq version
+    git log -n 1 "$old_coq_commit"
+    echo INFO: New Coq version
+    git log -n 1 "$new_coq_commit"
+
+    not_installable_coq_opam_packages=`comm -23 <(echo $sorted_coq_opam_packages | sed 's/ /\n/g' | sort | uniq) <(echo $installable_coq_opam_packages | sed 's/ /\n/g' | sort | uniq) | sed 's/\t//g'`
+
+    coqbot_update_comment "done" "${rendered_results}" "${not_installable_coq_opam_packages}"
+
+    exit_code=0
+
+    if [ ! -z "$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"
+        exit_code=1
+    fi
+
+    exit 0
+fi