From 0cc5e2790b9aea327b21aa1e167489b7c1bc63b5 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 7 Sep 2023 19:14:51 -0700
Subject: [PATCH] Fix coq-vst.2.12 to work with coq-native installed

Version 2.13 will not need this patch, as CompCert 3.13 contains a fix
for https://github.com/AbsInt/CompCert/issues/476
---
 .../files/0001-coq-native-fix.patch           | 54 +++++++++++++++++++
 .../packages/coq-vst-32/coq-vst-32.2.12/opam  |  9 ++--
 .../coq-vst-lib/coq-vst-lib.2.12/opam         |  6 +--
 .../files/0001-coq-native-fix.patch           | 54 +++++++++++++++++++
 released/packages/coq-vst/coq-vst.2.12/opam   |  9 ++--
 5 files changed, 123 insertions(+), 9 deletions(-)
 create mode 100644 released/packages/coq-vst-32/coq-vst-32.2.12/files/0001-coq-native-fix.patch
 create mode 100644 released/packages/coq-vst/coq-vst.2.12/files/0001-coq-native-fix.patch

diff --git a/released/packages/coq-vst-32/coq-vst-32.2.12/files/0001-coq-native-fix.patch b/released/packages/coq-vst-32/coq-vst-32.2.12/files/0001-coq-native-fix.patch
new file mode 100644
index 000000000..50ea0d633
--- /dev/null
+++ b/released/packages/coq-vst-32/coq-vst-32.2.12/files/0001-coq-native-fix.patch
@@ -0,0 +1,54 @@
+diff --git a/Makefile b/Makefile
+index 22f9374e..05726096 100644
+--- a/Makefile
++++ b/Makefile
+@@ -69,6 +69,7 @@ COMPCERT ?= platform
+ ZLIST ?= bundled
+ ARCH ?=
+ BITSIZE ?=
++COQEXTRAFLAGS ?=
+ 
+ # # Internal variables #
+ # Set to true if the bundled CompCert is used
+@@ -340,6 +341,7 @@ $(info COMPCERT_EXPLICIT_PATH=$(COMPCERT_EXPLICIT_PATH))
+ $(info COMPCERT_BUILD_FROM_SRC=$(COMPCERT_BUILD_FROM_SRC))
+ $(info COMPCERT_NEW=$(COMPCERT_NEW))
+ $(info COQFLAGS=$(COQFLAGS))
++$(info COQEXTRAFLAGS=$(COQEXTRAFLAGS))
+ $(info COMPCERT_R_FLAGS=$(COMPCERT_R_FLAGS))
+ $(info =================================)
+ 
+@@ -685,7 +687,7 @@ IRIS_INSTALL_FILES=$(sort $(IRIS_INSTALL_FILES_SRC) $(IRIS_INSTALL_FILES_VO))
+ 
+ # This line sets COQF depending on the folder of the input file $<
+ # If the folder name contains compcert, $(COMPCERT_R_FLAGS) is added, otherwise not.
+-%.vo: COQF=$(if $(findstring $(COMPCERT_SRC_DIR), $(dir $<)), $(COMPCERT_R_FLAGS), $(COQFLAGS))
++%.vo: COQF=$(if $(findstring $(COMPCERT_SRC_DIR), $(dir $<)), $(COMPCERT_R_FLAGS), $(COQFLAGS)) $(COQEXTRAFLAGS)
+ 
+ # If CompCert changes, all .vo files need to be recompiled
+ %.vo: $(COMPCERT_CONFIG)
+@@ -793,8 +795,8 @@ install: VST.config
+ 	for f in $(EXTRA_INSTALL_FILES); do install -m 0644 $$f "$(INSTALLDIR)/$$(dirname $$f)"; done
+ 
+ build-iris: _CoqProject
+-	$(COQC) $(COQFLAGS) $(PROGSDIR)/incr.v
+-	for f in $(IRIS_INSTALL_FILES_SRC); do if [ "$${f##*.}" = "v" ]; then echo COQC $$f; $(COQC) $(COQFLAGS) $$f; fi; done
++	$(COQC) $(COQFLAGS) $(COQEXTRAFLAGS) $(PROGSDIR)/incr.v
++	for f in $(IRIS_INSTALL_FILES_SRC); do if [ "$${f##*.}" = "v" ]; then echo COQC $$f; $(COQC) $(COQFLAGS) $(COQEXTRAFLAGS) $$f; fi; done
+ 
+ install-iris: VST.config
+ 	install -d "$(INSTALLDIR)"
+@@ -938,7 +940,7 @@ memmgr:  floyd/proofauto.vo floyd/library.vo floyd/VSU.vo
+ nothing: # need this target for the degenerate case of "make -tk */*.vo" in coq-action.yml
+ 
+ assumptions.txt: veric/tcb.vo
+-	$(COQC) $(COQFLAGS) veric/tcb.v > assumptions.txt
++	$(COQC) $(COQFLAGS) $(COQEXTRAFLAGS) veric/tcb.v > assumptions.txt
+ 	bash util/check_assumptions.sh
+ 
+ # $(CC_TARGET): compcert/make
+@@ -950,4 +952,3 @@ assumptions.txt: veric/tcb.vo
+ # such problem, not sure exactly.  -- Andrew)
+ include .depend
+ -include .depend-concur
+-
diff --git a/released/packages/coq-vst-32/coq-vst-32.2.12/opam b/released/packages/coq-vst-32/coq-vst-32.2.12/opam
index ef167488b..ded89e205 100644
--- a/released/packages/coq-vst-32/coq-vst-32.2.12/opam
+++ b/released/packages/coq-vst-32/coq-vst-32.2.12/opam
@@ -22,14 +22,17 @@ dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
 bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
 license: "BSD-2-Clause"
 
