[sp2019latest] User docker for master test (#1696)

* User docker for master test * Comment out unused gcc * Split up docker action
mit-plv · Nov 1, 2023 · 77a2f7d · 77a2f7d
1 parent 8c5424c
commit 77a2f7d
Show file tree

Hide file tree

Showing 4 changed files with 176 additions and 3 deletions.
diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml
@@ -15,7 +15,6 @@ jobs:
       fail-fast: false
       matrix:
         env:
-        - { COQ_VERSION: "master", COQ_PACKAGE: "coq"       , PPA: "ppa:jgross-h/coq-master-daily"            , SKIP_DISPLAY_TEST: "1", CC: "gcc", ALLOW_DIFF: ""  }
         - { COQ_VERSION: "8.17.1", COQ_PACKAGE: "coq-8.17.1", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11", SKIP_DISPLAY_TEST: "1", CC: "gcc", ALLOW_DIFF: ""  }
         - { COQ_VERSION: "8.16.1", COQ_PACKAGE: "coq-8.16.1", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11", SKIP_DISPLAY_TEST: "1", CC: "gcc", ALLOW_DIFF: ""  }
 
@@ -46,8 +45,8 @@ jobs:
         coqc -config
         true | coqtop
     - uses: actions/checkout@v4
-    - name: submodules-init
-      uses: snickerbockers/submodules-init@v4
+      with:
+        submodules: recursive
     - name: remove autogenerated
       run: etc/ci/remove_autogenerated.sh
     - name: some-early util

diff --git a/.github/workflows/docker-coq.yml b/.github/workflows/docker-coq.yml
@@ -0,0 +1,120 @@
+name: CI (Coq, docker, dev)
+
+on:
+  push:
+    branches: [ sp2019latest ]
+  pull_request:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 0 1 * *'
+
+jobs:
+  docker-build:
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+        - env: { COQ_VERSION: "master", DOCKER_COQ_VERSION: "dev", DOCKER_OCAML_VERSION: "default", SKIP_DISPLAY_TEST: "1", CC: "gcc", ALLOW_DIFF: "" }
+          os: 'ubuntu-latest'
+
+    runs-on: ${{ matrix.os }}
+    env: ${{ matrix.env }}
+    name: ${{ matrix.env.COQ_VERSION }}
+
+    concurrency:
+      group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }}
+      cancel-in-progress: true
+
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        submodules: recursive
+    - name: echo host build params
+      run: etc/ci/describe-system-config.sh
+    - name: echo container build params
+      uses: coq-community/docker-coq-action@v1
+      with:
+        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
+        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
+        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
+        custom_script: |
+          eval $(opam env)
+          etc/ci/describe-system-config.sh
+    - name: remove autogenerated
+      run: etc/ci/remove_autogenerated.sh
+    - name: install gcc
+      uses: coq-community/docker-coq-action@v1
+      with:
+        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
+        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
+        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
+        custom_script: |
+           #startGroup 'install gcc'
+           #sudo apt-get update -q
+           #sudo apt-get install g++-7 libssl-dev -y --allow-unauthenticated
+           #sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-7 60 --slave /usr/bin/g++ g++ /usr/bin/g++-7
+           #endGroup
+    - name: some-early util
+      uses: coq-community/docker-coq-action@v1
+      with:
+        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
+        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
+        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
+        custom_script: |
+           etc/ci/github-actions-docker-make.sh -j2 some-early util
+    - name: printlite lite
+      uses: coq-community/docker-coq-action@v1
+      with:
+        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
+        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
+        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
+        custom_script: |
+           etc/ci/github-actions-docker-make.sh -j2 printlite lite
+    - name: no-curves-proofs-non-specific
+      uses: coq-community/docker-coq-action@v1
+      with:
+        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
+        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
+        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
+        custom_script: |
+           etc/ci/github-actions-docker-make.sh -j2 no-curves-proofs-non-specific
+    - name: curves-proofs
+      uses: coq-community/docker-coq-action@v1
+      with:
+        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
+        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
+        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
+        custom_script: |
+           etc/ci/github-actions-docker-make.sh -j2 curves-proofs
+    - name: selected-specific selected-specific-display
+      uses: coq-community/docker-coq-action@v1
+      with:
+        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
+        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
+        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
+        custom_script: |
+           ALLOW_DIFF="${SKIP_DISPLAY_TEST}" etc/ci/github-actions-docker-make.sh -j2 selected-specific selected-specific-display
+    - name: selected-specific-display-test and more
+      uses: coq-community/docker-coq-action@v1
+      with:
+        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
+        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
+        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
+        custom_script: |
+           #startGroup selected-specific-display-test
+           #etc/ci/github-actions-docker-make.sh -j2 selected-specific-display-test
+           #endGroup
+           #if: env.SKIP_DISPLAY_TEST != '1'
+           #startGroup build-selected-test build-selected-bench
+           #etc/ci/github-actions-docker-make.sh -j2 build-selected-test build-selected-bench
+           #endGroup
+           #if: env.SKIP_DISPLAY_TEST != '1'
+           #startGroup test for adx
+           #etc/assert-adx.sh || true
+           #endGroup
+           #continue-on-error: true
+           #if: env.SKIP_DISPLAY_TEST != '1'
+           #startGroup selected-test selected-bench
+           #ALLOW_DIFF=1 SKIP_ICC="$(etc/assert-adx.sh || echo 1)" etc/ci/github-actions-docker-make.sh -j2 selected-test selected-bench
+           #endGroup
+           #if: env.SKIP_DISPLAY_TEST != '1'
diff --git a/etc/ci/describe-system-config.sh b/etc/ci/describe-system-config.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+cd -- "$( dirname -- "${BASH_SOURCE[0]}" )"
+cd ../..
+
+function run() {
+    "${SHELL}" -c "$@" || true
+}
+
+if [ ! -z "$CI" ]; then
+    function group() {
+        echo "::group::$@"
+        run "$@"
+        echo "::endgroup::"
+    }
+else
+    function group() { run "$@"; }
+fi
+
+group lscpu
+group uname -a
+group lsb_release -a
+group ulimit -aH
+group ulimit -aS
+group ghc --version
+group gcc -v
+group ocamlc -config
+group coqc --config
+group coqc --version
+group "true | coqtop"
+group etc/machine.sh
+group "echo PATH=$PATH"
diff --git a/etc/ci/github-actions-docker-make.sh b/etc/ci/github-actions-docker-make.sh
@@ -0,0 +1,22 @@
+#!/usr/bin/env bash
+
+set -x
+
+cd -- "$( dirname -- "${BASH_SOURCE[0]}" )"
+cd ../..
+
+if [ -z "${EXTRA_PACKAGES+x}" ]; then
+    EXTRA_PACKAGES=""
+fi
+
+sudo chmod -R a=u .
+# Work around https://github.com/actions/checkout/issues/766
+git config --global --add safe.directory "*"
+echo '::group::install general dependencies'
+sudo apt-get update -y
+sudo apt-get install -y python python3 bsdmainutils ${EXTRA_PACKAGES}
+eval $(opam env)
+echo '::endgroup::'
+echo '::remove-matcher owner=coq-problem-matcher::'
+etc/ci/describe-system-config.sh
+etc/ci/github-actions-make.sh "$@"