# ASSUMPTIONS: # - the OPAM packages, specified by the user, are topologically sorted wrt. to the dependency relationship. # - all the variables below are set.
# 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
# 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
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=""
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}Old Rocq version ${old_coq_commit}"
comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${old_coq_commit}")${nl}${end_code_block}${nl}"
comment_text="${comment_text}${nl}${nl}New Rocq version ${new_coq_commit}"
comment_text="${comment_text}${nl}${nl}${start_code_block}${nl}$(git log -n 1 "${new_coq_commit}")${nl}${end_code_block}${nl}"
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 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 """"""
# Create an opam root and install Rocq # $1 = root_name {ex: NEW / OLD} # $2 = compiler name # $3 = git hash of Rocq to be installed # $4 = directory of coq opam archive # $5 = use flambda if nonempty
create_opam() {
local RUNNER="$1"
local OPAM_DIR="$working_dir/opam.$RUNNER"
local OCAML_VER="$2"
local COQ_HASH="$3"
local COQ_VER="$4"
local OPAM_COQ_DIR="$5"
local OPAM_OVERRIDE_URLS="$6"
local USE_FLAMBDA="$7"
# For some reason opam guesses an incorrect upper bound on the # number of jobs available on Travis, so we set it here manually:
opam var --global jobs=$number_of_processors >/dev/null if [ ! -z "$BENCH_DEBUG" ]; then opam config list; fi
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 install -qy -j$number_of_processors $initial_opam_packages if [ ! -z "$BENCH_DEBUG" ]; then opam repo list; fi
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_commit""$new_coq_version" \ "$new_coq_opam_archive_dir""$new_opam_override_urls""$new_ocaml_flambda"
new_coq_commit_long="$COQ_HASH_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
# Create an OPAM-root to which we will install the OLD version of Rocq.
create_opam "OLD""$old_ocaml_version""$old_coq_commit""$old_coq_version" \ "$old_coq_opam_archive_dir""$old_opam_override_urls""$old_ocaml_flambda"
old_coq_commit_long="$COQ_HASH_LONG"
# -------------------------------------------------------------------------------- # 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 coqide-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 echo"Testing NEW commit: $(date)" else export OPAMROOT="$old_opam_root"
COQ_HASH=$old_coq_commit_long echo"Testing OLD commit: $(date)" fi
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
for dep in $(opam install --show-actions "$coq_opam_package" | grep -o '∗\s*install\s*[^ ]*' | sed 's/∗\s*install\s*//g'); do # show-actions will print transitive deps # so we don't need to look at the skipped_packages ifecho"$failed_packages" | grep -q "^$dep "; then
skipped_packages="$skipped_packages
$coq_opam_package (dependency $dep failed)"
continue 3 fi done
# OPAM 2.0 likes to ignore the -j when it feels like :S so we # workaround that here.
opam var --global jobs=$number_of_processors >/dev/null
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 -v -b -j1 $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 ]; 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
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
coqide-server|coq) # don't render results for these
;;
*)
installable_coq_opam_packages="$installable_coq_opam_packages $coq_opam_package"
esac
# 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
# 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
# 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"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
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."
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
