From 324072c12a164f98d0ffa8125d319ffb49df87d8 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 31 Oct 2019 17:04:48 +0100
Subject: Communicate CFLAGS to dune

---
 .gitignore          |  1 +
 configure.ml        | 10 ++++++++++
 kernel/byterun/dune | 13 +++++++++++++
 3 files changed, 24 insertions(+)

diff --git a/.gitignore b/.gitignore
index ad5204847c..50b29b213e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -150,6 +150,7 @@ plugins/ssr/ssrvernac.ml
 
 # other auto-generated files
 
+kernel/byterun/dune.c_flags
 kernel/byterun/coq_instruct.h
 kernel/byterun/coq_jumptbl.h
 kernel/genOpcodeFiles.exe
diff --git a/configure.ml b/configure.ml
index af07ec4bb0..a53292b4cf 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1208,6 +1208,16 @@ let write_makefile f =
 
 let _ = write_makefile "config/Makefile"
 
+let write_dune_c_flags f =
+  safe_remove f;
+  let o = open_out f in
+  let pr s = fprintf o s in
+  pr "(%s)\n" cflags;
+  close_out o;
+  Unix.chmod f 0o444
+
+let _ = try write_dune_c_flags "kernel/byterun/dune.c_flags" with _ -> ()
+
 let write_macos_metadata exec =
   let f = "config/Info-"^exec^".plist" in
   let () = safe_remove f in
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index 20bdf28e54..d0145176ea 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -1,3 +1,16 @@
+; Dune doesn't use configure's output, but it is still necessary for
+; some Coq files to work; will be fixed in the future.
+(rule
+ (targets dune.c_flags)
+ (mode fallback)
+ (deps %{project_root}/configure.ml %{project_root}/dev/ocamldebug-coq.run (env_var COQ_CONFIGURE_PREFIX))
+ (action (chdir %{project_root} (run %{ocaml} configure.ml -no-ask -native-compiler no))))
+
+(env
+ (dev     (c_flags (:include dune.c_flags)))
+ (release (c_flags (:include dune.c_flags)))
+ (ireport (c_flags (:include dune.c_flags))))
+
 (library
  (name byterun)
  (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
-- 
cgit v1.2.3