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
mit-plv · Oct 4, 2024 · aad1a9b · aad1a9b
1 parent 87581f8
commit aad1a9b
Show file tree

Hide file tree

Showing 2 changed files with 91 additions and 63 deletions.
diff --git 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
@@ -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' }}