From 0cc07dd290eb85bbb167dae2985cd1e468df882c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
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).
---
 tools/CoqMakefile.in | 15 +++++++--------
 tools/coqmktop.ml    |  4 +++-
 2 files changed, 10 insertions(+), 9 deletions(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index f4d1118d0f..6d51838c1e 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 28a3c791cb..524fe63232 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
-- 
cgit v1.2.3


From ef5aeafb74e33be6ac5b93a9713a3769f5917bd6 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 3 Oct 2017 17:41:12 +0200
Subject: fix compilation on OCaml < 4.04

---
 tools/coqmktop.ml | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 524fe63232..c21db300ad 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -252,6 +252,17 @@ let create_tmp_main_file modules =
   with reraise ->
     clean main_name; raise reraise
 
+(* TODO: remove once OCaml 4.04 is adopted *)
+let split_on_char sep s =
+  let r = ref [] in
+  let j = ref (String.length s) in
+  for i = String.length s - 1 downto 0 do
+      if s.[i] = sep then begin
+      r := String.sub s (i + 1) (!j - i - 1) :: !r;
+      j := i
+    end
+  done;
+  String.sub s 0 !j :: !r
 
 (** {6 Main } *)
 
@@ -272,7 +283,7 @@ let main () =
     (* - 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
+      List.filter ((<>) "") (split_on_char ' ' Coq_config.caml_flags) in
     let args =
       coq_camlflags @ "-linkall" :: "-w" :: "-31" :: flags @ copts @ options @
       (std_includes basedir) @ tolink @ [ main_file ] @ topstart
-- 
cgit v1.2.3