From 5fc5beecdcc74e177dbeb42f4c0a4b9becf1e790 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Tue, 28 Sep 2021 13:45:36 +0200 Subject: [PATCH] feat: Take advantage of the coq-native package (CEP 048, item 3) * href: https://github.com/coq/ceps/blob/master/text/048-packaging-coq-native.md#regarding-item-3 * Only update coq-mathcomp-multinomials.dev's deps and mathcomp.1.12.0 (some similar PRs could be opened for other deps if need be). --- .../coq-mathcomp-algebra/coq-mathcomp-algebra.1.12.0/opam | 2 +- .../coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.0/opam | 2 +- .../coq-mathcomp-character/coq-mathcomp-character.1.12.0/opam | 2 +- .../coq-mathcomp-field-extra.1.6.1/opam | 2 +- .../packages/coq-mathcomp-field/coq-mathcomp-field.1.12.0/opam | 2 +- .../coq-mathcomp-fingroup/coq-mathcomp-fingroup.1.12.0/opam | 2 +- .../packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.0/opam | 2 +- .../packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.1/opam | 2 +- .../coq-mathcomp-solvable/coq-mathcomp-solvable.1.12.0/opam | 2 +- .../coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.12.0/opam | 2 +- 10 files changed, 10 insertions(+), 10 deletions(-) diff --git a/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.1.12.0/opam b/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.1.12.0/opam index c013aba8d..30291a28c 100644 --- a/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.1.12.0/opam +++ b/released/packages/coq-mathcomp-algebra/coq-mathcomp-algebra.1.12.0/opam @@ -6,7 +6,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/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" ] depends: [ "coq-mathcomp-fingroup" { = version } ] diff --git a/released/packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.0/opam b/released/packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.0/opam index 965d24952..62c04e9a1 100644 --- a/released/packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.0/opam +++ b/released/packages/coq-mathcomp-bigenough/coq-mathcomp-bigenough.1.0.0/opam @@ -8,7 +8,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" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/bigenough'" ] depends: [ diff --git a/released/packages/coq-mathcomp-character/coq-mathcomp-character.1.12.0/opam b/released/packages/coq-mathcomp-character/coq-mathcomp-character.1.12.0/opam index 58a535761..a181a3ee8 100644 --- a/released/packages/coq-mathcomp-character/coq-mathcomp-character.1.12.0/opam +++ b/released/packages/coq-mathcomp-character/coq-mathcomp-character.1.12.0/opam @@ -6,7 +6,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/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" ] depends: [ "coq-mathcomp-field" { = version } ] diff --git a/released/packages/coq-mathcomp-field-extra/coq-mathcomp-field-extra.1.6.1/opam b/released/packages/coq-mathcomp-field-extra/coq-mathcomp-field-extra.1.6.1/opam index 78dee30a0..492a00661 100644 --- a/released/packages/coq-mathcomp-field-extra/coq-mathcomp-field-extra.1.6.1/opam +++ b/released/packages/coq-mathcomp-field-extra/coq-mathcomp-field-extra.1.6.1/opam @@ -7,7 +7,7 @@ homepage: "http://ssr.msr-inria.inria.fr/" bug-reports: "Mathematical Components " 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" ] depends: [ "ocaml" diff --git a/released/packages/coq-mathcomp-field/coq-mathcomp-field.1.12.0/opam b/released/packages/coq-mathcomp-field/coq-mathcomp-field.1.12.0/opam index a15dc9640..c4ca3e6bf 100644 --- a/released/packages/coq-mathcomp-field/coq-mathcomp-field.1.12.0/opam +++ b/released/packages/coq-mathcomp-field/coq-mathcomp-field.1.12.0/opam @@ -6,7 +6,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/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" ] depends: [ "coq-mathcomp-solvable" { = version } ] diff --git a/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.1.12.0/opam b/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.1.12.0/opam index 9b14331b5..474d5d0b4 100644 --- a/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.1.12.0/opam +++ b/released/packages/coq-mathcomp-fingroup/coq-mathcomp-fingroup.1.12.0/opam @@ -6,7 +6,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/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" ] depends: [ "coq-mathcomp-ssreflect" { = version } ] diff --git a/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.0/opam b/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.0/opam index 6c1a1c3ed..30b6ecda7 100644 --- a/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.0/opam +++ b/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.0/opam @@ -6,7 +6,7 @@ bug-reports: "https://github.com/math-comp/finmap/issues" dev-repo: "git+https://github.com/math-comp/finmap.git" license: "CECILL-B" -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.7" & < "8.13~") } diff --git a/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.1/opam b/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.1/opam index 312ee062b..ff422470c 100644 --- a/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.1/opam +++ b/released/packages/coq-mathcomp-finmap/coq-mathcomp-finmap.1.5.1/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.15~") | (= "dev") } diff --git a/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.1.12.0/opam b/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.1.12.0/opam index fd2eae02b..7898a84eb 100644 --- a/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.1.12.0/opam +++ b/released/packages/coq-mathcomp-solvable/coq-mathcomp-solvable.1.12.0/opam @@ -6,7 +6,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/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" ] depends: [ "coq-mathcomp-algebra" { = version } ] diff --git a/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.12.0/opam b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.12.0/opam index 7c308c80e..0b53547dd 100644 --- a/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.12.0/opam +++ b/released/packages/coq-mathcomp-ssreflect/coq-mathcomp-ssreflect.1.12.0/opam @@ -6,7 +6,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.10" & < "8.15~") } ]