Skip to content

Qualifying expr.expr and cie coming from Uncurried and EdDSA.sign from Spec #4151

Qualifying expr.expr and cie coming from Uncurried and EdDSA.sign from Spec

Qualifying expr.expr and cie coming from Uncurried and EdDSA.sign from Spec #4151

Workflow file for this run

name: CI (Coq)
on:
push:
pull_request:
schedule:
- cron: '0 0 1 * *'
jobs:
build:
runs-on: ubuntu-20.04
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: "" }
env: ${{ matrix.env }}
name: ${{ matrix.env.COQ_VERSION }}
concurrency:
group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }}
cancel-in-progress: true
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
coqc -config
true | coqtop
- uses: actions/checkout@v3
- name: submodules-init
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
run: etc/ci/github-actions-make.sh -j2 printlite lite
- 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: 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
- 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: 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'
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' }}