From 77a2f7db22cfe88d92c6331e20fce22cd3b9bc1d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 31 Oct 2023 20:03:16 -0700 Subject: [PATCH] [sp2019latest] User docker for master test (#1696) * User docker for master test * Comment out unused gcc * Split up docker action --- .github/workflows/coq.yml | 5 +- .github/workflows/docker-coq.yml | 120 +++++++++++++++++++++++++++ etc/ci/describe-system-config.sh | 32 +++++++ etc/ci/github-actions-docker-make.sh | 22 +++++ 4 files changed, 176 insertions(+), 3 deletions(-) create mode 100644 .github/workflows/docker-coq.yml create mode 100755 etc/ci/describe-system-config.sh create mode 100755 etc/ci/github-actions-docker-make.sh diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 230c83d187..db54774403 100644 --- 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 new file mode 100644 index 0000000000..005a74c39b --- /dev/null +++ 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 new file mode 100755 index 0000000000..db767d4163 --- /dev/null +++ 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 new file mode 100755 index 0000000000..92b41e9b6c --- /dev/null +++ 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 "$@"