From aad1a9b264bc619f8d41181fe50c8bf91d67538c Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 4 Oct 2024 13:24:25 -0700 Subject: [PATCH] Use docker for all Coq versions (#161) * Use docker for all Coq versions I don't really want to keep updating the ubuntu packages * Comment out coq.yml * Add back validate job --- .github/workflows/coq-docker.yml | 32 +++++++- .github/workflows/coq.yml | 122 +++++++++++++++---------------- 2 files changed, 91 insertions(+), 63 deletions(-) diff --git a/.github/workflows/coq-docker.yml b/.github/workflows/coq-docker.yml index 070d0fe8d..e5546644a 100644 --- a/.github/workflows/coq-docker.yml +++ b/.github/workflows/coq-docker.yml @@ -17,8 +17,9 @@ jobs: strategy: fail-fast: false matrix: - #coq-version: [ '8.16' ] - #extra-gh-reportify: [ '' ] + coq-version: [ '8.18', '8.19', '8.20' ] + extra-gh-reportify: [ '' ] + skip-validate: [ '' ] include: - coq-version: 'dev' extra-gh-reportify: '--warnings' @@ -51,6 +52,33 @@ jobs: CI=1 etc/ci/describe-system-config.sh etc/ci/github-actions-make.sh ${{ matrix.extra-gh-reportify }} -j2 all etc/ci/github-actions-make.sh ${{ matrix.extra-gh-reportify }} -j2 perf-Sanity + - 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 +# - name: upload timing and .vo info +# uses: actions/upload-artifact@v1 +# with: +# name: build-outputs-${{ matrix.env.COQ_VERSION }} +# path: . +# if: always () + - name: validate + uses: coq-community/docker-coq-action@v1 + with: + coq_version: ${{ matrix.coq-version }} + ocaml_version: default + custom_script: | + 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-is-python3 python3 + eval $(opam env) + echo '::endgroup::' + echo '::remove-matcher owner=coq-problem-matcher::' + etc/ci/github-actions-make.sh TIMED=1 validate COQCHKFLAGS="-o" + if: matrix.skip-validate == '' && github.event_name != 'pull_request' docker-check-all: runs-on: ubuntu-latest diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 4e216c25e..ede70d062 100644 --- a/.github/workflows/coq.yml +++ b/.github/workflows/coq.yml @@ -1,68 +1,68 @@ -name: CI (Coq) +# name: CI (Coq) -on: - push: - branches: [ master ] - pull_request: - merge_group: - workflow_dispatch: - release: - types: [published] - schedule: - - cron: '0 0 1 * *' +# on: +# push: +# branches: [ master ] +# pull_request: +# merge_group: +# workflow_dispatch: +# release: +# types: [published] +# schedule: +# - cron: '0 0 1 * *' -jobs: - build: +# jobs: +# build: - strategy: - fail-fast: false - matrix: - env: - - { COQ_VERSION: "8.18.0", COQ_PACKAGE: "coq-8.18.0 libcoq-8.18.0-ocaml-dev", SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11" } - - { COQ_VERSION: "8.17.1", COQ_PACKAGE: "coq-8.17.1 libcoq-8.17.1-ocaml-dev", SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11" } +# strategy: +# fail-fast: false +# matrix: +# env: +# - { COQ_VERSION: "8.18.0", COQ_PACKAGE: "coq-8.18.0 libcoq-8.18.0-ocaml-dev", SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11" } +# - { COQ_VERSION: "8.17.1", COQ_PACKAGE: "coq-8.17.1 libcoq-8.17.1-ocaml-dev", SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11" } - env: ${{ matrix.env }} - runs-on: ubuntu-latest +# env: ${{ matrix.env }} +# runs-on: ubuntu-latest - concurrency: - group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true +# concurrency: +# group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }} +# cancel-in-progress: true - steps: - - name: install Coq - run: | - if [ ! -z "$PPA" ]; then sudo add-apt-repository "$PPA" -y; fi - sudo apt-get -o Acquire::Retries=30 update -q - sudo apt-get -o Acquire::Retries=30 install ocaml-findlib $COQ_PACKAGE -y --allow-unauthenticated - - uses: actions/checkout@v4 - with: - submodules: recursive - - name: echo build params - run: etc/ci/describe-system-config.sh - - name: all - run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 all - - name: perf-Sanity - run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 perf-Sanity - - 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 -# - name: upload timing and .vo info -# uses: actions/upload-artifact@v1 -# with: -# name: build-outputs-${{ matrix.env.COQ_VERSION }} -# path: . -# if: always () - - name: validate - run: make TIMED=1 validate COQCHKFLAGS="-o" - if: matrix.env.SKIP_VALIDATE == '' && github.event_name != 'pull_request' +# steps: +# - name: install Coq +# run: | +# if [ ! -z "$PPA" ]; then sudo add-apt-repository "$PPA" -y; fi +# sudo apt-get -o Acquire::Retries=30 update -q +# sudo apt-get -o Acquire::Retries=30 install ocaml-findlib $COQ_PACKAGE -y --allow-unauthenticated +# - uses: actions/checkout@v4 +# with: +# submodules: recursive +# - name: echo build params +# run: etc/ci/describe-system-config.sh +# - name: all +# run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 all +# - name: perf-Sanity +# run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 perf-Sanity +# - 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 +# # - name: upload timing and .vo info +# # uses: actions/upload-artifact@v1 +# # with: +# # name: build-outputs-${{ matrix.env.COQ_VERSION }} +# # path: . +# # if: always () +# - name: validate +# run: make TIMED=1 validate COQCHKFLAGS="-o" +# if: matrix.env.SKIP_VALIDATE == '' && github.event_name != 'pull_request' - check-all: - runs-on: ubuntu-latest - needs: build - if: always() - steps: - - run: echo 'The triggering workflow passed' - if: ${{ needs.build.result == 'success' }} - - run: echo 'The triggering workflow failed' && false - if: ${{ needs.build.result != 'success' }} +# check-all: +# runs-on: ubuntu-latest +# needs: build +# if: always() +# steps: +# - run: echo 'The triggering workflow passed' +# if: ${{ needs.build.result == 'success' }} +# - run: echo 'The triggering workflow failed' && false +# if: ${{ needs.build.result != 'success' }}