Skip to content

Commit

Permalink
use profile files for timelog2html in bench
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Jan 9, 2025
1 parent 0751e47 commit 4e5b152
Showing 1 changed file with 53 additions and 16 deletions.
69 changes: 53 additions & 16 deletions dev/bench/bench.sh
Original file line number Diff line number Diff line change
Expand Up @@ -137,9 +137,6 @@ number_of_processors=$(cat /proc/cpuinfo | grep '^processor *' | wc -l)

program_name="$0"
program_path=$(readlink -f "${program_name%/*}")
render_results="dune exec --no-print-directory --root $program_path/../.. -- dev/bench/render_results.exe"
render_line_results="dune exec --no-print-directory --root $program_path/../.. -- dev/bench/render_line_results.exe"
timelog2html="dune exec --no-print-directory --root $program_path/../.. -- rocq timelog2html"

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

Expand Down Expand Up @@ -344,7 +341,7 @@ git clone -q --depth 1 -b "$old_coq_opam_archive_git_branch" "$old_coq_opam_arch
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 yojson"
initial_opam_packages="num zarith ocamlfind dune yojson"

# Create an opam root and install Coq
# $1 = root_name {ex: NEW / OLD}
Expand Down Expand Up @@ -433,6 +430,16 @@ 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)

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

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")
rocq_exe=$(readlink -f "$program_path/../../_build/default/topbin/rocq.exe")
timelog2html="$rocq_exe timelog2html"

# Create an OPAM-root to which we will install the OLD version of Coq.
create_opam "OLD" "$old_ocaml_version" "$old_coq_commit" "$old_coq_version" \
"$old_coq_opam_archive_dir" "$old_opam_override_urls" "$old_ocaml_flambda"
Expand Down Expand Up @@ -462,7 +469,7 @@ export PROFILING=1
export COQ_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 coq-stdlib coqide-server coq'
core_packages='rocq-runtime coq-core rocq-core rocq-stdlib coq-stdlib coqide-server rocq coq'

for coq_opam_package in $core_packages $coq_opam_packages; do

Expand Down Expand Up @@ -647,17 +654,47 @@ $skipped_packages"
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%%o}.timing ] && \
[ -e $new_base_path/${vo%%o}.timing ]; then
mkdir -p $working_dir/html/$coq_opam_package/$(dirname $vo)/
# NB: sometimes randomly fails
$timelog2html $new_base_path/${vo%%o} \
$old_base_path/${vo%%o}.timing \
$new_base_path/${vo%%o}.timing > \
$working_dir/html/$coq_opam_package/${vo%%o}.html ||
echo "Failed (code $?):" $timelog2html $new_base_path/${vo%%o} \
$old_base_path/${vo%%o}.timing \
$new_base_path/${vo%%o}.timing

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

if [ "$old_data" ] && [ "$new_data" ]; then
# timelog2html doesn't know how to uncompress
if [ "$old_compressed" ]; then
gunzip --keep "$old_data"
fi
if [ "$new_compressed" ]; then
gunzip --keep "$new_data"
fi
mkdir -p "$working_dir/html/$coq_opam_package/$(dirname "$vo")/"
$timelog2html \
"$new_base_path/${vo%%o}" \
"${old_data%.gz}" \
"${new_data%.gz}" \
> "$working_dir/html/$coq_opam_package/${vo%%o}.html" ||
echo "Failed (code $?): timelog2html for $vo on $old_data $new_data"
if [ "$old_compressed" ]; then
rm "${old_data%.gz}"
fi
if [ "$new_compressed" ]; then
rm "${new_data%.gz}"
fi
fi
done
done
Expand Down

0 comments on commit 4e5b152

Please sign in to comment.