[sp2019latest] [CI] Drop Coq < 8.16

In preparation for bumping bbv for mit-plv/bbv#47 / coq/coq#18164
mit-plv · Oct 22, 2023 · 859d5b6 · 859d5b6
1 parent d7b417f
commit 859d5b6
Showing 1 changed file with 4 additions and 7 deletions.
diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml
@@ -14,9 +14,9 @@ jobs:
     strategy:
       matrix:
         env:
-        - { COQ_VERSION: "master", COQ_PACKAGE: "coq"       , PPA: "ppa:jgross-h/coq-master-daily"            , SKIP_DISPLAY_TEST: "1", CC: "gcc", REMOVE_GLOBAL_ATTR: "" , ALLOW_DIFF: ""  }
-        - { COQ_VERSION: "8.15.2", COQ_PACKAGE: "coq-8.15.2", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08", SKIP_DISPLAY_TEST: "1", CC: "gcc", REMOVE_GLOBAL_ATTR: "" , ALLOW_DIFF: ""  }
-        - { COQ_VERSION: "8.14.1", COQ_PACKAGE: "coq-8.14.1", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08", SKIP_DISPLAY_TEST: "1", CC: "gcc", REMOVE_GLOBAL_ATTR: "" , ALLOW_DIFF: ""  }
+        - { 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: ""  }
 
     env: ${{ matrix.env }}
     name: ${{ matrix.env.COQ_VERSION }}
@@ -49,9 +49,6 @@ jobs:
       uses: snickerbockers/submodules-init@v4
     - name: remove autogenerated
       run: etc/ci/remove_autogenerated.sh
-    - name: remove global attribute
-      run: git ls-files --recurse-submodules "*.v" | xargs sed 's/#\[global\]//g' -i
-      if: env.REMOVE_GLOBAL_ATTR == '1'
     - name: some-early util
       run: etc/ci/github-actions-make.sh -j2 some-early util
     - name: printlite lite
@@ -61,7 +58,7 @@ jobs:
     - name: curves-proofs
       run: etc/ci/github-actions-make.sh -j2 curves-proofs
     - name: selected-specific selected-specific-display
-      run: ALLOW_DIFF="${SKIP_DISPLAY_TEST}${REMOVE_GLOBAL_ATTR}" etc/ci/github-actions-make.sh -j2 selected-specific selected-specific-display
+      run: ALLOW_DIFF="${SKIP_DISPLAY_TEST}" etc/ci/github-actions-make.sh -j2 selected-specific selected-specific-display
     - name: selected-specific-display-test
       run: etc/ci/github-actions-make.sh -j2 selected-specific-display-test
       if: env.SKIP_DISPLAY_TEST != '1'