From b5d928ed2a96d8d05e8267a3940a27e1c9ce32b2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 31 Oct 2023 17:46:55 -0700 Subject: [PATCH 1/3] User docker for master test --- .github/workflows/coq.yml | 5 +- .github/workflows/docker-coq.yml | 88 ++++++++++++++++++++++++++++ etc/ci/describe-system-config.sh | 32 ++++++++++ etc/ci/github-actions-docker-make.sh | 22 +++++++ 4 files changed, 144 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..050d33b865 --- /dev/null +++ b/.github/workflows/docker-coq.yml @@ -0,0 +1,88 @@ +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 SKUP_DISPLAY_TEST CC + custom_script: | + eval $(opam env) + etc/ci/describe-system-config.sh + - name: remove autogenerated + run: etc/ci/remove_autogenerated.sh + - name: build + 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 SKUP_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 + startGroup 'some-early util' + etc/ci/github-actions-docker-make.sh -j2 some-early util + endGroup + startGroup 'printlite lite' + etc/ci/github-actions-docker-make.sh -j2 printlite lite + endGroup + startGroup no-curves-proofs-non-specific + etc/ci/github-actions-docker-make.sh -j2 no-curves-proofs-non-specific + endGroup + startGroup curves-proofs + etc/ci/github-actions-docker-make.sh -j2 curves-proofs + endGroup + startGroup selected-specific selected-specific-display + ALLOW_DIFF="${SKIP_DISPLAY_TEST}" etc/ci/github-actions-docker-make.sh -j2 selected-specific selected-specific-display + endGroup + #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 "$@" From 4dc1d15bca4f66051e0deedf93b584fa8ec99af3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 31 Oct 2023 19:31:14 -0700 Subject: [PATCH 2/3] Comment out unused gcc --- .github/workflows/docker-coq.yml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/.github/workflows/docker-coq.yml b/.github/workflows/docker-coq.yml index 050d33b865..2f3565a4ef 100644 --- a/.github/workflows/docker-coq.yml +++ b/.github/workflows/docker-coq.yml @@ -49,11 +49,11 @@ jobs: ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} export: CI ALLOW_DIFF SKUP_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 + #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 startGroup 'some-early util' etc/ci/github-actions-docker-make.sh -j2 some-early util endGroup From 7f488d949b82c0fa604c243d6a0bdef3ab49200c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 31 Oct 2023 19:45:32 -0700 Subject: [PATCH 3/3] Split up docker action --- .github/workflows/docker-coq.yml | 58 +++++++++++++++++++++++++------- 1 file changed, 45 insertions(+), 13 deletions(-) diff --git a/.github/workflows/docker-coq.yml b/.github/workflows/docker-coq.yml index 2f3565a4ef..005a74c39b 100644 --- a/.github/workflows/docker-coq.yml +++ b/.github/workflows/docker-coq.yml @@ -36,39 +36,71 @@ jobs: with: coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} - export: CI ALLOW_DIFF SKUP_DISPLAY_TEST CC + 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: build + - 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 SKUP_DISPLAY_TEST CC + 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 - startGroup 'some-early util' + - 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 - endGroup - startGroup 'printlite lite' + - 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 - endGroup - startGroup no-curves-proofs-non-specific + - 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 - endGroup - startGroup curves-proofs + - 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 - endGroup - startGroup selected-specific selected-specific-display + - 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 - endGroup + - 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