docker-coq.yml

name: CI (Coq, docker, dev)

on:
  push:
    branches: [ sp2019latest ]
  pull_request:
  workflow_dispatch:
  schedule:
    - cron: '0 0 1 * *'

jobs:
  docker-build:
    strategy:
      fail-fast: false
      matrix:
        include:
        - env: { COQ_VERSION: "master", DOCKER_COQ_VERSION: "dev", DOCKER_OCAML_VERSION: "default", SKIP_DISPLAY_TEST: "1", CC: "gcc", ALLOW_DIFF: "" }
          os: 'ubuntu-latest'

    runs-on: ${{ matrix.os }}
    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:
    - uses: actions/checkout@v4
      with:
        submodules: recursive
    - name: echo host build params
      run: etc/ci/describe-system-config.sh
    - name: echo container build params
      uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
        custom_script: |
          eval $(opam env)
          etc/ci/describe-system-config.sh
    - name: remove autogenerated
      run: etc/ci/remove_autogenerated.sh
    - name: install dependencies
      uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
        custom_script: |
           #startGroup 'install gcc'
           #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
           #endGroup
           startGroup 'install dependencies'
           sudo apt-get -o Acquire::Retries=30 update -q
           sudo apt-get -o Acquire::Retries=30 install python3-is-python -y --allow-unauthenticated
           endGroup
    - name: some-early util
      uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
        custom_script: |
           etc/ci/github-actions-docker-make.sh -j2 some-early util
    - name: printlite lite
      uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
        custom_script: |
           etc/ci/github-actions-docker-make.sh -j2 printlite lite
    - name: no-curves-proofs-non-specific
      uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
        custom_script: |
           etc/ci/github-actions-docker-make.sh -j2 no-curves-proofs-non-specific
    - name: curves-proofs
      uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
        custom_script: |
           etc/ci/github-actions-docker-make.sh -j2 curves-proofs
    - name: selected-specific selected-specific-display
      uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
        custom_script: |
           ALLOW_DIFF="${SKIP_DISPLAY_TEST}" etc/ci/github-actions-docker-make.sh -j2 selected-specific selected-specific-display
    - name: selected-specific-display-test and more
      uses: coq-community/docker-coq-action@v1
      with:
        coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }}
        ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }}
        export: CI ALLOW_DIFF SKIP_DISPLAY_TEST CC
        custom_script: |
           #startGroup selected-specific-display-test
           #etc/ci/github-actions-docker-make.sh -j2 selected-specific-display-test
           #endGroup
           #if: env.SKIP_DISPLAY_TEST != '1'
           #startGroup build-selected-test build-selected-bench
           #etc/ci/github-actions-docker-make.sh -j2 build-selected-test build-selected-bench
           #endGroup
           #if: env.SKIP_DISPLAY_TEST != '1'
           #startGroup test for adx
           #etc/assert-adx.sh || true
           #endGroup
           #continue-on-error: true
           #if: env.SKIP_DISPLAY_TEST != '1'
           #startGroup selected-test selected-bench
           #ALLOW_DIFF=1 SKIP_ICC="$(etc/assert-adx.sh || echo 1)" etc/ci/github-actions-docker-make.sh -j2 selected-test selected-bench
           #endGroup
           #if: env.SKIP_DISPLAY_TEST != '1'