coq-action.yml

---
name: CI

on:
  push:
    branches:
      - master
    paths-ignore:
      - 'lib/**'
  pull_request:
    paths-ignore:
      - 'lib/**'

jobs:
  build:
    runs-on: ubuntu-latest
    strategy:
      fail-fast: false
      matrix:
        # ATTENTION: the "matrix" section must be identical for the "build" and "test" job
        # except for the "make_target" field and make_target related excludes
        coq_version:
          # See https://github.com/coq-community/docker-coq/wiki for supported images
#          - '8.17'
          - '8.18'
          - '8.19'
          - 'dev'
        bit_size:
          - 32
          - 64
        make_target:
          - vst
        exclude:   
#         - coq_version: 8.17
#            bit_size: 32
          - coq_version: 8.18
            bit_size: 32
          - coq_version: dev
            bit_size: 32
    steps:
      - uses: actions/checkout@v2
        with:
          submodules: true
      - uses: coq-community/docker-coq-action@v1
        with:
          coq_version: ${{ matrix.coq_version }}
          # See https://github.com/coq-community/docker-coq-action/tree/v1 for usage
          before_install: |
            startGroup "Opam config"
              opam repo add -y prerelease file://$(pwd)/opam-prerelease
              opam update -y
              opam config list; opam repo list; opam list
            endGroup
          install: |
            startGroup "Install dependencies"
              opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13.1' || 'coq-compcert.3.13.1' }}
              # Required by test2
              opam install -y coq-ext-lib
            endGroup
          # See https://github.com/coq-community/docker-coq-action/tree/v1#permissions
          before_script: |
            startGroup "Workaround permission issue"
              sudo chmod -R a=u .
            endGroup
          script: |
            startGroup "Build & Install"
              # put the first version back once CompCert 3.15 is in the Coq Platform
              # make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }} IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=bundled IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
            endGroup
          after_script: |
            startGroup 'Copy Opam coq/user-contrib and coq-variant'
              cp -R -v "$(opam var lib)"/coq/user-contrib .
              mkdir -p "$(opam var lib)"/coq-variant/dummy
              cp -R -v "$(opam var lib)"/coq-variant .
            endGroup
          uninstall:
      - name: 'Create archive'
        run: tar -cpvzf archive.tgz * .depend
      - name: 'Upload archive'
        uses: actions/upload-artifact@v2
        with:
          name: 'VST build artifacts ${{matrix.coq_version}} ${{matrix.bit_size}}'
          path: archive.tgz
          retention-days: 1

  test:
    needs: build
    runs-on: ubuntu-latest
    strategy:
      fail-fast: false
      matrix:
        coq_version:
#          - '8.17'
          - '8.18'
          - '8.19'
          - 'dev' 
        make_target:
          - assumptions.txt
          - test
          - test2
          - test3
          - test4
          - test5
        bit_size:
          - 32
          - 64
        exclude:
#          - coq_version: 8.17
#            bit_size: 32
          - coq_version: 8.18
            bit_size: 32
          - coq_version: dev
            bit_size: 32
          - bit_size: 64
            make_target: test3
          - bit_size: 32
            make_target: test4
          - bit_size: 32
            make_target: test5

    steps:
      - name: 'Download archive'
        uses: actions/download-artifact@v2
        id: download
        with:
          name: 'VST build artifacts ${{matrix.coq_version}} ${{matrix.bit_size}}'
      - name: 'Extract archive'
        run: tar -xvpzf archive.tgz
      - uses: coq-community/docker-coq-action@v1
        with:
          coq_version: ${{ matrix.coq_version }}
          install: |
            startGroup "Copy downloaded Opam coq/user-contrib and coq-variant"
              cp -R -v user-contrib/* "$(opam var lib)"/coq/user-contrib
              mkdir -p "$(opam var lib)"/coq-variant
              cp -R -v coq-variant/* "$(opam var lib)"/coq-variant
            endGroup
          before_script: |
            startGroup "Workaround permission issue"
              sudo chmod -R a=u .
            endGroup
          script: |
            startGroup "Build & Install"
              make -f util/make-touch  IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
              # put the first version back once CompCert 3.15 is in the Coq Platform
              # make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }}  IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
              make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=bundled IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true
            endGroup
          uninstall: