Only use -native-compiler ondemand for coq-compcert:version < "3.13~"

VeriNum · Sep 8, 2023 · abec7ad · abec7ad
1 parent 02d5287
commit abec7ad
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/coq-vcfloat.opam b/coq-vcfloat.opam
@@ -18,13 +18,13 @@ bug-reports: "https://github.com/VeriNum/vcfloat/issues"
 license: "LGPL-3.0-or-later"
 
 build: [
-  [ make "-C" "vcfloat" "-j%{jobs}%" "vcfloat2" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
+  [ make "-C" "vcfloat" "-j%{jobs}%" "vcfloat2" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed & coq-compcert:version < "3.13~"}]
 ]
 install: [
-  [make "-C" "vcfloat" "-j%{jobs}%" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/vcfloat" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
+  [make "-C" "vcfloat" "-j%{jobs}%" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/vcfloat" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed  & coq-compcert:version < "3.13~"}]
 ]
 run-test: [
-  [make "-C" "vcfloat" "-j%{jobs}%" "tests" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
+  [make "-C" "vcfloat" "-j%{jobs}%" "tests" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed  & coq-compcert:version < "3.13~"}]
 ]
 depends: [
   "coq" {>= "8.16" & < "8.18~"}