Debian CI WIP

mit-plv · Aug 7, 2023 · 43ae18b · 43ae18b
1 parent 60efd19
commit 43ae18b
Show file tree

Hide file tree

Showing 2 changed files with 122 additions and 1 deletion.
diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
@@ -0,0 +1,120 @@
+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: bootstrap
+      run: |
+        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
+        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 ca-certificates 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)"
+        sudo mkdir -p "/chroot/$(pwd)"
+        sudo chown "$(id -u):$(id -g)" "/chroot/$(pwd)"
+        sudo mount --bind "$(pwd)" "/chroot/$(pwd)"
+
+    - name: host build params
+      run: |
+        "$(pwd)/etc/ci/describe-system-config.sh"
+    - name: chroot build params
+      run: |
+        sudo chroot /chroot setpriv --reuid "$(id -u)" --regid "$(id -g)" --init-groups \
+          "$(pwd)/etc/ci/describe-system-config.sh"
+    - name: make deps
+      run: |
+        sudo chroot /chroot setpriv --reuid "$(id -u)" --regid "$(id -g)" --init-groups \
+          "$(pwd)/etc/ci/github-actions-make.sh" -C "$(pwd)" -j2 deps
+    - name: all-except-generated
+      run: |
+        sudo chroot /chroot setpriv --reuid "$(id -u)" --regid "$(id -g)" --init-groups \
+          "$(pwd)/etc/ci/github-actions-make.sh" -C "$(pwd)" -j2 all-except-generated
+    - name: generated-files
+      run: |
+        sudo chroot /chroot setpriv --reuid "$(id -u)" --regid "$(id -g)" --init-groups \
+          "$(pwd)/etc/ci/github-actions-make.sh" -C "$(pwd)" -j2 generated-files
+      if: github.event_name == 'pull_request' || ${{ matrix.env.COQ_VERSION }} != 'master'
+    - run: tar -czvf generated-files.tgz fiat-*/
+      if: ${{ failure() }}
+    - name: upload generated files
+      uses: actions/upload-artifact@v3
+      with:
+        name: generated-files-${{ matrix.env.COQ_VERSION }}
+        path: generated-files.tgz
+      if: ${{ failure() }}
+    - name: upload OCaml files
+      uses: actions/upload-artifact@v3
+      with:
+        name: ExtractionOCaml-${{ matrix.env.COQ_VERSION }}
+        path: src/ExtractionOCaml
+      if: always ()
+    - name: standalone-haskell
+      run: |
+        sudo chroot /chroot setpriv --reuid "$(id -u)" --regid "$(id -g)" --init-groups \
+          "$(pwd)/etc/ci/github-actions-make.sh" -C "$(pwd)" -j1 standalone-haskell GHCFLAGS='+RTS -M6G -RTS'
+    - name: upload Haskell files
+      uses: actions/upload-artifact@v3
+      with:
+        name: ExtractionHaskell-${{ matrix.env.COQ_VERSION }}
+        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
+
+    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: Download a Build Artifact
+      uses: actions/download-artifact@v3
+      with:
+        name: "ExtractionOCaml-Ubuntu LTS"
+        path: src/ExtractionOCaml
+    - name: make binaries executable
+      run: chmod +x src/ExtractionOCaml/*
+    - name: make only-test-amd64-files
+      run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files SLOWEST_FIRST=1
+      env: 
+        ALLOW_DIFF: 1
diff --git a/etc/ci/github-actions-make.sh b/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=""