Add coq-native support (if available) as per CEP 48 (#45)

erikmd · web-flow · commit c0d3db4e8689 · 2021-09-29T08:06:26.000+02:00
* 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`
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -1,3 +1,5 @@
+name: Docker CI
+
 on: [push, pull_request]
 
 jobs:
@@ -6,12 +8,59 @@ jobs:
     strategy:
       matrix:
         image:
-        -  mathcomp/mathcomp:1.12.0-coq-8.10
-        -  mathcomp/mathcomp:1.12.0-coq-8.11
-        -  mathcomp/mathcomp:1.12.0-coq-8.12
+          - mathcomp/mathcomp:1.12.0-coq-8.10
+          - mathcomp/mathcomp:1.12.0-coq-8.11
+          - mathcomp/mathcomp:1.12.0-coq-8.12 # 8.12.1+ support ocaml/dune#3210
+          - coqorg/coq:8.13-native-ocaml-4.07 # with the coq-native opam pkg
+          - coqorg/coq:8.14-native-ocaml-4.07 # with the coq-native opam pkg
+          - mathcomp/mathcomp:1.12.0-coq-8.13 # (without coq-native for now)
+          - mathcomp/mathcomp:1.12.0-coq-8.14 # (without coq-native for now)
+          # the previous comments refer to https://github.com/coq/ceps/pull/48
       fail-fast: false
     steps:
-    - uses: actions/checkout@v2
-    - uses: coq-community/docker-coq-action@v1
-      with:
-        custom_image: ${{ matrix.image }}
+      - uses: actions/checkout@v2
+      - uses: coq-community/docker-coq-action@v1
+        env:
+          LIBRARY_NAME: 'SsrMultinomials'
+          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
+              . configure  # sourcing mandatory
+              coq_version
+            endGroup
+            # Note: Replace with "if coq_native_compiler"
+            # to also test with Coq 8.12.1+
+            if coq_native_compiler_default; 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
+                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/SsrMultinomials/.coq-native/NSsrMultinomials_ssrcomplements.cmxs
diff --git a/.gitignore b/.gitignore
@@ -1,2 +1,4 @@
 /attic/
 /_build/
+/src/dune
+*~
diff --git a/configure b/configure
@@ -0,0 +1,52 @@
+#!/usr/bin/env bash
+# Erik Martin-Dorel, 2021 (configure script for SsrMultinomials)
+
+dir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )
+
+le_version() {
+    [ "$(printf '%s\n' "$1" "$2" | sort -V -u | tail -n1)" = "$2" ]
+}
+
+# BEGIN TESTS
+fail_test() {
+    echo "error: test $* failed" >&2; exit 2
+}
+unit_tests() {
+    le_version "8.12.1" "8.12.1" || fail_test 0
+    le_version "8.9.0" "8.12.1" || fail_test 1
+    le_version "8.12.1" "8.12.2" || fail_test 2
+    le_version "8.12.2" "8.13.0" || fail_test 3
+}
+# unit_tests
+# END TESTS
+
+coq_version() {
+    coqc --version | grep version | \
+        sed -e 's/^.*version \([-0-9a-z.+~]\+\)\( .*\)\?$/\1/'
+}
+
+coq_native_compiler_default() {
+    coqc -config | grep -q 'COQ_NATIVE_COMPILER_DEFAULT=yes'
+}
+
+coq_native_compiler() {
+    cv=$(coq_version)
+    { le_version "8.12.1" "$cv" && ! le_version "8.13.0" "$cv"; } \
+        || coq_native_compiler_default
+}
+
+main() {
+    # Note: Replace with "if coq_native_compiler"
+    # to also test with Coq 8.12.1+
+    if coq_native_compiler_default; then
+        echo 'coq-native support enabled!' >&2
+        sed -e 's/;coq-native-disabled; \?//' "$dir/src/dune.in" > "$dir/src/dune"
+    else
+        cat "$dir/src/dune.in" > "$dir/src/dune"
+    fi
+}
+
+# Credits: https://stackoverflow.com/a/28776166/9164010
+( return 0 2>/dev/null ) || main
+# ./configure => Run main
+# . configure => Don't run main (useful in .github/workflows/ci.yml)
diff --git a/coq-mathcomp-multinomials.opam b/coq-mathcomp-multinomials.opam
@@ -1,14 +1,16 @@
 opam-version: "2.0"
-name: "coq-mathcomp-multinomials"
 maintainer: "pierre-yves@strub.nu"
 homepage: "https://github.com/math-comp/multinomials"
 bug-reports: "https://github.com/math-comp/multinomials/issues"
 dev-repo: "git+https://github.com/math-comp/multinomials.git"
 license: "CeCILL-B"
 authors: ["Pierre-Yves Strub"]
-build: [ "dune" "build" "-p" name "-j" jobs ]
+build: [
+  [ "bash" "./configure" ]
+  [ "dune" "build" "-p" name "-j" jobs ]
+]
 depends: [
-  "coq"                    {(>= "8.10" & < "8.14~") | = "dev"}
+  "coq"                    {(>= "8.10" & < "8.15~") | = "dev"}
   "dune"                   {>= "2.5"}
   "coq-mathcomp-ssreflect" {(>= "1.12" & < "1.13~") | = "dev"}
   "coq-mathcomp-algebra"
diff --git a/dune-project b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
-(using coq 0.2)
+(lang dune 2.8)
+(using coq 0.3)
 (name multinomials)
diff --git a/src/dune.in b/src/dune.in
@@ -1,5 +1,6 @@
 (coq.theory
  (name SsrMultinomials)
+ ;coq-native-disabled; (mode native)
  (package coq-mathcomp-multinomials)
  (flags -w -ambiguous-paths
         -w -notation-overridden

-Original file line number
+Diff line change
@@ @@ -1,2 +1,4 @@ @@
 /attic/
 /_build/
 +/src/dune
 +*~