From 0cc07dd290eb85bbb167dae2985cd1e468df882c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 8 Sep 2017 23:13:53 +0200
Subject: coq_makefile: make sure compile flags for Coq and coq_makefile are in
 sync

E.g. -safe-string is set by configure.ml and made available to
both make (via config/Makefile) and coq_makefile (via
config/coq_config.ml -> lib/envars.ml -> CoqMakefile.in).
---
 configure.ml | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

(limited to 'configure.ml')

diff --git a/configure.ml b/configure.ml
index b5e456779..fc2233f78 100644
--- a/configure.ml
+++ b/configure.ml
@@ -263,10 +263,6 @@ module Prefs = struct
   let debug = ref true
   let profile = ref false
   let annotate = ref false
-  (* Note, disabling this should be OK, but be careful with the
-     sharing invariants.
-  *)
-  let safe_string = ref true
   let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
   let coqwebsite = ref "http://coq.inria.fr/"
   let force_caml_version = ref false
@@ -376,8 +372,9 @@ let coq_annotate_flag =
   then if program_in_path "ocamlmerlin" then "-bin-annot" else "-annot"
   else ""
 
-let coq_safe_string =
-  if !Prefs.safe_string then "-safe-string" else ""
+(* This variable can be overriden only for debug purposes, use with
+   care. *)
+let coq_safe_string = "-safe-string"
 
 let cflags = "-Wall -Wno-unused -g -O2"
 
@@ -512,19 +509,22 @@ let camltag = match caml_version_list with
     50: unexpected documentation comment: too common and annoying to avoid
     56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3
 *)
-let coq_warn_flags =
-  let warnings = "-w +a-4-9-27-41-42-44-45-48-50" in
-  let errors =
+let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50"
+let coq_warn_error =
     if !Prefs.warn_error
     then "-warn-error +a"
          ^ (if caml_version_nums > [4;2;3]
             then "-56"
             else "")
     else ""
-  in
-  warnings ^ " " ^ errors
 
+(* Flags used to compile Coq and plugins (via coq_makefile) *)
+let caml_flags =
+  Printf.sprintf "-thread -rectypes %s %s %s" coq_warnings coq_annotate_flag coq_safe_string
 
+(* Flags used to compile Coq but _not_ plugins (via coq_makefile) *)
+let coq_caml_flags =
+  coq_warn_error
 
 (** * CamlpX configuration *)
 
@@ -1050,6 +1050,7 @@ let write_configml f =
   pr_s "camlp4lib" camlpXlibdir;
   pr_s "camlp4compat" camlp4compat;
   pr_s "cflags" cflags;
+  pr_s "caml_flags" caml_flags;
   pr_s "best" best_compiler;
   pr_s "osdeplibs" osdeplibs;
   pr_s "version" coq_version;
@@ -1156,7 +1157,7 @@ let write_makefile f =
   pr "CAMLHLIB=%S\n\n" camllib;
   pr "# Caml link command and Caml make top command\n";
   pr "# Caml flags\n";
-  pr "CAMLFLAGS=-rectypes %s %s %s\n" coq_warn_flags coq_annotate_flag coq_safe_string;
+  pr "CAMLFLAGS=%s %s\n" caml_flags coq_caml_flags;
   pr "# User compilation flag\n";
   pr "USERFLAGS=\n\n";
   pr "# Flags for GCC\n";
-- 
cgit v1.2.3