Skip to content

Commit 4f18dc2

Browse files
erikmdthery
erikmd
authored and
thery
committed
Add coq-native support (if available) as per CEP 48 (math-comp#45)
* For details, see: - https://opam.ocaml.org/packages/coq-native/ - CEP 48 <https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#note-to-library-developers-and-package-maintainers> * can be reverted anytime after the merge of rocq-prover/opam#1835 and the rebuild of `mathcomp/mathcomp:1.12.0-coq-8.12`
1 parent 7007712 commit 4f18dc2

File tree

6 files changed

+118
-12
lines changed

6 files changed

+118
-12
lines changed

‎.github/workflows/ci.yml

Lines changed: 56 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
name: Docker CI
2+
13
on: [push, pull_request]
24

35
jobs:
@@ -6,12 +8,59 @@ jobs:
68
strategy:
79
matrix:
810
image:
9-
- mathcomp/mathcomp:1.12.0-coq-8.10
10-
- mathcomp/mathcomp:1.12.0-coq-8.11
11-
- mathcomp/mathcomp:1.12.0-coq-8.12
11+
- mathcomp/mathcomp:1.12.0-coq-8.10
12+
- mathcomp/mathcomp:1.12.0-coq-8.11
13+
- mathcomp/mathcomp:1.12.0-coq-8.12 # 8.12.1+ support ocaml/dune#3210
14+
- coqorg/coq:8.13-native-ocaml-4.07 # with the coq-native opam pkg
15+
- coqorg/coq:8.14-native-ocaml-4.07 # with the coq-native opam pkg
16+
- mathcomp/mathcomp:1.12.0-coq-8.13 # (without coq-native for now)
17+
- mathcomp/mathcomp:1.12.0-coq-8.14 # (without coq-native for now)
18+
# the previous comments refer to https://github.com/coq/ceps/pull/48
1219
fail-fast: false
1320
steps:
14-
- uses: actions/checkout@v2
15-
- uses: coq-community/docker-coq-action@v1
16-
with:
17-
custom_image: ${{ matrix.image }}
21+
- uses: actions/checkout@v2
22+
- uses: coq-community/docker-coq-action@v1
23+
env:
24+
LIBRARY_NAME: 'SsrMultinomials'
25+
ROOT_THEORIES: 'mpoly monalg'
26+
with:
27+
opam_file: 'coq-mathcomp-multinomials.opam'
28+
custom_image: ${{ matrix.image }}
29+
export: 'LIBRARY_NAME ROOT_THEORIES'
30+
# Note: these native-compiler tests are generic,
31+
# thanks to env variables & the configure script
32+
after_script: |
33+
startGroup "Print native_compiler status"
34+
coqc -config
35+
. configure # sourcing mandatory
36+
coq_version
37+
endGroup
38+
# Note: Replace with "if coq_native_compiler"
39+
# to also test with Coq 8.12.1+
40+
if coq_native_compiler_default; then
41+
startGroup "Workaround permission issue"
42+
sudo chown -R coq:coq . # <--(§)
43+
endGroup
44+
startGroup "Check native_compiler on a test file"
45+
printf '%s\n' "From $LIBRARY_NAME Require Import $ROOT_THEORIES." > test.v
46+
coqc -debug -native-compiler yes test.v > stdout.txt || ret=$?
47+
cat stdout.txt
48+
( exit "${ret:-0}" )
49+
endGroup
50+
# in practice, we get ret=0 even if deps were not native-compiled
51+
# but the logs are useful...(*), so we keep this first test group
52+
# and add another test group which is less verbose, but stricter.
53+
startGroup "Check installation of .coq-native/ files"
54+
set -o pipefail
55+
# fail noisily if ever 'find' gives 'No such file or directory'
56+
num=$(find "$(coqc -where)/user-contrib/$LIBRARY_NAME" -type d -name ".coq-native" | wc -l)
57+
[ "$num" -gt 0 ]
58+
endGroup
59+
fi
60+
- name: Revert permissions
61+
# to avoid a warning at cleanup time
62+
if: ${{ always() }}
63+
run: sudo chown -R 1001:116 . # <--(§)
64+
65+
#(§)=> https://github.com/coq-community/docker-coq-action#permissions
66+
#(*)=> Cannot find native compiler file /home/coq/.opam/4.07.1/lib/coq/user-contrib/SsrMultinomials/.coq-native/NSsrMultinomials_ssrcomplements.cmxs

‎.gitignore

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,4 @@
11
/attic/
22
/_build/
3+
/src/dune
4+
*~

‎configure

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
#!/usr/bin/env bash
2+
# Erik Martin-Dorel, 2021 (configure script for SsrMultinomials)
3+
4+
dir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
5+
6+
le_version() {
7+
[ "$(printf '%s\n' "$1" "$2" | sort -V -u | tail -n1)" = "$2" ]
8+
}
9+
10+
# BEGIN TESTS
11+
fail_test() {
12+
echo "error: test $* failed" >&2; exit 2
13+
}
14+
unit_tests() {
15+
le_version "8.12.1" "8.12.1" || fail_test 0
16+
le_version "8.9.0" "8.12.1" || fail_test 1
17+
le_version "8.12.1" "8.12.2" || fail_test 2
18+
le_version "8.12.2" "8.13.0" || fail_test 3
19+
}
20+
# unit_tests
21+
# END TESTS
22+
23+
coq_version() {
24+
coqc --version | grep version | \
25+
sed -e 's/^.*version \([-0-9a-z.+~]\+\)\( .*\)\?$/\1/'
26+
}
27+
28+
coq_native_compiler_default() {
29+
coqc -config | grep -q 'COQ_NATIVE_COMPILER_DEFAULT=yes'
30+
}
31+
32+
coq_native_compiler() {
33+
cv=$(coq_version)
34+
{ le_version "8.12.1" "$cv" && ! le_version "8.13.0" "$cv"; } \
35+
|| coq_native_compiler_default
36+
}
37+
38+
main() {
39+
# Note: Replace with "if coq_native_compiler"
40+
# to also test with Coq 8.12.1+
41+
if coq_native_compiler_default; then
42+
echo 'coq-native support enabled!' >&2
43+
sed -e 's/;coq-native-disabled; \?//' "$dir/src/dune.in" > "$dir/src/dune"
44+
else
45+
cat "$dir/src/dune.in" > "$dir/src/dune"
46+
fi
47+
}
48+
49+
# Credits: https://stackoverflow.com/a/28776166/9164010
50+
( return 0 2>/dev/null ) || main
51+
# ./configure => Run main
52+
# . configure => Don't run main (useful in .github/workflows/ci.yml)

‎coq-mathcomp-multinomials.opam

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,16 @@
11
opam-version: "2.0"
2-
name: "coq-mathcomp-multinomials"
32
maintainer: "[email protected]"
43
homepage: "https://github.com/math-comp/multinomials"
54
bug-reports: "https://github.com/math-comp/multinomials/issues"
65
dev-repo: "git+https://github.com/math-comp/multinomials.git"
76
license: "CeCILL-B"
87
authors: ["Pierre-Yves Strub"]
9-
build: [ "dune" "build" "-p" name "-j" jobs ]
8+
build: [
9+
[ "bash" "./configure" ]
10+
[ "dune" "build" "-p" name "-j" jobs ]
11+
]
1012
depends: [
11-
"coq" {(>= "8.10" & < "8.14~") | = "dev"}
13+
"coq" {(>= "8.10" & < "8.15~") | = "dev"}
1214
"dune" {>= "2.5"}
1315
"coq-mathcomp-ssreflect" {(>= "1.12" & < "1.13~") | = "dev"}
1416
"coq-mathcomp-algebra"

‎dune-project

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
(lang dune 2.5)
2-
(using coq 0.2)
1+
(lang dune 2.8)
2+
(using coq 0.3)
33
(name multinomials)

‎src/dune renamed to ‎src/dune.in

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
(coq.theory
22
(name SsrMultinomials)
3+
;coq-native-disabled; (mode native)
34
(package coq-mathcomp-multinomials)
45
(flags -w -ambiguous-paths
56
-w -notation-overridden

0 commit comments

Comments
 (0)