diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml new file mode 100644 index 00000000000..c50d3a129ac --- /dev/null +++ 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 index 27419804e7e..c5d5b2dd6ed 100755 --- 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=""