Skip to content

Commit

Permalink
CI: use --real when generating per file timing tables
Browse files Browse the repository at this point in the history
The default of using user times seems to under report child process times.
  • Loading branch information
SkySkimmer committed Nov 22, 2023
1 parent f74ae51 commit c768e3d
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
4 changes: 2 additions & 2 deletions dev/bench/bench.sh
Original file line number Diff line number Diff line change
Expand Up @@ -604,7 +604,7 @@ $skipped_packages"
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 \
"$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"
Expand Down Expand Up @@ -654,7 +654,7 @@ du -ha "$working_dir" > "$working_dir/files.listing"
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 \
"$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"
Expand Down
2 changes: 1 addition & 1 deletion dev/ci/ci-wrapper.sh
Original file line number Diff line number Diff line change
Expand Up @@ -17,5 +17,5 @@ export TIMED=1
bash "${DIR}/${CI_SCRIPT}" 2>&1 | tee "$CI_NAME.log"
code=$?
echo 'Aggregating timing log...'
python ./tools/make-one-time-file.py "$CI_NAME.log"
python ./tools/make-one-time-file.py --real "$CI_NAME.log"
exit $code

0 comments on commit c768e3d

Please sign in to comment.