diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml new file mode 100644 index 00000000000..dd582929699 --- /dev/null +++ b/.github/workflows/coq-debian.yml @@ -0,0 +1,119 @@ +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 apt-get -q -y -o Acquire::Retries=30 update + sudo apt-get -q -y -o Acquire::Retries=30 install debootstrap + df -h + root="$(mktemp -d)" + sudo debootstrap --include=ca-certificates,git,make,python3,coq,libcoq-core-ocaml-dev,jq "$DEBIAN" "$root" http://debian-archive.trafficmanager.net/debian/ || cat /tmp/tmp.*/debootstrap/debootstrap.log + sudo mount proc "$root"/proc -t proc + sudo mount sysfs "$root"/sys -t sysfs + sudo mount --bind "$PWD" "$root/$PWD" + + sudo chroot "$root" groupadd -g "$(id -g)" "$(id -u -n)" + sudo chroot "$root" useradd -u "$(id -u)" -g "$(id -g)" "$(id -u -n)" + + - name: install Haskell + run: | + sudo chroot "$root" apt-get -q -y -o Acquire::Retries=30 install cabal-install + - name: echo build params + run: | + sudo chroot "$root" setpriv --reuid "$(id -u)" --regid "$(id -g)" --init-groups \ + etc/ci/describe-system-config.sh + - name: make deps + run: | + sudo chroot "$root" setpriv --reuid "$(id -u)" --regid "$(id -g)" --init-groups \ + etc/ci/github-actions-make.sh -C "$PWD" -j2 deps + - name: all-except-generated + run: | + sudo chroot "$root" setpriv --reuid "$(id -u)" --regid "$(id -g)" --init-groups \ + etc/ci/github-actions-make.sh -C "$PWD" -j2 all-except-generated + - name: generated-files + run: | + sudo chroot "$root" setpriv --reuid "$(id -u)" --regid "$(id -g)" --init-groups \ + 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 "$root" setpriv --reuid "$(id -u)" --regid "$(id -g)" --init-groups \ + 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