From 859d5b6e9f83899a9fd2383db38a16ee973a5792 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 22 Oct 2023 10:04:57 -0700 Subject: [PATCH] [sp2019latest] [CI] Drop Coq < 8.16 In preparation for bumping bbv for https://github.com/mit-plv/bbv/pull/47 / https://github.com/coq/coq/pull/18164 --- .github/workflows/coq.yml | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 55293dbbe4..9d359470f5 100644 --- 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'