Benchmarking

Benchmarking

For changes based on master: Make a PR and have someone with the rights on gitlab to start the "bench" job.

To compare arbitrary Coq commits: currently impractical.

The job itself produces a looooong log. At its end you should see the results rendered as a table:

Each line shows the measurement for a single OPAM package.

Each measured/computed quantity has its own column.

The git commits, that were considered are stated explicitely below the table as NEW and OLD.

E.g., in the table shown above, we see that the compilation of coq-geocoq

• originally took 2394.71 seconds
• now it takes 2215.65
• which means that it decreased by cca. 7%

The lines of the table are ordered wrt. improvements in the overall compilation times.

Benchmarking (with "overlays")

The following two environment variables

• new_coq_opam_archive_git_uri
• new_coq_opam_archive_git_branch

enable us to define "overlays", i.e. tweak the definitions of OPAM packages to be used with new_coq_commit.

They can be set when starting the bench job.

Choosing opam package

The variable coq_opam_packages can be set to a list of a restrict list of opam packages to bench.

Setting up new machines

Replace TOKEN by the one from https://gitlab.com/coq/coq/-/settings/ci_cd see https://docs.gitlab.com/runner/register/#linux

# opam, time and perf for the bench
# perl and gmp for zarith
# lua for timelog2html (NB it wants 5.1 specifically at time of writing this, see shebang)
# m4, autoconf and automake for hott and others
# jq for fiat-crypto
sudo apt-get install -y curl opam time linux-perf perl libgmp-dev lua5.1 m4 automake autoconf jq

sudo bash -c 'echo -1 > /proc/sys/kernel/perf_event_paranoid'
sudo bash -c "echo 'kernel.perf_event_paranoid = -1' > /etc/sysctl.d/00-coq-bench.conf"

curl -L "https://packages.gitlab.com/install/repositories/runner/gitlab-runner/script.deb.sh" | sudo bash

sudo env GITLAB_RUNNER_DISABLE_SKEL=true apt-get install -y gitlab-runner

sudo gitlab-runner register \
     --non-interactive \
     --url 'https://gitlab.com' \
     --registration-token TOKEN \
     --name "$(hostname -f)" \
     --tag-list timing \
     --executor shell

sudo gitlab-runner start