coq.yml

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", 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 }}

    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@v4
      with:
        submodules: recursive
    - 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: 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}" 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' }}