Self-hosted Github runner

Stream: general

[Jannis Limperg]

Breaking this out of the speed-up project returns thread.

It seems like it might be beneficial to have a custom Github runner which could build mathlib much faster than Github's runners. I'm currently running some experiments in this direction with initial funding graciously provided by @Jalex Stark.

To determine what sort of build server we'd want, a key factor is how mathlib scales with additional cores. I'm currently running benchmarks on a dedicated server with 8 cores and a virtual server with 16 cores. @Scott Morrison, could you perhaps run the same benchmark on your machine? Just so that we have a bit more data.

Here's the benchmark script:

#!/bin/bash

function die() {
  echo $1
  echo "Usage: mathlib-bench <mathlib-dir> <n1> [n2 ...]"
  exit 1
}

test -n "$1" || die "Mathlib directory not specified."
mathlib_dir="$1"
shift

test -n "$1" || die "Thread count not specified"

echo "===== Cloning mathlib repo in '$mathlib_dir'"
git clone https://github.com/leanprover-community/mathlib "$mathlib_dir" && \
  pushd "$mathlib_dir" && \
  git checkout d0beb496140b5506530e18033591c711030546ad && \
  popd

test "$?" -eq 0 || die "Unable to clone mathlib."

echo "===== Installing Lean toolchain"
pushd "$mathlib_dir" && \
  leanpkg configure && \
  popd

test "$?" -eq 0 || die "Unable to install Lean toolchain."

while test -n "$1"; do
  test "$1" -gt 0 || die "Not a positive number: $1."
  n_threads="$1"

  echo "===== Building mathlib with $n_threads threads" && \
    find "$mathlib_dir" -name '*.olean' -delete && \
    pushd "$mathlib_dir" && \
    command time leanpkg build -- --threads="$n_threads" --memory=16000 && \
    popd

  test $? -eq 0 || die "Error while building mathlib."
done

Usage: mathlib-bench <dir> <n1> ... <nm> where dir is the directory where mathlib will be checked out (must be empty or nonexistent) and the ni are thread counts. I'm using mathlib-bench <dir> 1 2 4 6 8 10 12 14 16.

[Jannis Limperg]

Also, if anyone knows an organisation that would give us build servers for free/cheap, I'm all ears.

[Ryan Lahfa]

Jannis Limperg said:

Also, if anyone knows an organisation that would give us build servers for free/cheap, I'm all ears.

We have nothing to lose to try:
— Nix/NixOS community
— Packet.com
— University

Also, thanks for the benchmark script, I'll be able to play around with Packet's EPYC now :-)

[Scott Morrison]

(the same machine is at the moment running two single-threaded builds of old commits of mathlib, which will presumably interfere for the higher core numbers...)

[Scott Morrison]

Running!

[Jannis Limperg]

Thanks Scott and Ryan! Those numbers will be very interesting.

[Johan Commelin]

And thanks Jalex and Jannis!

[Jannis Limperg]

sigh The security issues of self-hosted Github runners are much worse than I thought. Essentially: Anyone can make a PR that changes the GH actions workflow file, then this new file is run (because it can say, 'run me on a self-hosted runner when a PR is created'), and the runner does no sandboxing whatsoever. I was able to create a PR (as a random user with no affiliation with the repo) that changed the workflow file to cat /etc/passwd and this was executed and displayed without a hitch. Whoever thought this was a remotely sensible design deserves to be slapped.

What this means for the project is that I need to figure out whether I can sandbox the runner myself in a VM or something. Fun times...

[Johan Commelin]

That's quite ridiculous indeed.

[Johan Commelin]

And running it inside some docker sandbox probably hinders the performance

[Johan Commelin]

How about a qemu bare metal VM?

[Johan Commelin]

But it comes with extra maintenance ~~> headaches

[Reid Barton]

All solutions for CI involve security issues like this to various extents, as well as the reverse issue: how do I know I can trust the binaries produced by your server?

