Generalize some results in monalg to nmodType and semiRingType #176
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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-dev:coq-8.16 | |
| - mathcomp/mathcomp-dev:coq-8.17 | |
| - mathcomp/mathcomp-dev:coq-8.18 | |
| - 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 |