Skip to content

Add a test-suite target so swe bench can uniformly test different com… #643

Add a test-suite target so swe bench can uniformly test different com…

Add a test-suite target so swe bench can uniformly test different com… #643

Workflow file for this run

name: CI (Coq)
on:
push:
pull_request:
schedule:
- cron: '0 0 1 * *'
jobs:
build:
runs-on: ubuntu-latest
strategy:
matrix:
env:
- { COQ_VERSION: "8.11.0", COQ_PACKAGE: "coq-8.11.0", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05", SKIP_DISPLAY_TEST: "1", CC: "gcc" }
- { COQ_VERSION: "8.10.2", COQ_PACKAGE: "coq-8.10.2", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05", SKIP_DISPLAY_TEST: "1", CC: "gcc" }
- { COQ_VERSION: "8.9.1" , COQ_PACKAGE: "coq-8.9.1" , PPA: "ppa:jgross-h/many-coq-versions" , SKIP_DISPLAY_TEST: "1", CC: "gcc" }
- { COQ_VERSION: "8.8.2" , COQ_PACKAGE: "coq-8.8.2" , PPA: "ppa:jgross-h/many-coq-versions" , SKIP_DISPLAY_TEST: "" , CC: "gcc" }
- { COQ_VERSION: "8.7.2" , COQ_PACKAGE: "coq-8.7.2" , PPA: "ppa:jgross-h/many-coq-versions" , SKIP_DISPLAY_TEST: "" , CC: "gcc" }
- { COQ_VERSION: "master", COQ_PACKAGE: "coq" , PPA: "ppa:jgross-h/coq-master-daily" , SKIP_DISPLAY_TEST: "1", CC: "gcc" }
- { COQ_VERSION: "v8.11" , COQ_PACKAGE: "coq" , PPA: "ppa:jgross-h/coq-8.11-daily" , SKIP_DISPLAY_TEST: "1", CC: "gcc" }
- { COQ_VERSION: "v8.10" , COQ_PACKAGE: "coq" , PPA: "ppa:jgross-h/coq-8.10-daily" , SKIP_DISPLAY_TEST: "1", CC: "gcc" }
- { COQ_VERSION: "v8.9" , COQ_PACKAGE: "coq" , PPA: "ppa:jgross-h/coq-8.9-daily" , SKIP_DISPLAY_TEST: "1", CC: "gcc" }
- { COQ_VERSION: "v8.8" , COQ_PACKAGE: "coq" , PPA: "ppa:jgross-h/coq-8.8-daily" , SKIP_DISPLAY_TEST: "" , CC: "gcc" }
- { COQ_VERSION: "v8.7" , COQ_PACKAGE: "coq" , PPA: "ppa:jgross-h/coq-8.7-daily" , SKIP_DISPLAY_TEST: "" , CC: "gcc" }
env: ${{ matrix.env }}
steps:
- name: install gcc
run: |
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
- name: install Coq
run: |
if [ ! -z "$PPA" ]; then sudo add-apt-repository "$PPA" -y; fi
sudo apt-get update -q
sudo apt-get install ocaml-findlib $COQ_PACKAGE -y --allow-unauthenticated
- name: echo build params
run: |
lscpu
uname -a
lsb_release -a
coqc --version
echo | coqtop
- uses: actions/checkout@v2
- name: submodules-init
uses: snickerbockers/submodules-init@v4
- name: remove autogenerated
run: etc/ci/remove_autogenerated.sh
- name: some-early util
run: etc/ci/github-actions-make.sh -j2 some-early util
- name: printlite lite
run: etc/ci/github-actions-make.sh -j2 printlite lite
- name: pre-standalone
run: etc/ci/github-actions-make.sh -j2 pre-standalone
- name: new-pipeline
run: etc/ci/github-actions-make.sh -j2 new-pipeline
- name: no-curves-proofs-non-specific
run: etc/ci/github-actions-make.sh -j2 no-curves-proofs-non-specific
- name: curves-proofs
run: etc/ci/github-actions-make.sh -j2 curves-proofs
- name: standalone-ocaml
run: etc/ci/github-actions-make.sh -j2 standalone-ocaml
- name: selected-specific selected-specific-display c-files
run: ALLOW_DIFF="${SKIP_DISPLAY_TEST}" etc/ci/github-actions-make.sh -j2 selected-specific selected-specific-display c-files
- name: selected-specific-display-test
run: etc/ci/github-actions-make.sh -j2 selected-specific-display-test
if: env.SKIP_DISPLAY_TEST != '1'
- name: build-selected-test build-selected-bench
run: etc/ci/github-actions-make.sh -j2 build-selected-test build-selected-bench
if: env.SKIP_DISPLAY_TEST != '1'
- name: standalone-ocaml c-files test-c-files
run: etc/ci/github-actions-make.sh -j2 test-c-files
if: env.SKIP_DISPLAY_TEST != '1'
- name: test for adx
run: etc/assert-adx.sh
continue-on-error: true
if: env.SKIP_DISPLAY_TEST != '1'
- name: selected-test selected-bench
run: ALLOW_DIFF=1 SKIP_ICC="$(etc/assert-adx.sh || echo 1)" etc/ci/github-actions-make.sh -j2 selected-test selected-bench
if: env.SKIP_DISPLAY_TEST != '1'