From aea7b4c5029562a5ddddc66c7e20ef27687634a6 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 27 Sep 2021 21:30:00 +0200 Subject: [PATCH 1/7] refactor(ci.yml): Fix indentation --- .github/workflows/ci.yml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d4cb324..7ec4389 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -6,12 +6,12 @@ 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 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 + with: + custom_image: ${{ matrix.image }} From 2f342435b8b5225a93c5870ad2e68773c96135a6 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 27 Sep 2021 22:51:53 +0200 Subject: [PATCH 2/7] refactor(ci.yml): Add workflow name --- .github/workflows/ci.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7ec4389..0251f13 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,3 +1,5 @@ +name: Docker CI + on: [push, pull_request] jobs: @@ -14,4 +16,5 @@ jobs: - uses: actions/checkout@v2 - uses: coq-community/docker-coq-action@v1 with: + opam_file: 'coq-mathcomp-multinomials.opam' custom_image: ${{ matrix.image }} From f8988bec7688b7c9e68fe18ddc2158d671d7a203 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 27 Sep 2021 22:54:28 +0200 Subject: [PATCH 3/7] chore: Bump coq version href: https://github.com/coq/opam-coq-archive/commit/e0f156558b2ce6ab8b1be29051d62bfa09a6099d --- coq-mathcomp-multinomials.opam | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/coq-mathcomp-multinomials.opam b/coq-mathcomp-multinomials.opam index 4a7ee7b..199d658 100644 --- a/coq-mathcomp-multinomials.opam +++ b/coq-mathcomp-multinomials.opam @@ -1,5 +1,4 @@ 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" @@ -8,7 +7,7 @@ license: "CeCILL-B" authors: ["Pierre-Yves Strub"] build: [ "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" From f567af0059f942944fff00640fe966b9a9e73937 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 27 Sep 2021 22:48:58 +0200 Subject: [PATCH 4/7] feat: Test "coqc -native-compiler yes" support * For details, see also: - https://opam.ocaml.org/packages/coq-native/ - CEP 48 --- .github/workflows/ci.yml | 42 ++++++++++++++++++++++++++++++++- configure | 50 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 91 insertions(+), 1 deletion(-) create mode 100755 configure diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0251f13..428ecd6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -10,11 +10,51 @@ jobs: 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.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 + 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 + if coq_native_compiler; 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 + 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 diff --git a/configure b/configure new file mode 100755 index 0000000..8dd416d --- /dev/null +++ b/configure @@ -0,0 +1,50 @@ +#!/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() { + if coq_native_compiler; 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) From a2972cac903b55052f17250274bd22a4b2b8bd4d Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 28 Sep 2021 03:24:44 +0200 Subject: [PATCH 5/7] docs(ci.yml): Add comments --- .github/workflows/ci.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 428ecd6..fab9aea 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -45,6 +45,9 @@ jobs: 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' @@ -58,3 +61,4 @@ jobs: 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 From 6f737bb0c674da21bad99cfb15a4cc27601ba7cd Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 28 Sep 2021 03:10:51 +0200 Subject: [PATCH 6/7] fix(coq-native): Run ./configure before the dune build * Bump dune-project accordingly --- .gitignore | 2 ++ coq-mathcomp-multinomials.opam | 5 ++++- dune-project | 4 ++-- src/{dune => dune.in} | 1 + 4 files changed, 9 insertions(+), 3 deletions(-) rename src/{dune => dune.in} (85%) 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/coq-mathcomp-multinomials.opam b/coq-mathcomp-multinomials.opam index 199d658..84d57aa 100644 --- a/coq-mathcomp-multinomials.opam +++ b/coq-mathcomp-multinomials.opam @@ -5,7 +5,10 @@ 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.15~") | = "dev"} "dune" {>= "2.5"} 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 From 52988b64863644eb1afd9c16beb181314004d80e Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 28 Sep 2021 14:23:15 +0200 Subject: [PATCH 7/7] refactor: Don't require (mode native) for Coq >= 8.12.1 & < 8.13 * 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 | 4 +++- configure | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fab9aea..b0c1d1c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -35,7 +35,9 @@ jobs: . configure # sourcing mandatory coq_version endGroup - if coq_native_compiler; then + # 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 diff --git a/configure b/configure index 8dd416d..1c5c6fc 100755 --- a/configure +++ b/configure @@ -36,7 +36,9 @@ coq_native_compiler() { } main() { - if coq_native_compiler; then + # 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