Trying out self-hosted runners

[andres-erbsen]

Do not merge, this branch runs only self-hosted runners as a test. I am hoping though that with the other changes here we could mix them by labeling our runners as ubuntu-latest (somewhat misleadingly). I started the two current runners using the following script:

#!/bin/bash -eux

# USAGE: 
# 1. get API token from  https://github.com/mit-plv/fiat-crypto/settings/actions/runners/new  or  https://docs.github.com/en/rest/reference/actions#create-a-registration-token-for-a-repository
# 2. edit --token below
# 3. https://horizon.csail.mit.edu/horizon/project/instances/ xl.2core ubuntu Post-Creation

su -s /bin/bash ubuntu -- -eux <<'EOF'
cd
mkdir actions-runner && cd actions-runner
curl -o actions-runner-linux-x64-2.283.1.tar.gz -L https://github.com/actions/runner/releases/download/v2.283.1/actions-runner-linux-x64-2.283.1.tar.gz
echo "aebaaf7c00f467584b921f432f9f9fb50abf06e1b6b226545fbcbdaa65ed3031  actions-runner-linux-x64-2.283.1.tar.gz" | shasum -a 256 -c
tar xzf ./actions-runner-linux-x64-2.283.1.tar.gz
./config.sh --unattended --labels ubuntu-upstream-latest --name "$(hostname)" --url https://github.com/mit-plv/fiat-crypto --token TODO_INSERT_TOKEN_HERE
./run.sh
EOF

I'm not sure whether this will work because github self-hosted runners do not have any of the isolation (and thus cleanup) functionality we've come to expect from public CI services. In particular, I'm curious to see what happens when the same runner gets assigned a job with a different coq version than before. But it might just work.

[andres-erbsen]

Indeed, the second run of the first runner got all the way to dpkg and then failed badly when trying to install two coq packages that included different files for the same path. @JasonGross you probably know more about debian/ubuntu packaging than me, do you think using virtual Conflicts,Provides,Replaces in many-coq-versions would make things work here? EDIT: pushing a change with this ci config should trigger a build on the same runners still.

[JasonGross]

Hmmm, I could try something like that. I'm not sure what the right way to do this is, though. The current files look like https://github.com/JasonGross/coq-debian-build-scripts/blob/master/reference-from-coq_8.14-8.5/debian/control (I think they get modified by sed in https://github.com/JasonGross/coq-debian-build-scripts/blob/a49243337eca02f0e1b9392b6158b1b55e79ac15/04-make-debian-from-reference.sh#L156-L160 )

[andres-erbsen]

Looking at URLs like https://launchpad.net/~jgross-h/+archive/ubuntu/many-coq-versions-ocaml-4-05/+sourcefiles/coq-8.13.1/8.13.1-1~focal~ppa161/coq-8.13.1_8.13.1-1~focal~ppa161.debian.tar.xz makes me think there is some preprocessing step (maybe the same sed script that you mentioned) that appends the coq version to its name (after which the package version gets appended, leaving us with two version numbers). In that case, my understanding of the documentation I linked is that adding Conflicts: coq Provides: coq Replaces: coq to package coq-8.13.1 and other version-specific packages would do the trick. And I guess the same trick would have to be repeated for other package families that have package names generated based on version? But reading https://launchpad.net/%7Ejgross-h/+archive/ubuntu/many-coq-versions-ocaml-4-05/+packages?batch=75&memo=75&start=75 makes me think there might not be any that we rely on.

[andres-erbsen]

Oh, and the CI script also uses different repositories -- should we expect additional issues when multiple of these are added at once?

[JasonGross]

Regarding multiple ppas, it depends how good debian's version resolution is. The issue is that the underlying OCaml versions are incompatible, and apt seems to not like installing older versions of packages when newer versions are available (hence why I rename all the Coq packages to include version numbers in the name). So it may be the case that it's very sad anytime it needs to downgrade the version of OCaml

[JasonGross]

I think if we're going to use self-hosted runners without wiping state, it's probably better to just pin a bunch of Coq versions with opam and use opam switch to pick the version. The only reason I don't do this on CI is that I don't want the overhead of compiling both Coq and OCaml on every run, but probably even if we start doing this on the main ci the marginal difference is negligible

[andres-erbsen]

I don't really have an opinion other than having our CI scripts runnable at github-hosted runners (at least if we use github CI at all).