diff options
Diffstat (limited to 'dev/bench')
| -rw-r--r-- | dev/bench/gitlab-bench.yml | 4 | ||||
| -rwxr-xr-x | dev/bench/gitlab.sh | 14 |
2 files changed, 8 insertions, 10 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 7796ae3b01..2ce3cb77be 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-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) @@ -287,8 +287,8 @@ create_opam() { /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 1>&3 \ - 4>$log_dir/coq.$RUNNER.opam_install.1.stderr 2>&4 || \ + 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" @@ -363,8 +363,8 @@ for coq_opam_package in $sorted_coq_opam_packages; do opam config set-global jobs $number_of_processors opam install $coq_opam_package -v -b -j$number_of_processors --deps-only -y \ - 3>$log_dir/$coq_opam_package.$RUNNER.opam_install.deps_only.stdout 1>&3 \ - 4>$log_dir/$coq_opam_package.$RUNNER.opam_install.deps_only.stderr 2>&4 || continue 2 + 3>$log_dir/$coq_opam_package.$RUNNER.opam_install.deps_only.stdout.log 1>&3 \ + 4>$log_dir/$coq_opam_package.$RUNNER.opam_install.deps_only.stderr.log 2>&4 || continue 2 opam config set-global jobs 1 @@ -375,8 +375,8 @@ for coq_opam_package in $sorted_coq_opam_packages; do /usr/bin/time -o "$log_dir/$coq_opam_package.$RUNNER.$iteration.time" --format="%U %M %F" \ perf stat -e instructions:u,cycles:u -o "$log_dir/$coq_opam_package.$RUNNER.$iteration.perf" \ opam install -v -b -j1 $coq_opam_package \ - 3>$log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.stdout 1>&3 \ - 4>$log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.stderr 2>&4 || \ + 3>$log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.stdout.log 1>&3 \ + 4>$log_dir/$coq_opam_package.$RUNNER.opam_install.$iteration.stderr.log 2>&4 || \ _RES=$? if [ $_RES = 0 ]; then |