From 02d5287d82b2bd583f14f2d29be41ce5796667f5 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 7 Sep 2023 20:23:29 -0700
Subject: [PATCH 1/2] Support coq-native by passing through `COQEXTRAFLAGS`

Since coq-interval doesn't build nor install .coq-native files, when
coq-native is installed, vcfloat should avoid looking for .coq-native
files.
---
 coq-vcfloat.opam | 6 +++---
 vcfloat/Makefile | 7 ++++---
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/coq-vcfloat.opam b/coq-vcfloat.opam
index 5c84090..221a1e4 100644
--- 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"]
+  [ make "-C" "vcfloat" "-j%{jobs}%" "vcfloat2" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
 ]
 install: [
-  [make "-C" "vcfloat" "-j%{jobs}%" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/vcfloat"]
+  [make "-C" "vcfloat" "-j%{jobs}%" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/vcfloat" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
 ]
 run-test: [
-  [make "-C" "vcfloat" "-j%{jobs}%" "tests"]
+  [make "-C" "vcfloat" "-j%{jobs}%" "tests" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
 ]
 depends: [
   "coq" {>= "8.16" & < "8.18~"}
diff --git a/vcfloat/Makefile b/vcfloat/Makefile
index 062b6bc..78fad69 100644
--- a/vcfloat/Makefile
+++ b/vcfloat/Makefile
@@ -1,11 +1,12 @@
 # This Makefile assumes that coq already has access to
 # Flocq, Interval, CompCert, etc.,
-# which will be true if coq was installed through opam 
+# which will be true if coq was installed through opam
 # or as a "Coq Platform" package.
 
 COQC=coqc
 COQDEP=coqdep
 COQFLAGS := $(shell cat _CoqProject)
+COQEXTRAFLAGS?=
 
 target:  vcfloat2 tests
 
@@ -16,7 +17,7 @@ tests: ../Test/Test.vo ../Test/TestFunc.vo ../Test/TestPaper.vo ../Test/Test2.vo
 vcfloat2:  VCFloat.vo FPCompCert.vo Version.vo FPLib.vo
 
 %.vo: %.v
-	$(COQC) $(COQFLAGS) $*.v
+	$(COQC) $(COQFLAGS) $(COQEXTRAFLAGS) $*.v
 
 ifdef INSTALLDIR
 INSTALLFILES=$(shell make -Bn vcfloat2 2>/dev/null | awk '/^coqc.*v$$/{print $$NF"o"}')
@@ -31,7 +32,7 @@ endif
 	install -d $(INSTALLDIR)
 	install -m 0644 $(INSTALLFILES) $(INSTALLDIR)
 
-depend: 
+depend:
 	$(COQDEP) $(COQFLAGS) *.v ../Test/*.v > .depend
 
 ifneq ($(MAKECMDGOALS),depend)

From abec7adebc2289da5442bf812ec46f29af425ff0 Mon Sep 17 00:00:00 2001
From: Jason Gross <jasongross9@gmail.com>
Date: Fri, 8 Sep 2023 07:08:02 -0700
Subject: [PATCH 2/2] Only use -native-compiler ondemand for
 coq-compcert:version < "3.13~"

---
 coq-vcfloat.opam | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/coq-vcfloat.opam b/coq-vcfloat.opam
index 221a1e4..6ce8989 100644
--- 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~"}