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).

6 files changed, 27 insertions, 23 deletions

diff --git a/Makefile.build b/Makefile.build
index 26a40c6cc..10d314f0d 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -195,8 +195,8 @@ MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
 OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
 
-BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS)
-OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
+BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
+OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
 DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$<),, -I ide -I ide/utils)
 
 # On MacOS, the binaries are signed, except our private ones
diff --git a/config/coq_config.mli b/config/coq_config.mli
index b0f39e9d2..429d8811b 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -36,6 +36,7 @@ val camlp4compat : string (* compatibility argument to camlp4/5 *)
 
 val coqideincl : string (* arguments for building coqide (e.g. lablgtk) *)
 val cflags : string     (* arguments passed to gcc *)
+val caml_flags : string     (* arguments passed to ocamlc (ie. CAMLFLAGS) *)
 
 val best : string       (* byte/opt *)
 val arch : string       (* architecture *)
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";
diff --git a/lib/envars.ml b/lib/envars.ml
index 68604ae6c..206d75033 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -213,6 +213,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs =
   fprintf f "%sCAMLP4BIN=%s/\n" prefix_var_name (camlp4bin ());
   fprintf f "%sCAMLP4LIB=%s\n" prefix_var_name (camlp4lib ());
   fprintf f "%sCAMLP4OPTIONS=%s\n" prefix_var_name Coq_config.camlp4compat;
+  fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags;
   fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name
     (if Coq_config.has_natdynlink then "true" else "false");
   fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs)
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index f4d1118d0..6d51838c1 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -39,6 +39,7 @@ CAMLP4O           := $(COQMF_CAMLP4O)
 CAMLP4BIN         := $(COQMF_CAMLP4BIN)
 CAMLP4LIB         := $(COQMF_CAMLP4LIB)
 CAMLP4OPTIONS     := $(COQMF_CAMLP4OPTIONS)
+CAMLFLAGS         := $(COQMF_CAMLFLAGS)
 HASNATDYNLINK     := $(COQMF_HASNATDYNLINK)
 
 @CONF_FILE@: @PROJECT_FILE@
@@ -100,11 +101,11 @@ AFTER ?=
 CAMLDONTLINK=camlp5.gramlib,unix,str
 
 # OCaml binaries
-CAMLC       ?= "$(OCAMLFIND)" ocamlc -c -rectypes -thread
-CAMLOPTC    ?= "$(OCAMLFIND)" opt    -c -rectypes -thread
-CAMLLINK    ?= "$(OCAMLFIND)" ocamlc    -rectypes -thread -linkpkg -dontlink $(CAMLDONTLINK)
-CAMLOPTLINK ?= "$(OCAMLFIND)" opt       -rectypes -thread -linkpkg -dontlink $(CAMLDONTLINK)
-CAMLDOC     ?= "$(OCAMLFIND)" ocamldoc  -rectypes
+CAMLC       ?= "$(OCAMLFIND)" ocamlc   -c
+CAMLOPTC    ?= "$(OCAMLFIND)" opt      -c
+CAMLLINK    ?= "$(OCAMLFIND)" ocamlc   -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLOPTLINK ?= "$(OCAMLFIND)" opt      -linkpkg -dontlink $(CAMLDONTLINK)
+CAMLDOC     ?= "$(OCAMLFIND)" ocamldoc
 CAMLDEP     ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
 
 # DESTDIR is prepended to all installation paths
@@ -114,8 +115,6 @@ DESTDIR ?=
 CAMLDEBUG ?=
 COQDEBUG ?=
 
-# Extra flags to the OCaml compiler
-CAMLFLAGS ?=
 # Extra packages to be linked in (as in findlib -package)
 CAMLPKGS ?=
 
@@ -749,7 +748,7 @@ printenv::
 # file you can extend the merlin-hook target in @LOCAL_FILE@
 .merlin:
 	$(SHOW)'FILL .merlin'
-	$(HIDE)echo 'FLG -rectypes -thread' > .merlin
+	$(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin
 	$(HIDE)echo 'B $(COQLIB)' >> .merlin
 	$(HIDE)echo 'S $(COQLIB)' >> .merlin
 	$(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 28a3c791c..524fe6323 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -271,8 +271,10 @@ let main () =
   try
     (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper.
        - With the coq .cma, we MUST use the -linkall option. *)
+    let coq_camlflags =
+      List.filter ((<>) "") (String.split_on_char ' ' Coq_config.caml_flags) in
     let args =
-      "-linkall" :: "-rectypes" :: "-w" :: "-31" :: flags @ copts @ options @
+      coq_camlflags @ "-linkall" :: "-w" :: "-31" :: flags @ copts @ options @
       (std_includes basedir) @ tolink @ [ main_file ] @ topstart
     in
     if !echo then begin