Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728729730731732733734735736737738739740741742743744745746747748749750751752753754755756757758759760761762763764765766767768769770771772773774775776777778779780781782783784785786787788789790791792793794795796797798799800801802803804805806807808#! /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' # boldu='\033[4m' # underlinenl=$'\n'bt='`' # backtickstart_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_versionold_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 1fi
bench_dirname="_bench"mkdir -p "${bench_dirname}"working_dir="$PWD/${bench_dirname}"
log_dir=$working_dir/logsmkdir "$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 urldeclare -A auto_overlay_mapauto_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 donefi
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 PATHBIN=$(pwd)/.binmkdir "$BIN"wget https://github.com/ocaml/opam/releases/download/2.3.0/opam-2.3.0-x86_64-linux -O "$BIN"/opamchmod +x "$BIN"/opam
export OPAMSKIPUPDATE=1 # stop opam from messing with our pin edits
# generate per file info in test suite and coq_makefile devsexport 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 -nelse echo > /dev/stderr echo "ERROR: \"perf\" program is not available." > /dev/stderr echo > /dev/stderr exit 1fi
if which curl > /dev/null; then :else echo > /dev/stderr echo "ERROR: \"curl\" program is not available." > /dev/stderr echo > /dev/stderr exit 1fi
if which du > /dev/null; then :else echo > /dev/stderr echo "ERROR: \"du\" program is not available." > /dev/stderr echo > /dev/stderr exit 1fi
if [ ! -e "$working_dir" ]; then echo > /dev/stderr echo "ERROR: \"$working_dir\" does not exist." > /dev/stderr echo > /dev/stderr exit 1fi
if [ ! -d "$working_dir" ]; then echo > /dev/stderr echo "ERROR: \"$working_dir\" is not a directory." > /dev/stderr echo > /dev/stderr exit 1fi
if [ ! -w "$working_dir" ]; then echo > /dev/stderr echo "ERROR: \"$working_dir\" is not writable." > /dev/stderr echo > /dev/stderr exit 1fi
# --------------------------------------------------------------------------------
# Tell coqbot to update the initial comment, if we know which one to updatefunction 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 progresscoqbot_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_URLTesting [$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="" ;; esacfi
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/15807if [ "$(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_repositorygit 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_makefileexport TIMING=1export PROFILING=1export ROCQ_PROFILE_COMPONENTS=command,parse_command,partac.perform
# packages tied to the coq commit need to be pinned accordinglycore_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="$msgFailed: $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 donedone
# 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 uploaddu -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 oncenew_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 datatimings=$working_dir/timingsmkdir -p $timings
# Print line by line slow downs and speed upsif [ -d "$working_dir/html" ]; then # might not exist if all jobs failedcd "$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 variablesfor f in fast_table.html slow_table.html timings_table.html; do if [ -f "$f" ]; then mv "$f" $timings; fidonefi
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 1fi
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 versiongit log -n 1 "$old_coq_commit"echo INFO: New Rocq versiongit 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" fielse # 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_failuresif [ -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 1fi
zulip_edit "Bench complete: all packages successfully installed."