Skip to content

Commit

Permalink
Fix bench with and without split stdlib
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Dec 6, 2024
1 parent 73de141 commit 7aa65aa
Showing 1 changed file with 30 additions and 62 deletions.
92 changes: 30 additions & 62 deletions dev/bench/bench.sh
Original file line number Diff line number Diff line change
Expand Up @@ -426,35 +426,6 @@ create_opam() {

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

for package in coq-core rocq-core coqide-server; do
export COQ_OPAM_PACKAGE=$package
export COQ_ITERATION=1

# build stdlib with -j 1 to get nicer timings
local this_nproc=$number_of_processors
if [ "$package" = rocq-core ]; then this_nproc=1; fi

_RES=0
opam pin add -y -b -j "$this_nproc" --kind=path $package.$COQ_VER . \
3>$log_dir/$package.$RUNNER.opam_install.1.stdout.log 1>&3 \
4>$log_dir/$package.$RUNNER.opam_install.1.stderr.log 2>&4 || \
_RES=$?
if [ $_RES = 0 ]; then
echo "$package ($RUNNER) installed successfully"
else
echo "ERROR: \"opam install $package.$coq_opam_version\" has failed (for the $RUNNER commit = $COQ_HASH_LONG)."
zulip_edit "Bench failed: could not install $package ($RUNNER)."
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/$package.$RUNNER.1.time" "$log_dir/$package.$RUNNER.$it.time"
cp "$log_dir/$package.$RUNNER.1.perf" "$log_dir/$package.$RUNNER.$it.perf"
done
done

}

# Create an OPAM-root to which we will install the NEW version of Coq.
Expand All @@ -467,14 +438,9 @@ 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"

# Packages which appear in the rendered table
# Deliberately don't include the "coqide-server" and "coq" packages
installable_coq_opam_packages="coq-core rocq-core"
installable_coq_opam_packages=""

echo "DEBUG: $render_results $log_dir $num_of_iterations 0 user_time_pdiff $installable_coq_opam_packages"
rendered_results="$($render_results "$log_dir" $num_of_iterations 0 user_time_pdiff $installable_coq_opam_packages)"
echo "${rendered_results}"
zulip_edit "Benching continues..."
zulip_edit "Opam setup, benching continues..."

format_vosize() {
old=$(stat -c%s $2)
Expand All @@ -484,33 +450,11 @@ format_vosize() {
echo "$1 $old $new $diff $diffpercent%"
}

# HTML for stdlib
# NB: unlike coq_makefile packages, stdlib produces foo.timing not foo.v.timing
new_base_path=$new_opam_root/ocaml-NEW/.opam-switch/build/rocq-core.dev/_build/default/theories/
old_base_path=$old_opam_root/ocaml-OLD/.opam-switch/build/rocq-core.dev/_build/default/theories/
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
if [ -e $old_base_path/${vo%%.vo}.timing ] && \
[ -e $new_base_path/${vo%%.vo}.timing ]; then
mkdir -p $working_dir/html/rocq-core/$(dirname $vo)/
# NB: sometimes randomly fails
$timelog2html $new_base_path/${vo%%o} \
$old_base_path/${vo%%.vo}.timing \
$new_base_path/${vo%%.vo}.timing > \
$working_dir/html/rocq-core/${vo%%o}.html ||
echo "Failed (code $?):" $timelog2html $new_base_path/${vo%%o} \
$old_base_path/${vo%%.vo}.timing \
$new_base_path/${vo%%.vo}.timing
fi
done

# --------------------------------------------------------------------------------
# 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})
sorted_coq_opam_packages=${coq_opam_packages}
echo "sorted_coq_opam_packages = ${sorted_coq_opam_packages}"

failed_packages=
Expand All @@ -521,9 +465,12 @@ export TIMING=1
export PROFILING=1
export COQ_PROFILE_COMPONENTS=command,parse_command,partac.perform

for coq_opam_package in $sorted_coq_opam_packages; do
for coq_opam_package in coq-core rocq-core $sorted_coq_opam_packages; do

export COQ_OPAM_PACKAGE=$coq_opam_package
if [ $coq_opam_package = coq-core ] || [ $coq_opam_package = rocq-core ] || [ $coq_opam_package = coq-stdlib ]; then
: not getting info from opam repo
else
if [ ! -z "$BENCH_DEBUG" ]; then
opam list
opam show $coq_opam_package || {
Expand All @@ -539,6 +486,7 @@ $coq_opam_package (unknown package)"
continue
}
fi
fi
echo "coq_opam_package = $coq_opam_package"

for RUNNER in NEW OLD; do
Expand All @@ -547,13 +495,33 @@ $coq_opam_package (unknown package)"

# 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)"
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 ] && ! [ -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
Expand Down

0 comments on commit 7aa65aa

Please sign in to comment.