ci.yml

name: Docker CI

on: [push, pull_request]

jobs:
  build:
    runs-on: ubuntu-20.04
    strategy:
      matrix:
        image:
          - mathcomp/mathcomp:2.0.0-coq-8.16
          - mathcomp/mathcomp:2.0.0-coq-8.17
          - mathcomp/mathcomp:2.0.0-coq-8.18
          - mathcomp/mathcomp:2.1.0-coq-8.16
          - mathcomp/mathcomp:2.1.0-coq-8.17
          - mathcomp/mathcomp:2.1.0-coq-8.18
          - mathcomp/mathcomp:2.2.0-coq-8.16
          - mathcomp/mathcomp:2.2.0-coq-8.17
          - mathcomp/mathcomp:2.2.0-coq-8.18
          - mathcomp/mathcomp:2.2.0-coq-8.19
          - mathcomp/mathcomp-dev:coq-8.18
          - mathcomp/mathcomp-dev:coq-8.19
          - mathcomp/mathcomp-dev:coq-dev
      fail-fast: false
    steps:
      - uses: actions/checkout@v2
      - uses: coq-community/docker-coq-action@v1
        env:
          LIBRARY_NAME: 'mathcomp.multinomials'
          ROOT_THEORIES: 'mpoly monalg'
        with:
          opam_file: 'coq-mathcomp-multinomials.opam'
          custom_image: ${{ matrix.image }}
          export: 'LIBRARY_NAME ROOT_THEORIES'
          # Note: these native-compiler tests are generic,
          # thanks to env variables & the configure script
          after_script: |
            startGroup "Print native_compiler status"
              coqc -config
              coq_version() {
                coqc --version | grep version | \
                  sed -e 's/^.*version \([-0-9a-z.+~]\+\)\( .*\)\?$/\1/'
              }
              le_version() {
                [ "$(printf '%s\n' "$1" "$2" | sort -V -u | tail -n1)" = "$2" ]
              }
              coq_native_compiler_default() {
                coqc -config | grep -q 'COQ_NATIVE_COMPILER_DEFAULT=yes'
              }
              coqv=$(coq_version)
              coq_native_compiler_default && echo native-compiler
              coq_native=$(opam var coq-native:installed)
            endGroup
            if [ "$coq_native" = "true" ] && le_version "8.13.0" "$coqv"; then
              startGroup "Workaround permission issue"
                sudo chown -R coq:coq .  # <--(§)
              endGroup
              startGroup "Check native_compiler on a test file"
                printf '%s\n' "From $LIBRARY_NAME Require Import $ROOT_THEORIES." > test.v
                if le_version "8.14" "$coqv"; then
                  debug=(-d native-compiler)
                else
                  debug=(-debug)
                fi
                coqc "${debug[@]}" -native-compiler yes test.v > stdout.txt || ret=$?
                cat stdout.txt
                ( exit "${ret:-0}" )
              endGroup
              # in practice, we get ret=0 even if deps were not native-compiled
              # but the logs are useful...(*), so we keep this first test group
              # and add another test group which is less verbose, but stricter.
              startGroup "Check installation of .coq-native/ files"
                set -o pipefail
                # fail noisily if ever 'find' gives 'No such file or directory'
                num=$(find "$(coqc -where)/user-contrib/${LIBRARY_NAME//\.//}" -type d -name ".coq-native" | wc -l)
                [ "$num" -gt 0 ]
              endGroup
            fi
      - name: Revert permissions
        # to avoid a warning at cleanup time
        if: ${{ always() }}
        run: sudo chown -R 1001:116 .  # <--(§)

#(§)=> https://github.com/coq-community/docker-coq-action#permissions
#(*)=> Cannot find native compiler file /home/coq/.opam/4.07.1/lib/coq/user-contrib/mathcomp.multinomials/.coq-native/Nmathcomp.multinomials_ssrcomplements.cmxs