[Reid Barton]

How about just not building PRs?

[Yury G. Kudryashov]

As far as I understand, a PR can say " let's build PRs"

[Yury G. Kudryashov]

Am I right?

[Reid Barton]

oh, I don't know about this github self-hosted thing in particular

[Yury G. Kudryashov]

Does it run under root user account (otherwise it shouldn't have access to /etc/passwd)?

[Reid Barton]

I agree if it can't even be configured to only build commits to master, that's an extra level of dumb.

[Rob Lewis]

I think the solution is going to depend on exactly what you want to do with this. Is this supposed to be a replacement for the CI running on Actions right now? Or is it separate, just for benchmarking?

[Rob Lewis]

If it's just for benchmarking, it doesn't have to be tied to the mathlib repo at all.

[Jannis Limperg]

Yury G. Kudryashov said:

As far as I understand, a PR can say " let's build PRs"

Yes, that's one part of the problem. The workflow itself defines when it is run, and there are no repository-wide configuration options to restrict this. I thought it might be possible to disable Actions for PRs from forks, but no such luck.

Yury G. Kudryashov said:

Does it run under root user account (otherwise it shouldn't have access to /etc/passwd)?

No, you can run it as an unprivileged user. (/etc/passwd is world-readable by default, at least on this installation.) But then it still has access to any world-readable files as well as the network, which is way too much attack surface.

Rob Lewis said:

I think the solution is going to depend on exactly what you want to do with this. Is this supposed to be a replacement for the CI running on Actions right now? Or is it separate, just for benchmarking?

No, I want this to be a faster replacement for the default Github Actions runners. The idea is to get mathlib compile times to a more tolerable level for all contributors.

Johan Commelin said:

How about a qemu bare metal VM?

The problem is that you really want to spin up a new VM/container for every job, to make sure that they can't leave anything behind. This would have to be done by the GH runner, which, as far as I can tell, can't do it.

[Yury G. Kudryashov]

(/etc/passwd is world-readable by default
I should read more carefully: it's "just" /etc/passwd, not /etc/shadow

[Gabriel Ebner]

Jannis Limperg said:

No, I want this to be a faster replacement for the default Github Actions runners. The idea is to get mathlib compile times to a more tolerable level for all contributors.

Have you done the calculations on this? How many machines would we need to build all PR commits? (Say one build takes 20 minutes, then we can only do 72 commits per day. This seems potentially low.)

[Yury G. Kudryashov]

An alternative approach: make github just wget some URL on the server. Then a script can checkout the specified commit, compile it using a hardcoded script, publish oleans, and post a status update.

[Gabriel Ebner]

Please be aware that you can execute arbitrary commands when compiling Lean code. (See io.cmd.)

[Reid Barton]

and, for example, you do not want that arbitrary code to have access to your cloud storage credentials

[Rob Lewis]

With that setup, we can at least restrict to people we've offered write access to mathlib branches. External PRs can't access GH secrets, so you just need the script to be called with a stored passphrase.

[Johan Commelin]

@Jannis Limperg What's wrong with the current Github actions + leanproject setup?

[Rob Lewis]

But, like Gabriel, I'm skeptical about the scalability here. Github gives us a crazy amount of resources for free, even if they aren't blazing fast.

[Jannis Limperg]

Gabriel Ebner said:

Have you done the calculations on this? How many machines would we need to build all PR commits? (Say one build takes 20 minutes, then we can only do 72 commits per day. This seems potentially low.)

No, I'm waiting for the benchmark results to see what the numbers are like. I'm also not sure that they're going to be good enough for this whole thing to be worth it. However, on my machine, compilation with 4 threads already takes under 1h (around half the time GH actions currently needs), so I could run 2 jobs in parallel.

Johan Commelin said:

Jannis Limperg What's wrong with the current Github actions + leanproject setup?

That it takes 2h until you know whether your commit broke anything (and 3h for linting etc.). I was under the impression that people were unhappy with this and would be happier if it took significantly less long. However, if there's no demand for this project, I'll gladly drop it; the compile times don't bother me personally much (because my machine will likely remain faster than CI).

[Jannis Limperg]

@Scott Morrison @Ryan Lahfa The benchmark script was missing a shift, so it'll run the 1-thread benchmark forever. Sorry! (Why is there no facepalm emoji?)

Corrected script:

#!/bin/bash

function die() {
  echo $1
  echo "Usage: mathlib-bench <mathlib-dir> <n1> [n2 ...]"
  exit 1
}

test -n "$1" || die "Mathlib directory not specified."
mathlib_dir="$1"
shift

test -n "$1" || die "Thread count not specified"

echo "===== Cloning mathlib repo in '$mathlib_dir'"
git clone https://github.com/leanprover-community/mathlib "$mathlib_dir" && \
  pushd "$mathlib_dir" && \
  git checkout d0beb496140b5506530e18033591c711030546ad && \
  popd

test "$?" -eq 0 || die "Unable to clone mathlib."

echo "===== Installing Lean toolchain"
pushd "$mathlib_dir" && \
  leanpkg configure && \
  popd

test "$?" -eq 0 || die "Unable to install Lean toolchain."

while test -n "$1"; do
  test "$1" -gt 0 || die "Not a positive number: $1."
  n_threads="$1"

  echo "===== Building mathlib with $n_threads threads" && \
    find "$mathlib_dir" -name '*.olean' -delete && \
    pushd "$mathlib_dir" && \
    command time leanpkg build -- --threads="$n_threads" --memory=16000 && \
    popd

  test $? -eq 0 || die "Error while building mathlib."
  shift
done

[Johan Commelin]

@Jannis Limperg It's :face palm:. I've needed it a lot.

[Jannis Limperg]

What's the correct reaction when you're too dumb to find an emoji? :face_palm:

[Ryan Lahfa]

Jannis Limperg said:

sigh The security issues of self-hosted Github runners are much worse than I thought. Essentially: Anyone can make a PR that changes the GH actions workflow file, then this new file is run (because it can say, 'run me on a self-hosted runner when a PR is created'), and the runner does no sandboxing whatsoever. I was able to create a PR (as a random user with no affiliation with the repo) that changed the workflow file to cat /etc/passwd and this was executed and displayed without a hitch. Whoever thought this was a remotely sensible design deserves to be slapped.

What this means for the project is that I need to figure out whether I can sandbox the runner myself in a VM or something. Fun times...

That's why I think we should go for a Hydra (Nix/NixOS) model

[Ryan Lahfa]

The GH Actions are cool for simple stuff, beyond that, it's becoming annoyingly difficult to do it

[Ryan Lahfa]

Johan Commelin said:

Jannis Limperg What's wrong with the current Github actions + leanproject setup?

That it takes 2h until you know whether your commit broke anything (and 3h for linting etc.). I was under the impression that people were unhappy with this and would be happier if it took significantly less long. However, if there's no demand for this project, I'll gladly drop it; the compile times don't bother me personally much (because my machine will likely remain faster than CI).

In addition, if it takes 2 hours now, it might slowly getting longer and longer.
Faster feedback is nice, but also makes it future-proof.

[Johan Commelin]

I see. But maybe we can first focus on detailed and reliable profiling. So that we better understand where the slow bits of code are?

[Johan Commelin]

Still, of course I would love "instant CI"

[Ryan Lahfa]

Johan Commelin said:

I see. But maybe we can first focus on detailed and reliable profiling. So that we better understand where the slow bits of code are?

Agreed, I'm not jumping yet on the running stuff yet, I just want to setup simple experiments

[Ryan Lahfa]

Ideally, reproducible experiments would be arguably nice

[Scott Morrison]

I'm running the updated benchmark script.