-
Notifications
You must be signed in to change notification settings - Fork 147
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
c65632e
commit 8d12f39
Showing
4 changed files
with
47 additions
and
48 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -29,3 +29,4 @@ group coqc --config | |
group coqc --version | ||
group "true | coqtop" | ||
group etc/machine.sh | ||
group "echo PATH=$PATH" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
#!/bin/sh | ||
set -e -u -x | ||
|
||
# This script is intended to be called from github hosted runners only. | ||
|
||
exec sudo chroot /chroot setpriv --reuid "$(id -u)" --regid "$(id -g)" --init-groups \ | ||
/bin/sh -e -u -x -c 'cd "$1"; shift; exec sh -e -u -x "$@"' -- "$(pwd)" "$@" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
#/bin/sh | ||
set -e -u -x | ||
debian="$1" | ||
|
||
# This script is intended to be called from github hosted runners only. | ||
# It does not clean up after itself. | ||
|
||
sudo mkdir /chroot | ||
sudo apt-get -q -y -o Acquire::Retries=30 update | ||
sudo apt-get -q -y -o Acquire::Retries=30 install debootstrap | ||
sudo debootstrap --variant=minbase "$debian" /chroot http://debian-archive.trafficmanager.net/debian/ || ( cat /tmp/tmp.*/debootstrap/debootstrap.log ; exit 1 ) | ||
sudo mount proc /chroot/proc -t proc | ||
sudo mount sysfs /chroot/sys -t sysfs | ||
sudo chroot /chroot apt-get -q -y -o Acquire::Retries=30 install sudo git make time jq python3 python-is-python3 ocaml coq libcoq-core-ocaml-dev libfindlib-ocaml-dev ocaml-findlib cabal-install | ||
sudo chroot /chroot groupadd -g "$(id -g)" "$(id -g -n)" | ||
sudo chroot /chroot useradd -g "$(id -g)" -u "$(id -u)" "$(id -u -n)" | ||
printf "%s ALL=(ALL) NOPASSWD: ALL\n" "$(id -u -n)" | sudo tee /chroot/etc/sudoers.d/root | ||
sudo mkdir -p "/chroot/$HOME" | ||
sudo chown "$(id -u):$(id -g)" "/chroot/$HOME" | ||
sudo mount --bind "$HOME" "/chroot/$HOME" | ||
|
||
( cd "$(dirname "$0")" && pwd ) | tee -a "$GITHUB_PATH" |