+patches: [
+  "0001-coq-native-fix.patch"
+]
 build: [
-  [make "-j%{jobs}%" "vst" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=32"]
+  [make "-j%{jobs}%" "vst" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=32" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
 ]
 install: [
-  [make "install" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=32"]
+  [make "install" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=32" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
 ]
 run-test: [
-  [make "-j%{jobs}%" "test" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=32"]
+  [make "-j%{jobs}%" "test" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=32" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
 ]
 depends: [
   "ocaml"
diff --git a/released/packages/coq-vst-lib/coq-vst-lib.2.12/opam b/released/packages/coq-vst-lib/coq-vst-lib.2.12/opam
index 8c297eb08..6632b19f2 100644
--- a/released/packages/coq-vst-lib/coq-vst-lib.2.12/opam
+++ b/released/packages/coq-vst-lib/coq-vst-lib.2.12/opam
@@ -13,13 +13,13 @@ bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
 license: "BSD-2-Clause"
 
 build: [
-  [ make "-C" "lib" "-j%{jobs}%" "proof-only"]
+  [ make "-C" "lib" "-j%{jobs}%" "proof-only" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed & coq-compcert:version < "3.13~"}]
 ]
 install: [
-  [ make "-C" "lib" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/VSTlib"]
+  [ make "-C" "lib" "install" "INSTALLDIR=%{lib}%/coq/user-contrib/VSTlib" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed & coq-compcert:version < "3.13~"}]
 ]
 run-test: [
-  [ make "-C" "lib" "-j%{jobs}%" "test-only"]
+  [ make "-C" "lib" "-j%{jobs}%" "test-only" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed & coq-compcert:version < "3.13~"}]
 ]
 depends: [
   "coq" {>= "8.16" & < "8.18~"}
diff --git a/released/packages/coq-vst/coq-vst.2.12/files/0001-coq-native-fix.patch b/released/packages/coq-vst/coq-vst.2.12/files/0001-coq-native-fix.patch
new file mode 100644
index 000000000..50ea0d633
--- /dev/null
+++ b/released/packages/coq-vst/coq-vst.2.12/files/0001-coq-native-fix.patch
@@ -0,0 +1,54 @@
+diff --git a/Makefile b/Makefile
+index 22f9374e..05726096 100644
+--- a/Makefile
++++ b/Makefile
+@@ -69,6 +69,7 @@ COMPCERT ?= platform
+ ZLIST ?= bundled
+ ARCH ?=
+ BITSIZE ?=
++COQEXTRAFLAGS ?=
+ 
+ # # Internal variables #
+ # Set to true if the bundled CompCert is used
+@@ -340,6 +341,7 @@ $(info COMPCERT_EXPLICIT_PATH=$(COMPCERT_EXPLICIT_PATH))
+ $(info COMPCERT_BUILD_FROM_SRC=$(COMPCERT_BUILD_FROM_SRC))
+ $(info COMPCERT_NEW=$(COMPCERT_NEW))
+ $(info COQFLAGS=$(COQFLAGS))
++$(info COQEXTRAFLAGS=$(COQEXTRAFLAGS))
+ $(info COMPCERT_R_FLAGS=$(COMPCERT_R_FLAGS))
+ $(info =================================)
+ 
+@@ -685,7 +687,7 @@ IRIS_INSTALL_FILES=$(sort $(IRIS_INSTALL_FILES_SRC) $(IRIS_INSTALL_FILES_VO))
+ 
+ # This line sets COQF depending on the folder of the input file $<
+ # If the folder name contains compcert, $(COMPCERT_R_FLAGS) is added, otherwise not.
+-%.vo: COQF=$(if $(findstring $(COMPCERT_SRC_DIR), $(dir $<)), $(COMPCERT_R_FLAGS), $(COQFLAGS))
++%.vo: COQF=$(if $(findstring $(COMPCERT_SRC_DIR), $(dir $<)), $(COMPCERT_R_FLAGS), $(COQFLAGS)) $(COQEXTRAFLAGS)
+ 
+ # If CompCert changes, all .vo files need to be recompiled
+ %.vo: $(COMPCERT_CONFIG)
+@@ -793,8 +795,8 @@ install: VST.config
+ 	for f in $(EXTRA_INSTALL_FILES); do install -m 0644 $$f "$(INSTALLDIR)/$$(dirname $$f)"; done
+ 
+ build-iris: _CoqProject
+-	$(COQC) $(COQFLAGS) $(PROGSDIR)/incr.v
+-	for f in $(IRIS_INSTALL_FILES_SRC); do if [ "$${f##*.}" = "v" ]; then echo COQC $$f; $(COQC) $(COQFLAGS) $$f; fi; done
++	$(COQC) $(COQFLAGS) $(COQEXTRAFLAGS) $(PROGSDIR)/incr.v
++	for f in $(IRIS_INSTALL_FILES_SRC); do if [ "$${f##*.}" = "v" ]; then echo COQC $$f; $(COQC) $(COQFLAGS) $(COQEXTRAFLAGS) $$f; fi; done
+ 
+ install-iris: VST.config
+ 	install -d "$(INSTALLDIR)"
+@@ -938,7 +940,7 @@ memmgr:  floyd/proofauto.vo floyd/library.vo floyd/VSU.vo
+ nothing: # need this target for the degenerate case of "make -tk */*.vo" in coq-action.yml
+ 
+ assumptions.txt: veric/tcb.vo
+-	$(COQC) $(COQFLAGS) veric/tcb.v > assumptions.txt
++	$(COQC) $(COQFLAGS) $(COQEXTRAFLAGS) veric/tcb.v > assumptions.txt
+ 	bash util/check_assumptions.sh
+ 
+ # $(CC_TARGET): compcert/make
+@@ -950,4 +952,3 @@ assumptions.txt: veric/tcb.vo
+ # such problem, not sure exactly.  -- Andrew)
+ include .depend
+ -include .depend-concur
+-
diff --git a/released/packages/coq-vst/coq-vst.2.12/opam b/released/packages/coq-vst/coq-vst.2.12/opam
index e247e525b..b97353e6a 100644
--- a/released/packages/coq-vst/coq-vst.2.12/opam
+++ b/released/packages/coq-vst/coq-vst.2.12/opam
@@ -22,14 +22,17 @@ dev-repo: "git+https://github.com/PrincetonUniversity/VST.git"
 bug-reports: "https://github.com/PrincetonUniversity/VST/issues"
 license: "BSD-2-Clause"
 
+patches: [
+  "0001-coq-native-fix.patch"
+]
 build: [
-  [make "-j%{jobs}%" "vst" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
+  [make "-j%{jobs}%" "vst" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
 ]
 install: [
-  [make "install" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
+  [make "install" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
 ]
 run-test: [
-  [make "-j%{jobs}%" "test" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64"]
+  [make "-j%{jobs}%" "test" "IGNORECOQVERSION=true" "ZLIST=platform" "BITSIZE=64" "COQEXTRAFLAGS=-native-compiler ondemand" {coq-native:installed}]
 ]
 depends: [
   "ocaml"