From 4f18dc2bf4f42e18802785688007f909bba9e524 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Wed, 29 Sep 2021 08:06:26 +0200 Subject: [PATCH] Add coq-native support (if available) as per CEP 48 (#45) * For details, see: - https://opam.ocaml.org/packages/coq-native/ - CEP 48 * can be reverted anytime after the merge of https://github.com/coq/opam-coq-archive/pull/1835 and the rebuild of `mathcomp/mathcomp:1.12.0-coq-8.12` --- .github/workflows/ci.yml | 63 ++++++++++++++++++++++++++++++---- .gitignore | 2 ++ configure | 52 ++++++++++++++++++++++++++++ coq-mathcomp-multinomials.opam | 8 +++-- dune-project | 4 +-- src/{dune => dune.in} | 1 + 6 files changed, 118 insertions(+), 12 deletions(-) create mode 100755 configure rename src/{dune => dune.in} (85%) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d4cb324..b0c1d1c 100644 --- 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 index 40cb23e..dcfe5ad 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,4 @@ /attic/ /_build/ +/src/dune +*~ diff --git a/configure b/configure new file mode 100755 index 0000000..1c5c6fc --- /dev/null +++ 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 index 4a7ee7b..84d57aa 100644 --- 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 index ac9f9fb..7e29f95 100644 --- 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 b/src/dune.in similarity index 85% rename from src/dune rename to src/dune.in index 197688c..3acf78f 100644 --- a/src/dune +++ 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