diff options
Diffstat (limited to 'dev/bench')
| -rw-r--r-- | dev/bench/gitlab-bench.yml | 4 | ||||
| -rwxr-xr-x | dev/bench/gitlab.sh | 42 |
2 files changed, 23 insertions, 23 deletions
diff --git a/dev/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml index 25545cf565..69136ee773 100644 --- a/dev/bench/gitlab-bench.yml +++ b/dev/bench/gitlab-bench.yml @@ -4,9 +4,7 @@ bench: when: manual before_script: - printenv -0 | sort -z | tr '\0' '\n' - script: - - . ~/.opam/opam-init/init.sh - - ./dev/bench/gitlab.sh + script: dev/bench/gitlab.sh tags: - timing variables: diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index b616371ef8..49c8099e8b 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -52,7 +52,7 @@ check_variable "CI_JOB_URL" : "${new_coq_opam_archive_git_branch:=master}" : "${old_coq_opam_archive_git_branch:=master}" : "${num_of_iterations:=1}" -: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-perennial}" +: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast coq-perennial coq-vst}" new_coq_commit=$(git rev-parse HEAD^2) old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit) @@ -283,25 +283,27 @@ create_opam() { echo "$1_coq_commit_long = $COQ_HASH_LONG" - _RES=0 - /usr/bin/time -o "$log_dir/coq.$RUNNER.1.time" --format="%U %M %F" \ - perf stat -e instructions:u,cycles:u -o "$log_dir/coq.$RUNNER.1.perf" \ - opam pin add -y -b -j "$number_of_processors" --kind=path coq.dev . \ - 3>$log_dir/coq.$RUNNER.opam_install.1.stdout.log 1>&3 \ - 4>$log_dir/coq.$RUNNER.opam_install.1.stderr.log 2>&4 || \ - _RES=$? - if [ $_RES = 0 ]; then - echo "Coq ($RUNNER) installed successfully" - else - echo "ERROR: \"opam install coq.$coq_opam_version\" has failed (for the $RUNNER commit = $COQ_HASH_LONG)." - exit 1 - fi + for package in coq-core coq-stdlib coq; do + _RES=0 + /usr/bin/time -o "$log_dir/$package.$RUNNER.1.time" --format="%U %M %F" \ + perf stat -e instructions:u,cycles:u -o "$log_dir/$package.$RUNNER.1.perf" \ + opam pin add -y -b -j "$number_of_processors" --kind=path $package.dev . \ + 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)." + 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/coq.$RUNNER.1.time" "$log_dir/coq.$RUNNER.$it.time" - cp "$log_dir/coq.$RUNNER.1.perf" "$log_dir/coq.$RUNNER.$it.perf" + # 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 } @@ -327,7 +329,7 @@ fi export TIMING=1 # The following variable will be set in the following cycle: -installable_coq_opam_packages=coq +installable_coq_opam_packages="coq-core coq-stdlib coq" for coq_opam_package in $sorted_coq_opam_packages; do |