docker-coq.yml

name: CI (Coq, docker, dev)

on:
  push:
    branches: [ master , sp2019latest , v8.6 , v8.8 , v8.10 ]
  pull_request:
  merge_group:
  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_VALIDATE: "" , COQCHKEXTRAFLAGS: "-bytecode-compiler yes", EXTRA_GH_REPORTIFY: "--warnings", ALLOW_DIFF: "1" }
          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 COQCHKEXTRAFLAGS
        custom_script: |
          eval $(opam env)
          etc/ci/describe-system-config.sh
    - name: deps
      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 COQCHKEXTRAFLAGS
        custom_script: etc/ci/github-actions-docker-make.sh -j2 deps
    - name: all-except-generated
      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 COQCHKEXTRAFLAGS
        custom_script: etc/ci/github-actions-docker-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated
    - name: generated-files
      run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -f Makefile.examples -j2 generated-files
      if: github.event_name == 'pull_request' || ${{ matrix.env.COQ_VERSION }} != 'master'
    - run: tar -czvf generated-files.tgz fiat-*/
      if: ${{ failure() }}
    - name: upload generated files
      uses: actions/upload-artifact@v3
      with:
        name: generated-files-${{ matrix.env.COQ_VERSION }}
        path: generated-files.tgz
      if: ${{ failure() }}
    - name: upload OCaml files
      uses: actions/upload-artifact@v3
      with:
        name: ExtractionOCaml-${{ matrix.env.COQ_VERSION }}
        path: src/ExtractionOCaml
      if: always ()
    - name: standalone-haskell
      run: etc/ci/github-actions-make.sh -f Makefile.standalone -j1 standalone-haskell GHCFLAGS='+RTS -M6G -RTS'
    - name: upload Haskell files
      uses: actions/upload-artifact@v3
      with:
        name: ExtractionHaskell-${{ matrix.env.COQ_VERSION }}
        path: src/ExtractionHaskell
      if: always ()
    - name: display timing info
      run: cat time-of-build-pretty.log
    - name: display per-line timing info
      run: etc/ci/github-actions-display-per-line-timing.sh
#    - name: upload timing and .vo info
#      uses: actions/upload-artifact@v3
#      with:
#        name: build-outputs-${{ matrix.env.COQ_VERSION }}
#        path: .
#      if: always ()
    - name: validate
      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 COQCHKEXTRAFLAGS
        custom_script: etc/ci/github-actions-docker-make.sh TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"
      if: env.SKIP_VALIDATE == '' && github.event_name != 'pull_request'

  test-amd64:

    runs-on: ubuntu-latest

    concurrency:
      group: ${{ github.workflow }}-test-amd64-${{ github.head_ref || github.run_id }}
      cancel-in-progress: true
    needs: docker-build

    steps:
    - name: checkout repo
      uses: actions/checkout@v4
      with:
        submodules: recursive
    - name: Download a Build Artifact
      uses: actions/download-artifact@v3
      with:
        name: ExtractionOCaml-master
        path: src/ExtractionOCaml
    - name: make binaries executable
      run: chmod +x src/ExtractionOCaml/*
    - name: only-test-amd64-files
      run: etc/ci/github-actions-make.sh -f Makefile.examples -j2 only-test-amd64-files SLOWEST_FIRST=1
      env:
        ALLOW_DIFF: 1