Skip to content

Commit

Permalink
Bench: only show packages which took at least 1s in render_results table
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Jan 9, 2025
1 parent 8eacf86 commit 90bf0cb
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 5 deletions.
8 changes: 4 additions & 4 deletions dev/bench/bench.sh
Original file line number Diff line number Diff line change
Expand Up @@ -611,8 +611,8 @@ $coq_opam_package (in $RUNNER)"
:
else

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 "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}" ""
Expand Down Expand Up @@ -719,8 +719,8 @@ if [ -z "$installable_coq_opam_packages" ]; then
exit 1
fi

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 "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

Expand Down
2 changes: 1 addition & 1 deletion dev/bench/render_results.ml
Original file line number Diff line number Diff line change
Expand Up @@ -231,7 +231,7 @@ coq_opam_packages

|> CList.filter
(fun (_, new_t, old_t, _) ->
minimal_user_time <= new_t.user_time && minimal_user_time <= old_t.user_time)
minimal_user_time <= new_t.user_time || minimal_user_time <= old_t.user_time)

(* Below we take the measurements and format them to stdout. *)

Expand Down

0 comments on commit 90bf0cb

Please sign in to comment.