1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
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:2.2.0-coq-8.20
- mathcomp/mathcomp:2.2.0-coq-dev
- mathcomp/mathcomp:2.3.0-coq-8.18
- mathcomp/mathcomp:2.3.0-coq-8.19
- mathcomp/mathcomp:2.3.0-coq-8.20
- mathcomp/mathcomp:2.3.0-coq-dev
- mathcomp/mathcomp-dev:coq-8.18
- mathcomp/mathcomp-dev:coq-8.19
- mathcomp/mathcomp-dev:coq-8.20
- 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
|
