Debian CI

.github/workflows/coq-debian.yml

@@ -0,0 +1,105 @@
+name: CI (Coq, Debian)
+
+on:
+  push:
+    branches: [ master , sp2019latest ]
+  pull_request:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 0 1 * *'
+
+jobs:
+  build:
+
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+        - env: { DEBIAN: "sid" }
+        - env: { DEBIAN: "bookworm" }
+
+    runs-on: 'ubuntu-22.04'
+    env: ${{ matrix.env }}
+    name: ${{ matrix.env.DEBIAN }}
+
+    concurrency:
+      group: ${{ github.workflow }}-${{ matrix.env.DEBIAN }}-${{ github.head_ref || github.run_id }}
+      cancel-in-progress: true
+
+    steps:
+    - uses: actions/checkout@v3
+      with:
+        submodules: recursive
+    - name: setup Debian chroot
+      run: etc/ci/setup-debian-chroot.sh "$DEBIAN"
+    - name: host build params
+      run: etc/ci/describe-system-config.sh
+    - name: chroot build params
+      shell: in-debian-chroot.sh {0}
+      run: etc/ci/describe-system-config.sh
+    - name: make deps
+      shell: in-debian-chroot.sh {0}
+      run: etc/ci/github-actions-make.sh -j2 deps
+    - name: all-except-generated
+      shell: in-debian-chroot.sh {0}
+      run: etc/ci/github-actions-make.sh -j2 all-except-generated
+    - name: generated-files
+      shell: in-debian-chroot.sh {0}
+      run: etc/ci/github-actions-make.sh -j2 generated-files
+    - run: tar -czvf generated-files.tgz fiat-*/
+      if: ${{ failure() }}
+    - name: upload generated files
+      uses: actions/upload-artifact@v3
+      with:
+        name: generated-files-${{ matrix.env.DEBIAN }}
+        path: generated-files.tgz
+      if: ${{ failure() }}
+    - name: upload OCaml files
+      uses: actions/upload-artifact@v3
+      with:
+        name: ExtractionOCaml-${{ matrix.env.DEBIAN }}
+        path: src/ExtractionOCaml
+      if: always ()
+    - name: standalone-haskell
+      shell: in-debian-chroot.sh {0}
+      run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M6G -RTS'
+    - name: upload Haskell files
+      uses: actions/upload-artifact@v3
+      with:
+        name: ExtractionHaskell-${{ matrix.env.DEBIAN }}
+        path: src/ExtractionHaskell
+      if: always ()
+    - name: display timing info
+      run: cat time-of-build-pretty.log
+    - name: display per-line timing info
+      run: etc/ci/github-actions-display-per-line-timing.sh
+
+  test-amd64:
+
+    runs-on: ubuntu-latest
+    env: { DEBIAN: "sid" }
+
+    concurrency:
+      group: ${{ github.workflow }}-test-amd64-${{ github.head_ref || github.run_id }}
+      cancel-in-progress: true
+    needs: build
+
+    steps:
+    - name: checkout repo
+      uses: actions/checkout@v3
+      with:
+        submodules: recursive
+    - name: setup Debian chroot
+      run: etc/ci/setup-debian-chroot.sh "$DEBIAN"
+    - name: Download a Build Artifact
+      uses: actions/download-artifact@v3
+      with:
+        name: ExtractionOCaml-sid
+        path: src/ExtractionOCaml
+    - name: make binaries executable
+      run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x
+    - name: make only-test-amd64-files
+      shell: in-debian-chroot.sh {0}
+      run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files SLOWEST_FIRST=1
+      env: 
+        ALLOW_DIFF: 1

etc/ci/describe-system-config.sh

@@ -29,3 +29,4 @@ group coqc --config
 group coqc --version
 group "true | coqtop"
 group etc/machine.sh
+group "echo PATH=$PATH"

etc/ci/github-actions-make.sh

@@ -1,6 +1,7 @@
 #!/usr/bin/env bash
 
 set -x
+cd "$(dirname "$0")/../.." || exit 7
 
 if [ ! -z "${TOUCH}" ]; then
     make -j2 -t ${TOUCH} || exit $?
@@ -20,7 +21,7 @@ if [ "$1" == "--warnings" ]; then
     shift
 fi
 if [ ! -z "${reportify}" ]; then
-    reportify="COQC='$(pwd)/etc/coq-scripts/github/reportify-coq.sh'${reportify} ${COQBIN}coqc"
+    reportify="COQC=etc/coq-scripts/github/reportify-coq.sh${reportify} ${COQBIN}coqc"
 fi
 
 make_one_time_file_real=""

etc/ci/in-debian-chroot.sh

@@ -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)" "$@"

etc/ci/setup-debian-chroot.sh

@@ -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"