feat: Take advantage of the coq-native package (CEP 048, item 3)

* Follow-up of PR coq#1835
erikmd · Oct 18, 2021 · b88b9ba · b88b9ba
1 parent 4d5cbf1
commit b88b9ba
Show file tree

Hide file tree

Showing 8 changed files with 8 additions and 8 deletions.
diff --git a/extra-dev/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.dev/opam b/extra-dev/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.dev/opam
@@ -7,7 +7,7 @@ bug-reports: "Mathematical Components <[email protected]>"
 dev-repo: "git+https://github.com/math-comp/math-comp.git"
 license: "CeCILL-B"
 
-build: [ make "-C" "mathcomp/algebra" "-j" "%{jobs}%" ]
+build: [ make "-C" "mathcomp/algebra" "-j" "%{jobs}%" "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed & coq:version < "8.13~" } ]
 install: [ make "-C" "mathcomp/algebra" "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/algebra'" ]
 depends: [

diff --git a/extra-dev/packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.dev/opam b/extra-dev/packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.dev/opam
@@ -6,7 +6,7 @@ bug-reports: "https://github.com/math-comp/bigenough/issues"
 license: "CeCILL-B"
 dev-repo: "git+https://github.com/math-comp/bigenough"
 
-build: [ make "-j" "%{jobs}%" ]
+build: [ make "-j" "%{jobs}%" "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed & coq:version < "8.13~" } ]
 install: [ make "install" ]
 depends: [
   "ocaml"

diff --git a/extra-dev/packages/coq-mathcomp-character/coq-mathcomp-character.dev/opam b/extra-dev/packages/coq-mathcomp-character/coq-mathcomp-character.dev/opam
@@ -7,7 +7,7 @@ bug-reports: "Mathematical Components <[email protected]>"
 dev-repo: "git+https://github.com/math-comp/math-comp.git"
 license: "CeCILL-B"
 
-build: [ make "-C" "mathcomp/character" "-j" "%{jobs}%" ]
+build: [ make "-C" "mathcomp/character" "-j" "%{jobs}%" "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed & coq:version < "8.13~" } ]
 install: [ make "-C" "mathcomp/character" "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/character'" ]
 depends: [

diff --git a/extra-dev/packages/coq-mathcomp-field/coq-mathcomp-field.dev/opam b/extra-dev/packages/coq-mathcomp-field/coq-mathcomp-field.dev/opam
@@ -7,7 +7,7 @@ bug-reports: "Mathematical Components <[email protected]>"
 dev-repo: "git+https://github.com/math-comp/math-comp.git"
 license: "CeCILL-B"
 
-build: [ make "-C" "mathcomp/field" "-j" "%{jobs}%" ]
+build: [ make "-C" "mathcomp/field" "-j" "%{jobs}%" "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed & coq:version < "8.13~" } ]
 install: [ make "-C" "mathcomp/field" "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/field'" ]
 depends: [

diff --git a/extra-dev/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.dev/opam b/extra-dev/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.dev/opam
@@ -7,7 +7,7 @@ bug-reports: "Mathematical Components <[email protected]>"
 dev-repo: "git+https://github.com/math-comp/math-comp.git"
 license: "CeCILL-B"
 
-build: [ make "-C" "mathcomp/fingroup" "-j" "%{jobs}%" ]
+build: [ make "-C" "mathcomp/fingroup" "-j" "%{jobs}%" "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed & coq:version < "8.13~" } ]
 install: [ make "-C" "mathcomp/fingroup" "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/fingroup'" ]
 depends: [

diff --git a/extra-dev/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.dev/opam b/extra-dev/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.dev/opam
@@ -14,7 +14,7 @@ types). This includes support for functions with finite support and
 multisets. The library also contains a generic order and set libary,
 which will be used to subsume notations for finite sets, eventually."""
 
-build: [make "-j%{jobs}%" ]
+build: [make "-j%{jobs}%" "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed & coq:version < "8.13~" } ]
 install: [make "install"]
 depends: [
   "coq" { (>= "8.10" & < "8.14~") | (= "dev") }

diff --git a/extra-dev/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.dev/opam b/extra-dev/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.dev/opam
@@ -7,7 +7,7 @@ bug-reports: "Mathematical Components <[email protected]>"
 dev-repo: "git+https://github.com/math-comp/math-comp.git"
 license: "CeCILL-B"
 
-build: [ make "-C" "mathcomp/solvable" "-j" "%{jobs}%" ]
+build: [ make "-C" "mathcomp/solvable" "-j" "%{jobs}%" "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed & coq:version < "8.13~" } ]
 install: [ make "-C" "mathcomp/solvable" "install" ]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/solvable'" ]
 depends: [

diff --git a/extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam b/extra-dev/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.dev/opam
@@ -7,7 +7,7 @@ bug-reports: "https://github.com/math-comp/math-comp/issues"
 dev-repo: "git+https://github.com/math-comp/math-comp.git"
 license: "CeCILL-B"
 
-build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" ]
+build: [ make "-C" "mathcomp/ssreflect" "-j" "%{jobs}%" "COQEXTRAFLAGS+=-native-compiler yes" {coq-native:installed & coq:version < "8.13~" } ]
 install: [ make "-C" "mathcomp/ssreflect" "install" ]
 depends: [ "coq" { (>= "8.11" & < "8.15~") | (= "dev") } ]