Update installation information for gitlab runners.

misc/ci-bench.sh

 #!/bin/bash
 
-# runner:
-# apt-get install curl opam automake libgmp-dev zlib1g-dev
+# Runner installation
+# -------------------
+# apt-get install curl
 # curl -L https://packages.gitlab.com/install/repositories/runner/gitlab-runner/script.deb.sh | bash
-# apt-get install gitlab-runner
+# curl -fsSL https://download.docker.com/linux/debian/gpg | apt-key add -
+# apt-key fingerprint 0EBFCD88
+# echo "deb https://download.docker.com/linux/debian stretch stable" >> /etc/apt/sources.list
+# apt-get update
+# apt-get install gitlab-runner docker-ce
 # gitlab-runner register
 #   https://gitlab.inria.fr/
 #   shell
-# su gitlab-runner
-# cd
-# opam init
-# opam install menhir alt-ergo
+# usermod -aG docker gitlab-runner
 
 set -e
 eval `opam config env`

[Raphaël Rieu-Helft]

Is that not still needed?

[Guillaume Melquiond]

Which part? The installation of opam, menhir, and alt-ergo for the gitlab-runner user is needed for the branches that are still using the old approach, but not for master (since the packages get installed via docker).

[Raphaël Rieu-Helft]

I meant only the su gitlab-runner line. With these instructions, we are adding the user to the docker group, but not logging in as gitlab-runner, unless I am missing something?

[Guillaume Melquiond]

Logging as gitlab-runner was only needed to install opam and friends. Unless I forgot an item, we no longer have any action for which we need to impersonate gitlab-runner.

[Raphaël Rieu-Helft]

Correct, I misunderstood.